Analysis of Boolean Functions in Lean

1.3. The orthonormal basis of parity functions🔗

Definition1.3.1
uses 0
Used by 2
Reverse dependency previews
Preview
Proposition 1.4.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-1-3fidelity-exact-with-lp-definition-represented-by-real-rpow

Definition 1.3. For functions f,g : \{-1,1\}^n \to \mathbb R, define \langle f,g\rangle =2^{-n}\sum_{x\in\{-1,1\}^n}f(x)g(x) =\mathbb E_{\boldsymbol{x}\sim\{-1,1\}^n}[f(\boldsymbol{x})g(\boldsymbol{x})]. Also write \lVert f\rVert_2=\sqrt{\langle f,f\rangle}, \qquad \lVert f\rVert_p=\mathbb E[|f(\boldsymbol{x})|^p]^{1/p}.

Lean code for Definition1.3.1●3 declarations
  • defdefined in FABL/Chapter01/ParityBasis.lean
    complete
    def FABL.uniformInner.{u_1} {Ω : Type u_1} [Fintype Ω] (f g : Ω → ℝ) : ℝ
    def FABL.uniformInner.{u_1} {Ω : Type u_1}
  [Fintype Ω] (f g : Ω → ℝ) : ℝ
    The normalized inner product `⟨f,g⟩ = 𝔼[f g]` from O'Donnell, Definition 1.3.
  • defdefined in FABL/Chapter01/ParityBasis.lean
    complete
    def FABL.uniformLpNorm.{u_1} {Ω : Type u_1} [Fintype Ω] (p : ℝ)
  (f : Ω → ℝ) : ℝ
    def FABL.uniformLpNorm.{u_1} {Ω : Type u_1}
  [Fintype Ω] (p : ℝ) (f : Ω → ℝ) : ℝ
    The normalized `Lᵖ` quantity `(𝔼[|f|ᵖ])¹ᐟᵖ` from O'Donnell, Definition 1.3.
  • theoremdefined in FABL/Chapter01/BasicFourierFormulas.lean
    complete
    theorem FABL.uniformLpNorm_two_eq_sqrt_uniformInner {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.uniformLpNorm 2 f = √(FABL.uniformInner f f)
    theorem FABL.uniformLpNorm_two_eq_sqrt_uniformInner
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.uniformLpNorm 2 f =
    √(FABL.uniformInner f f)
    O'Donnell, Definition 1.3: the normalized `L²` quantity is the square root of the normalized
self-inner product.
Definition1.3.2
uses 0
Used by 13
Reverse dependency previews
Preview
Lemma 1.3.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-1-3fidelity-exact

Notation 1.4. The notation \boldsymbol{x}\sim\{-1,1\}^n means that \boldsymbol{x} is a uniformly chosen random string from \{-1,1\}^n. Equivalently, the coordinates \boldsymbol{x}_i are independent and each is +1 or -1 with probability 1/2. Unless another distribution is specified, \Pr and \mathbb E refer to this uniform choice. Thus the expectation in Definition 1.3 may be written \mathbb E_{\boldsymbol{x}}[f(\boldsymbol{x})g(\boldsymbol{x})], \mathbb E[f(\boldsymbol{x})g(\boldsymbol{x})], or \mathbb E[fg].

Lean code for Definition1.3.2●2 declarations
  • defdefined in FABL/Chapter01/ParityBasis.lean
    complete
    def FABL.uniformPMF.{u_1} (Ω : Type u_1) [Fintype Ω] [Nonempty Ω] : PMF Ω
    def FABL.uniformPMF.{u_1} (Ω : Type u_1)
  [Fintype Ω] [Nonempty Ω] : PMF Ω
    The uniform distribution denoted by `x ∼ Ω`; see O'Donnell, Notation 1.4.
  • theoremdefined in FABL/Chapter01/ParityBasis.lean
    complete
    theorem FABL.integral_uniformPMF_eq_expect.{u_1} {Ω : Type u_1} [Fintype Ω]
  [Nonempty Ω] [MeasurableSpace Ω] [MeasurableSingletonClass Ω]
  (f : Ω → ℝ) :
  ∫ (x : Ω), f x ∂(FABL.uniformPMF Ω).toMeasure =
    Finset.univ.expect fun x => f x
    theorem FABL.integral_uniformPMF_eq_expect.{u_1}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  [MeasurableSpace Ω]
  [MeasurableSingletonClass Ω]
  (f : Ω → ℝ) :
  ∫ (x : Ω),
      f x ∂(FABL.uniformPMF Ω).toMeasure =
    Finset.univ.expect fun x => f x
    Integration against the uniform PMF is Mathlib's normalized finite expectation.
Theorem1.3.3
Statement uses 2
Statement dependency previews
Preview
Lemma 1.3.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 6
Reverse dependency previews
Preview
Lemma 1.2.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-1-3fidelity-exact-with-explicit-sign-domain

Theorem 1.5. The 2^n parity functions \chi_S : \{-1,1\}^n \to \{-1,1\}, indexed by S\subseteq[n], form an orthonormal basis for the real vector space V of functions \{-1,1\}^n\to\mathbb R; that is, \langle\chi_S,\chi_T\rangle= \begin{cases} 1 & \text{if }S=T,\\ 0 & \text{if }S\ne T. \end{cases}

Lean code for Theorem1.3.3●3 declarations
  • defdefined in FABL/Chapter01/ParityBasis.lean
    complete
    def FABL.binaryWalshBasis (n : ℕ) :
  Module.Basis (Finset (Fin n)) ℝ (FABL.F₂Cube n → ℝ)
    def FABL.binaryWalshBasis (n : ℕ) :
  Module.Basis (Finset (Fin n)) ℝ
    (FABL.F₂Cube n → ℝ)
    The subset-indexed real Walsh basis on `𝔽₂ⁿ`. Its construction delegates linear independence
to Mathlib's finite-character orthogonality infrastructure.
  • defdefined in FABL/Chapter01/ParityBasis.lean
    complete
    def FABL.walshBasis (n : ℕ) :
  Module.Basis (Finset (Fin n)) ℝ (FABL.SignCube n → ℝ)
    def FABL.walshBasis (n : ℕ) :
  Module.Basis (Finset (Fin n)) ℝ
    (FABL.SignCube n → ℝ)
    The subset-indexed real Walsh basis on the sign cube. Its construction regards the
multiplicative sign cube as an additive group and reuses Mathlib's `AddChar` linear independence.
  • theoremdefined in FABL/Chapter01/ParityBasis.lean
    complete
    theorem FABL.parity_orthonormal_basis {n : ℕ} :
  (∀ (S : Finset (Fin n)), (FABL.walshBasis n) S = FABL.monomial S) ∧
    ∀ (S T : Finset (Fin n)),
      FABL.uniformInner (FABL.monomial S) (FABL.monomial T) =
        if S = T then 1 else 0
    theorem FABL.parity_orthonormal_basis {n : ℕ} :
  (∀ (S : Finset (Fin n)),
      (FABL.walshBasis n) S =
        FABL.monomial S) ∧
    ∀ (S T : Finset (Fin n)),
      FABL.uniformInner (FABL.monomial S)
          (FABL.monomial T) =
        if S = T then 1 else 0
    O'Donnell, Theorem 1.5: the parity functions form an orthonormal basis.
Lemma1.3.4
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 1.3.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-1-3fidelity-exact

Fact 1.6. For x\in\{-1,1\}^n and S,T\subseteq[n], one has \chi_S(x)\chi_T(x)=\chi_{S\mathbin{\triangle}T}(x), where S\mathbin{\triangle}T denotes symmetric difference.

Lean code for Lemma1.3.4●1 theorem
  • theoremdefined in FABL/Chapter01/ParityBasis.lean
    complete
    theorem FABL.monomial_mul_monomial {n : ℕ} (S T : Finset (Fin n))
  (x : FABL.SignCube n) :
  FABL.monomial S x * FABL.monomial T x = FABL.monomial (symmDiff S T) x
    theorem FABL.monomial_mul_monomial {n : ℕ}
  (S T : Finset (Fin n))
  (x : FABL.SignCube n) :
  FABL.monomial S x * FABL.monomial T x =
    FABL.monomial (symmDiff S T) x
    O'Donnell, Fact 1.6 on its stated domain `{-1,1}ⁿ`.
Lemma1.3.5
uses 1used by 1✓L∃∀N
Tagssection-1-3fidelity-exact

Fact 1.7. For every S\subseteq[n], with \boldsymbol{x} uniform on \{-1,1\}^n, \mathbb E[\chi_S(\boldsymbol{x})] =\mathbb E\left[\prod_{i\in S}\boldsymbol{x}_i\right] =\begin{cases} 1 & \text{if }S=\varnothing,\\ 0 & \text{if }S\ne\varnothing. \end{cases}

Lean code for Lemma1.3.5●1 theorem
  • theoremdefined in FABL/Chapter01/ParityBasis.lean
    complete
    theorem FABL.expect_monomial {n : ℕ} (S : Finset (Fin n)) :
  (Finset.univ.expect fun x => FABL.monomial S x) =
    if S = ∅ then 1 else 0
    theorem FABL.expect_monomial {n : ℕ}
  (S : Finset (Fin n)) :
  (Finset.univ.expect fun x =>
      FABL.monomial S x) =
    if S = ∅ then 1 else 0
    O'Donnell, Fact 1.7 on its stated domain `{-1,1}ⁿ`.