Analysis of Boolean Functions in Lean

3.2. Subspaces and decision trees🔗

Lemma3.2.1
Statement uses 3
Statement dependency previews
Preview
Theorem 1.2.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 7
Reverse dependency previews
Preview
Definition 3.2.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-3-2supportfidelity-exact-vector-indexing

Vector-indexed Fourier characters and Equation (3.1). Regard \mathbb F_2^n as an n-dimensional vector space over \mathbb F_2. For \gamma,x\in\mathbb F_2^n, set \chi_\gamma(x)=(-1)^{\gamma\mathbin\cdot x}, where the dot product is computed in \mathbb F_2. Then \chi_0 is the constant-one function, \chi_{e_i} is the ith dictator, and \chi_\beta\chi_\gamma=\chi_{\beta+\gamma} \qquad\text{for all }\beta,\gamma\in\mathbb F_2^n. \tag{3.1} The indexing is injective and respects addition and multiplication, so the character family is identified with the additive group \mathbb F_2^n. Writing a second copy of the group as \widehat{\mathbb F_2^n}, every f:\mathbb F_2^n\to\mathbb R has the Fourier expansion f(x)=\sum_{\gamma\in\widehat{\mathbb F_2^n}} \widehat f(\gamma)\chi_\gamma(x).

Lean code for Lemma3.2.1●12 declarations
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    def FABL.f₂Support {n : ℕ} (γ : FABL.F₂Cube n) : Finset (Fin n)
    def FABL.f₂Support {n : ℕ}
  (γ : FABL.F₂Cube n) : Finset (Fin n)
    The support of a vector in `𝔽₂ⁿ`.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    def FABL.f₂CubeOfFinset {n : ℕ} (S : Finset (Fin n)) : FABL.F₂Cube n
    def FABL.f₂CubeOfFinset {n : ℕ}
  (S : Finset (Fin n)) : FABL.F₂Cube n
    The binary vector whose support is `S`.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    def FABL.f₂CubeEquivFinset (n : ℕ) : FABL.F₂Cube n ≃ Finset (Fin n)
    def FABL.f₂CubeEquivFinset (n : ℕ) :
  FABL.F₂Cube n ≃ Finset (Fin n)
    A vector in `𝔽₂ⁿ` is canonically equivalent to its finite support.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    theorem FABL.f₂DotProduct_eq_coordinateSum_f₂Support {n : ℕ}
  (γ x : FABL.F₂Cube n) :
  FABL.f₂DotProduct γ x = (FABL.coordinateSum (FABL.f₂Support γ)) x
    theorem FABL.f₂DotProduct_eq_coordinateSum_f₂Support
  {n : ℕ} (γ x : FABL.F₂Cube n) :
  FABL.f₂DotProduct γ x =
    (FABL.coordinateSum
        (FABL.f₂Support γ))
      x
    The dot product with a binary vector is the coordinate sum over its support.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    def FABL.vectorWalshCharacter {n : ℕ} (γ : FABL.F₂Cube n) :
  AddChar (FABL.F₂Cube n) ℝ
    def FABL.vectorWalshCharacter {n : ℕ}
  (γ : FABL.F₂Cube n) :
  AddChar (FABL.F₂Cube n) ℝ
    The Walsh character indexed by a vector of `𝔽₂ⁿ`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    theorem FABL.vectorWalshCharacter_apply {n : ℕ} (γ x : FABL.F₂Cube n) :
  (FABL.vectorWalshCharacter γ) x =
    FABL.binarySign (FABL.f₂DotProduct γ x)
    theorem FABL.vectorWalshCharacter_apply {n : ℕ}
  (γ x : FABL.F₂Cube n) :
  (FABL.vectorWalshCharacter γ) x =
    FABL.binarySign
      (FABL.f₂DotProduct γ x)
    The vector-indexed character has the book's dot-product formula.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    theorem FABL.vectorWalshCharacter_f₂CubeOfFinset_singleton {n : ℕ} (i : Fin n)
  (x : FABL.F₂Cube n) :
  (FABL.vectorWalshCharacter (FABL.f₂CubeOfFinset {i})) x =
    FABL.binarySign (x i)
    theorem FABL.vectorWalshCharacter_f₂CubeOfFinset_singleton
  {n : ℕ} (i : Fin n)
  (x : FABL.F₂Cube n) :
  (FABL.vectorWalshCharacter
        (FABL.f₂CubeOfFinset {i}))
      x =
    FABL.binarySign (x i)
    The character indexed by a standard basis vector is the corresponding binary dictator.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    theorem FABL.vectorWalshCharacter_zero {n : ℕ} : FABL.vectorWalshCharacter 0 = 1
    theorem FABL.vectorWalshCharacter_zero {n : ℕ} :
  FABL.vectorWalshCharacter 0 = 1
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    theorem FABL.vectorWalshCharacter_mul {n : ℕ} (β γ : FABL.F₂Cube n) :
  FABL.vectorWalshCharacter β * FABL.vectorWalshCharacter γ =
    FABL.vectorWalshCharacter (β + γ)
    theorem FABL.vectorWalshCharacter_mul {n : ℕ}
  (β γ : FABL.F₂Cube n) :
  FABL.vectorWalshCharacter β *
      FABL.vectorWalshCharacter γ =
    FABL.vectorWalshCharacter (β + γ)
    O'Donnell, Equation (3.1): vector-indexed Walsh characters multiply by adding indices.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    theorem FABL.vectorWalshCharacter_injective {n : ℕ} :
  Function.Injective FABL.vectorWalshCharacter
    theorem FABL.vectorWalshCharacter_injective
  {n : ℕ} :
  Function.Injective
    FABL.vectorWalshCharacter
    Vector indexing is injective on the Walsh character family.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    def FABL.vectorFourierCoeff {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (γ : FABL.F₂Cube n) : ℝ
    def FABL.vectorFourierCoeff {n : ℕ}
  (f : FABL.F₂Cube n → ℝ)
  (γ : FABL.F₂Cube n) : ℝ
    The Fourier coefficient indexed by a vector in the dual binary cube.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    theorem FABL.vector_fourier_expansion {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (x : FABL.F₂Cube n) :
  f x =
    ∑ γ, FABL.vectorFourierCoeff f γ * (FABL.vectorWalshCharacter γ) x
    theorem FABL.vector_fourier_expansion {n : ℕ}
  (f : FABL.F₂Cube n → ℝ)
  (x : FABL.F₂Cube n) :
  f x =
    ∑ γ,
      FABL.vectorFourierCoeff f γ *
        (FABL.vectorWalshCharacter γ) x
    Fourier expansion reindexed by the vector/finite-support equivalence.
Definition3.2.2
Statement uses 2
Statement dependency previews
Preview
Theorem 1.4.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Lemma 3.2.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-3-2fidelity-exact-with-infinity-convention

Definition 3.8. For f:\{-1,1\}^n\to\mathbb R and 1\le p<\infty, the Fourier or spectral p-norm is \lVert\widehat f\rVert_p =\left( \sum_{\gamma\in\widehat{\mathbb F_2^n}} |\widehat f(\gamma)|^p \right)^{1/p}. The sum uses counting measure on \widehat{\mathbb F_2^n}. For the endpoint used below, \lVert\widehat f\rVert_\infty =\max_{\gamma\in\widehat{\mathbb F_2^n}}|\widehat f(\gamma)|. Parseval's Theorem is equivalently \lVert f\rVert_2=\lVert\widehat f\rVert_2.

Lean code for Definition3.2.2●4 declarations
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    def FABL.spectralPNorm {n : ℕ} (p : ℝ) (f : FABL.F₂Cube n → ℝ) : ℝ
    def FABL.spectralPNorm {n : ℕ} (p : ℝ)
  (f : FABL.F₂Cube n → ℝ) : ℝ
    O'Donnell, Definition 3.8: the Fourier `p`-norm with counting measure, for finite real `p`.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    def FABL.spectralInfinityNorm {n : ℕ} (f : FABL.F₂Cube n → ℝ) : ℝ
    def FABL.spectralInfinityNorm {n : ℕ}
  (f : FABL.F₂Cube n → ℝ) : ℝ
    O'Donnell, Definition 3.8: the endpoint Fourier infinity norm.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    theorem FABL.vector_plancherel {n : ℕ} (f g : FABL.F₂Cube n → ℝ) :
  (Finset.univ.expect fun x => f x * g x) =
    ∑ γ, FABL.vectorFourierCoeff f γ * FABL.vectorFourierCoeff g γ
    theorem FABL.vector_plancherel {n : ℕ}
  (f g : FABL.F₂Cube n → ℝ) :
  (Finset.univ.expect fun x =>
      f x * g x) =
    ∑ γ,
      FABL.vectorFourierCoeff f γ *
        FABL.vectorFourierCoeff g γ
    Plancherel's identity reindexed by vectors in the dual binary cube.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    theorem FABL.uniformLpNorm_two_eq_spectralPNorm_two {n : ℕ}
  (f : FABL.F₂Cube n → ℝ) :
  FABL.uniformLpNorm 2 f = FABL.spectralPNorm 2 f
    theorem FABL.uniformLpNorm_two_eq_spectralPNorm_two
  {n : ℕ} (f : FABL.F₂Cube n → ℝ) :
  FABL.uniformLpNorm 2 f =
    FABL.spectralPNorm 2 f
    Parseval in the norm notation of O'Donnell's Definition 3.8.
Definition3.2.3
uses 1
Used by 3
Reverse dependency previews
Preview
Lemma 3.2.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-3-2fidelity-exact

Definition 3.9. The Fourier or spectral sparsity of f:\{-1,1\}^n\to\mathbb R is \operatorname{sparsity}(\widehat f) =|\operatorname{supp}(\widehat f)| =\#\{\gamma\in\widehat{\mathbb F_2^n}:\widehat f(\gamma)\ne0\}.

Lean code for Definition3.2.3●1 definition
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    def FABL.spectralSparsity {n : ℕ} (f : FABL.F₂Cube n → ℝ) : ℕ
    def FABL.spectralSparsity {n : ℕ}
  (f : FABL.F₂Cube n → ℝ) : ℕ
    O'Donnell, Definition 3.9: the number of nonzero Fourier coefficients.
Definition3.2.4
Statement uses 2
Statement dependency previews
Preview
Lemma 1.2.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Lemma 3.2.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-3-2fidelity-exact

Definition 3.10. The Fourier transform \widehat f is \epsilon-granular if every Fourier coefficient is an integer multiple of \epsilon; that is, \forall\gamma\in\widehat{\mathbb F_2^n}\;\exists z\in\mathbb Z, \qquad \widehat f(\gamma)=z\epsilon.

Lean code for Definition3.2.4●2 declarations
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    def FABL.IsVectorFourierGranular {n : ℕ} (f : FABL.F₂Cube n → ℝ) (ε : ℝ) :
  Prop
    def FABL.IsVectorFourierGranular {n : ℕ}
  (f : FABL.F₂Cube n → ℝ) (ε : ℝ) : Prop
    O'Donnell, Definition 3.10 in vector indexing, implemented by reusing the Chapter 1
`IsFourierGranular` predicate through the canonical cube equivalence.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/VectorFourier.lean
    complete
    theorem FABL.isVectorFourierGranular_iff {n : ℕ} (f : FABL.F₂Cube n → ℝ)
  (ε : ℝ) :
  FABL.IsVectorFourierGranular f ε ↔
    ∀ (γ : FABL.F₂Cube n), ∃ z, FABL.vectorFourierCoeff f γ = ↑z * ε
    theorem FABL.isVectorFourierGranular_iff {n : ℕ}
  (f : FABL.F₂Cube n → ℝ) (ε : ℝ) :
  FABL.IsVectorFourierGranular f ε ↔
    ∀ (γ : FABL.F₂Cube n),
      ∃ z,
        FABL.vectorFourierCoeff f γ =
          ↑z * ε
    The reused granularity predicate has the expected vector-coefficient formulation.
Lemma3.2.5
uses 1
Used by 3
Reverse dependency previews
Preview
Proposition 3.2.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-3-2supportfidelity-exact

Perpendicular subspaces over \mathbb F_2. For a linear subspace A\le\mathbb F_2^n, define A^\perp =\{\gamma\in\widehat{\mathbb F_2^n}: \gamma\mathbin\cdot x=0\text{ for every }x\in A\}. Then \dim A^\perp=n-\dim A, \qquad A=(A^\perp)^\perp. The quantity \dim A^\perp is the codimension of A.

Lean code for Lemma3.2.5●8 declarations
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    def FABL.f₂DotProductBilin (n : ℕ) :
  LinearMap.BilinForm FABL.𝔽₂ (FABL.F₂Cube n)
    def FABL.f₂DotProductBilin (n : ℕ) :
  LinearMap.BilinForm FABL.𝔽₂
    (FABL.F₂Cube n)
    The standard dot product as a bilinear form on `𝔽₂ⁿ`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.f₂DotProductBilin_nondegenerate {n : ℕ} :
  (FABL.f₂DotProductBilin n).Nondegenerate
    theorem FABL.f₂DotProductBilin_nondegenerate
  {n : ℕ} :
  (FABL.f₂DotProductBilin n).Nondegenerate
    The standard binary dot product is nondegenerate.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    def FABL.perpendicularSubspace {n : ℕ}
  (A : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  Submodule FABL.𝔽₂ (FABL.F₂Cube n)
    def FABL.perpendicularSubspace {n : ℕ}
  (A :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  Submodule FABL.𝔽₂ (FABL.F₂Cube n)
    The perpendicular subspace `Aᵖ` with respect to the standard binary dot product.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.mem_perpendicularSubspace_iff {n : ℕ}
  (A : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (γ : FABL.F₂Cube n) :
  γ ∈ FABL.perpendicularSubspace A ↔ ∀ x ∈ A, FABL.f₂DotProduct γ x = 0
    theorem FABL.mem_perpendicularSubspace_iff {n : ℕ}
  (A : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (γ : FABL.F₂Cube n) :
  γ ∈ FABL.perpendicularSubspace A ↔
    ∀ x ∈ A, FABL.f₂DotProduct γ x = 0
    Membership in `Aᵖ` is the book's pointwise dot-product condition.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    def FABL.f₂Codimension {n : ℕ} (A : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) : ℕ
    def FABL.f₂Codimension {n : ℕ}
  (A :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  ℕ
    The codimension of a binary subspace, defined as the dimension of its perpendicular.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.finrank_perpendicularSubspace {n : ℕ}
  (A : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  Module.finrank FABL.𝔽₂ ↥(FABL.perpendicularSubspace A) =
    n - Module.finrank FABL.𝔽₂ ↥A
    theorem FABL.finrank_perpendicularSubspace {n : ℕ}
  (A :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  Module.finrank FABL.𝔽₂
      ↥(FABL.perpendicularSubspace A) =
    n - Module.finrank FABL.𝔽₂ ↥A
    Mathlib's nondegenerate-form dimension theorem gives the dimension of `Aᵖ`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.perpendicularSubspace_perpendicularSubspace {n : ℕ}
  (A : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  FABL.perpendicularSubspace (FABL.perpendicularSubspace A) = A
    theorem FABL.perpendicularSubspace_perpendicularSubspace
  {n : ℕ}
  (A :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  FABL.perpendicularSubspace
      (FABL.perpendicularSubspace A) =
    A
    Taking the perpendicular twice recovers the original binary subspace.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.card_perpendicularSubspace {n : ℕ}
  (A : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  Nat.card ↥(FABL.perpendicularSubspace A) = 2 ^ FABL.f₂Codimension A
    theorem FABL.card_perpendicularSubspace {n : ℕ}
  (A :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  Nat.card
      ↥(FABL.perpendicularSubspace A) =
    2 ^ FABL.f₂Codimension A
    The perpendicular of a codimension-`k` binary subspace has `2ᵏ` elements.
Proposition3.2.6
Statement uses 3
Statement dependency previews
Preview
Definition 1.5.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Lemma 3.2.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-3-2fidelity-exact

Proposition 3.11. If A\le\mathbb F_2^n has \operatorname{codim}A=\dim A^\perp=k, then its indicator and its uniform probability density have the Fourier expansions \mathbf1_A =\sum_{\gamma\in A^\perp}2^{-k}\chi_\gamma, \qquad \varphi_A =\sum_{\gamma\in A^\perp}\chi_\gamma.

Lean code for Proposition3.2.6●5 declarations
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    def FABL.subspaceCharacterSum {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (x : FABL.F₂Cube n) : ℝ
    def FABL.subspaceCharacterSum {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (x : FABL.F₂Cube n) : ℝ
    The sum of all vector-indexed characters whose indices lie in `H`.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    def FABL.inversePerpendicularCard {n : ℕ}
  (A : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) : ℝ
    def FABL.inversePerpendicularCard {n : ℕ}
  (A :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  ℝ
    The coefficient `2⁻ᵏ` attached to a subspace of codimension `k`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.setIndicator_submodule_fourier_expansion {n : ℕ}
  (A : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  FABL.setIndicator ↑A = fun x =>
    FABL.inversePerpendicularCard A *
      FABL.subspaceCharacterSum (FABL.perpendicularSubspace A) x
    theorem FABL.setIndicator_submodule_fourier_expansion
  {n : ℕ}
  (A :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  FABL.setIndicator ↑A = fun x =>
    FABL.inversePerpendicularCard A *
      FABL.subspaceCharacterSum
        (FABL.perpendicularSubspace A) x
    O'Donnell, Proposition 3.11: the subspace indicator as a sum of the characters indexed by
the perpendicular subspace.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.subsetDensity_submodule_fourier_expansion {n : ℕ}
  (A : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  (FABL.subsetDensity ↑A ⋯).toFun =
    FABL.subspaceCharacterSum (FABL.perpendicularSubspace A)
    theorem FABL.subsetDensity_submodule_fourier_expansion
  {n : ℕ}
  (A :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  (FABL.subsetDensity ↑A ⋯).toFun =
    FABL.subspaceCharacterSum
      (FABL.perpendicularSubspace A)
    O'Donnell, Proposition 3.11: functional form of the subspace-density Fourier expansion.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.subspaceUniformProbability_eq_inversePerpendicularCard {n : ℕ}
  (A : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  FABL.subspaceUniformProbability A = FABL.inversePerpendicularCard A
    theorem FABL.subspaceUniformProbability_eq_inversePerpendicularCard
  {n : ℕ}
  (A :
    Submodule FABL.𝔽₂ (FABL.F₂Cube n)) :
  FABL.subspaceUniformProbability A =
    FABL.inversePerpendicularCard A
    The uniform probability of a binary subspace is the reciprocal of the size of its
perpendicular.
Lemma3.2.7
Statement uses 2
Statement dependency previews
Preview
Lemma 3.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Lemma 3.2.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-3-2supportfidelity-exact

Affine subspaces, parity conditions, and subcubes. If H\le\mathbb F_2^n and a\in\mathbb F_2^n, then the affine subspace A=H+a is equivalently A=\{x\in\mathbb F_2^n: \gamma\mathbin\cdot x=\gamma\mathbin\cdot a \text{ for every }\gamma\in H^\perp\}. When the displayed parity conditions specialize to coordinate equations x_i=a_i, their solution set is a subcube; the Lean declaration identifies this coordinate subcube with the corresponding affine subspace.

Lean code for Lemma3.2.7●5 declarations
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    def FABL.binaryAffineSubspace {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n) :
  AffineSubspace FABL.𝔽₂ (FABL.F₂Cube n)
    def FABL.binaryAffineSubspace {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) :
  AffineSubspace FABL.𝔽₂ (FABL.F₂Cube n)
    The affine translate `H + a`, represented by Mathlib's `AffineSubspace.mk'`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.mem_binaryAffineSubspace_iff_add_mem {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a x : FABL.F₂Cube n) :
  x ∈ FABL.binaryAffineSubspace H a ↔ x + a ∈ H
    theorem FABL.mem_binaryAffineSubspace_iff_add_mem
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a x : FABL.F₂Cube n) :
  x ∈ FABL.binaryAffineSubspace H a ↔
    x + a ∈ H
    In characteristic two, membership in `H + a` is equivalent to `x + a ∈ H`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.mem_binaryAffineSubspace_iff_forall_perpendicular_parity {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a x : FABL.F₂Cube n) :
  x ∈ FABL.binaryAffineSubspace H a ↔
    ∀ γ ∈ FABL.perpendicularSubspace H,
      FABL.f₂DotProduct γ x = FABL.f₂DotProduct γ a
    theorem FABL.mem_binaryAffineSubspace_iff_forall_perpendicular_parity
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a x : FABL.F₂Cube n) :
  x ∈ FABL.binaryAffineSubspace H a ↔
    ∀ γ ∈ FABL.perpendicularSubspace H,
      FABL.f₂DotProduct γ x =
        FABL.f₂DotProduct γ a
    Membership in an affine binary subspace is equivalently the system of all perpendicular
parity equations.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    def FABL.F₂DecisionTree.coordinateSubcube {n : ℕ}
  (coordinates : Finset (Fin n)) (basePoint : FABL.F₂Cube n) :
  Set (FABL.F₂Cube n)
    def FABL.F₂DecisionTree.coordinateSubcube
  {n : ℕ} (coordinates : Finset (Fin n))
  (basePoint : FABL.F₂Cube n) :
  Set (FABL.F₂Cube n)
    The coordinate subcube obtained by fixing the selected coordinates to a base point.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.coordinateSubcube_eq_binaryAffineSubspace {n : ℕ}
  (coordinates : Finset (Fin n)) (basePoint : FABL.F₂Cube n) :
  FABL.F₂DecisionTree.coordinateSubcube coordinates basePoint =
    ↑(FABL.binaryAffineSubspace
        (FABL.F₂DecisionTree.coordinateZeroSubspace coordinates)
        basePoint)
    theorem FABL.F₂DecisionTree.coordinateSubcube_eq_binaryAffineSubspace
  {n : ℕ} (coordinates : Finset (Fin n))
  (basePoint : FABL.F₂Cube n) :
  FABL.F₂DecisionTree.coordinateSubcube
      coordinates basePoint =
    ↑(FABL.binaryAffineSubspace
        (FABL.F₂DecisionTree.coordinateZeroSubspace
          coordinates)
        basePoint)
    Fixing coordinates is exactly the affine subspace with coordinate-zero direction.
Lemma3.2.8
Statement uses 5
Statement dependency previews
Preview
Definition 3.2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-3-2supportfidelity-exact

Exercise 3.11. Derive the affine extension of Proposition 3.11. Namely, if A=H+a has codimension k, prove \widehat{\mathbf1_A}(\gamma) =\begin{cases} \chi_\gamma(a)2^{-k},&\gamma\in H^\perp,\\ 0,&\gamma\notin H^\perp, \end{cases} and hence \varphi_A=\sum_{\gamma\in H^\perp} \chi_\gamma(a)\chi_\gamma. Also prove \operatorname{sparsity}(\widehat{\mathbf1_A})=2^k, \qquad \lVert\widehat{\mathbf1_A}\rVert_\infty=2^{-k}, \qquad \lVert\widehat{\mathbf1_A}\rVert_1=1, and that \widehat{\mathbf1_A} is 2^{-k}-granular.

Lean code for Lemma3.2.8●6 theorems
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.setIndicator_binaryAffineSubspace_apply {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a x : FABL.F₂Cube n) :
  FABL.setIndicator (↑(FABL.binaryAffineSubspace H a)) x =
    FABL.inversePerpendicularCard H *
      FABL.subspaceCharacterSum (FABL.perpendicularSubspace H) (x + a)
    theorem FABL.setIndicator_binaryAffineSubspace_apply
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a x : FABL.F₂Cube n) :
  FABL.setIndicator
      (↑(FABL.binaryAffineSubspace H a))
      x =
    FABL.inversePerpendicularCard H *
      FABL.subspaceCharacterSum
        (FABL.perpendicularSubspace H)
        (x + a)
    O'Donnell, Proposition 3.12: pointwise Fourier expansion of an affine-subspace indicator.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.affineSubspaceUniformProbability_eq_inversePerpendicularCard
  {n : ℕ} (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n) :
  FABL.affineSubspaceUniformProbability H a =
    FABL.inversePerpendicularCard H
    theorem FABL.affineSubspaceUniformProbability_eq_inversePerpendicularCard
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) :
  FABL.affineSubspaceUniformProbability H
      a =
    FABL.inversePerpendicularCard H
    The uniform probability of an affine subspace is `2⁻ᵏ`, where `k` is its
codimension.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.vectorFourierCoeff_setIndicator_binaryAffineSubspace_ne_zero_iff
  {n : ℕ} (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a γ : FABL.F₂Cube n) :
  FABL.vectorFourierCoeff
        (FABL.setIndicator ↑(FABL.binaryAffineSubspace H a)) γ ≠
      0 ↔
    γ ∈ FABL.perpendicularSubspace H
    theorem FABL.vectorFourierCoeff_setIndicator_binaryAffineSubspace_ne_zero_iff
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a γ : FABL.F₂Cube n) :
  FABL.vectorFourierCoeff
        (FABL.setIndicator
          ↑(FABL.binaryAffineSubspace H
              a))
        γ ≠
      0 ↔
    γ ∈ FABL.perpendicularSubspace H
    The Fourier support of an affine-subspace indicator is exactly the perpendicular direction.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.abs_vectorFourierCoeff_setIndicator_binaryAffineSubspace_of_mem
  {n : ℕ} (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a γ : FABL.F₂Cube n)
  (hγ : γ ∈ FABL.perpendicularSubspace H) :
  |FABL.vectorFourierCoeff
        (FABL.setIndicator ↑(FABL.binaryAffineSubspace H a)) γ| =
    FABL.inversePerpendicularCard H
    theorem FABL.abs_vectorFourierCoeff_setIndicator_binaryAffineSubspace_of_mem
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a γ : FABL.F₂Cube n)
  (hγ :
    γ ∈ FABL.perpendicularSubspace H) :
  |FABL.vectorFourierCoeff
        (FABL.setIndicator
          ↑(FABL.binaryAffineSubspace H
              a))
        γ| =
    FABL.inversePerpendicularCard H
    Every Fourier coefficient on the perpendicular direction has absolute value `2⁻ᵏ`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.abs_vectorFourierCoeff_setIndicator_binaryAffineSubspace_of_not_mem
  {n : ℕ} (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a γ : FABL.F₂Cube n)
  (hγ : γ ∉ FABL.perpendicularSubspace H) :
  |FABL.vectorFourierCoeff
        (FABL.setIndicator ↑(FABL.binaryAffineSubspace H a)) γ| =
    0
    theorem FABL.abs_vectorFourierCoeff_setIndicator_binaryAffineSubspace_of_not_mem
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a γ : FABL.F₂Cube n)
  (hγ :
    γ ∉ FABL.perpendicularSubspace H) :
  |FABL.vectorFourierCoeff
        (FABL.setIndicator
          ↑(FABL.binaryAffineSubspace H
              a))
        γ| =
    0
    Every Fourier coefficient off the perpendicular direction has absolute value zero.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.sum_abs_vectorFourierCoeff_setIndicator_binaryAffineSubspace
  {n : ℕ} (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n) :
  ∑ γ,
      |FABL.vectorFourierCoeff
          (FABL.setIndicator ↑(FABL.binaryAffineSubspace H a)) γ| =
    1
    theorem FABL.sum_abs_vectorFourierCoeff_setIndicator_binaryAffineSubspace
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) :
  ∑ γ,
      |FABL.vectorFourierCoeff
          (FABL.setIndicator
            ↑(FABL.binaryAffineSubspace H
                a))
          γ| =
    1
    The absolute Fourier coefficients of an affine-subspace indicator sum to one.
Proposition3.2.9
Statement uses 4
Statement dependency previews
Preview
Definition 3.2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Lemma 3.2.14
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-3-2fidelity-exact

Proposition 3.12. If A=H+a is an affine subspace of \mathbb F_2^n of codimension k, then \widehat{\mathbf1_A}(\gamma) =\begin{cases} \chi_\gamma(a)2^{-k},&\gamma\in H^\perp,\\ 0,&\gamma\notin H^\perp. \end{cases} Consequently, \varphi_A=\sum_{\gamma\in H^\perp} \chi_\gamma(a)\chi_\gamma. Moreover, \operatorname{sparsity}(\widehat{\mathbf1_A})=2^k, \widehat{\mathbf1_A} is 2^{-k}-granular, and \lVert\widehat{\mathbf1_A}\rVert_\infty=2^{-k}, \qquad \lVert\widehat{\mathbf1_A}\rVert_1=1.

Lean code for Proposition3.2.9●8 theorems
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.setIndicator_binaryAffineSubspace_fourier_expansion {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n) :
  FABL.setIndicator ↑(FABL.binaryAffineSubspace H a) = fun x =>
    FABL.inversePerpendicularCard H *
      FABL.subspaceCharacterSum (FABL.perpendicularSubspace H) (x + a)
    theorem FABL.setIndicator_binaryAffineSubspace_fourier_expansion
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) :
  FABL.setIndicator
      ↑(FABL.binaryAffineSubspace H a) =
    fun x =>
    FABL.inversePerpendicularCard H *
      FABL.subspaceCharacterSum
        (FABL.perpendicularSubspace H)
        (x + a)
    O'Donnell, Proposition 3.12: functional form of the affine indicator expansion.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.vectorFourierCoeff_setIndicator_binaryAffineSubspace_of_mem {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a γ : FABL.F₂Cube n)
  (hγ : γ ∈ FABL.perpendicularSubspace H) :
  FABL.vectorFourierCoeff
      (FABL.setIndicator ↑(FABL.binaryAffineSubspace H a)) γ =
    (FABL.vectorWalshCharacter γ) a * FABL.inversePerpendicularCard H
    theorem FABL.vectorFourierCoeff_setIndicator_binaryAffineSubspace_of_mem
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a γ : FABL.F₂Cube n)
  (hγ :
    γ ∈ FABL.perpendicularSubspace H) :
  FABL.vectorFourierCoeff
      (FABL.setIndicator
        ↑(FABL.binaryAffineSubspace H a))
      γ =
    (FABL.vectorWalshCharacter γ) a *
      FABL.inversePerpendicularCard H
    Proposition 3.12 in coefficient form, on the perpendicular direction.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.vectorFourierCoeff_setIndicator_binaryAffineSubspace_of_not_mem
  {n : ℕ} (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a γ : FABL.F₂Cube n)
  (hγ : γ ∉ FABL.perpendicularSubspace H) :
  FABL.vectorFourierCoeff
      (FABL.setIndicator ↑(FABL.binaryAffineSubspace H a)) γ =
    0
    theorem FABL.vectorFourierCoeff_setIndicator_binaryAffineSubspace_of_not_mem
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a γ : FABL.F₂Cube n)
  (hγ :
    γ ∉ FABL.perpendicularSubspace H) :
  FABL.vectorFourierCoeff
      (FABL.setIndicator
        ↑(FABL.binaryAffineSubspace H a))
      γ =
    0
    Proposition 3.12 in coefficient form, off the perpendicular direction.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.subsetDensity_binaryAffineSubspace_fourier_expansion {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n) :
  (FABL.subsetDensity ↑(FABL.binaryAffineSubspace H a) ⋯).toFun =
    fun x =>
    FABL.subspaceCharacterSum (FABL.perpendicularSubspace H) (x + a)
    theorem FABL.subsetDensity_binaryAffineSubspace_fourier_expansion
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) :
  (FABL.subsetDensity
        ↑(FABL.binaryAffineSubspace H a)
        ⋯).toFun =
    fun x =>
    FABL.subspaceCharacterSum
      (FABL.perpendicularSubspace H)
      (x + a)
    O'Donnell, Proposition 3.12: functional form of the affine-density Fourier expansion.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.spectralSparsity_setIndicator_binaryAffineSubspace {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n) :
  FABL.spectralSparsity
      (FABL.setIndicator ↑(FABL.binaryAffineSubspace H a)) =
    2 ^ FABL.f₂Codimension H
    theorem FABL.spectralSparsity_setIndicator_binaryAffineSubspace
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) :
  FABL.spectralSparsity
      (FABL.setIndicator
        ↑(FABL.binaryAffineSubspace H
            a)) =
    2 ^ FABL.f₂Codimension H
    O'Donnell, Proposition 3.12: an affine subspace of codimension `k` has Fourier sparsity
`2ᵏ`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.isVectorFourierGranular_setIndicator_binaryAffineSubspace {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n) :
  FABL.IsVectorFourierGranular
    (FABL.setIndicator ↑(FABL.binaryAffineSubspace H a))
    (FABL.inversePerpendicularCard H)
    theorem FABL.isVectorFourierGranular_setIndicator_binaryAffineSubspace
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) :
  FABL.IsVectorFourierGranular
    (FABL.setIndicator
      ↑(FABL.binaryAffineSubspace H a))
    (FABL.inversePerpendicularCard H)
    O'Donnell, Proposition 3.12: the affine indicator spectrum is `2⁻ᵏ`-granular.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.spectralInfinityNorm_setIndicator_binaryAffineSubspace {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n) :
  FABL.spectralInfinityNorm
      (FABL.setIndicator ↑(FABL.binaryAffineSubspace H a)) =
    FABL.inversePerpendicularCard H
    theorem FABL.spectralInfinityNorm_setIndicator_binaryAffineSubspace
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) :
  FABL.spectralInfinityNorm
      (FABL.setIndicator
        ↑(FABL.binaryAffineSubspace H
            a)) =
    FABL.inversePerpendicularCard H
    O'Donnell, Proposition 3.12: the Fourier infinity norm of an affine-subspace indicator is
`2⁻ᵏ`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/Subspaces.lean
    complete
    theorem FABL.spectralPNorm_one_setIndicator_binaryAffineSubspace {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (a : FABL.F₂Cube n) :
  FABL.spectralPNorm 1
      (FABL.setIndicator ↑(FABL.binaryAffineSubspace H a)) =
    1
    theorem FABL.spectralPNorm_one_setIndicator_binaryAffineSubspace
  {n : ℕ}
  (H : Submodule FABL.𝔽₂ (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) :
  FABL.spectralPNorm 1
      (FABL.setIndicator
        ↑(FABL.binaryAffineSubspace H
            a)) =
    1
    O'Donnell, Proposition 3.12: the Fourier one-norm of an affine-subspace indicator is one.
Definition3.2.10
uses 0
Used by 4
Reverse dependency previews
Preview
Definition 3.2.11
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-3-2fidelity-exact

Definition 3.13. A decision tree T representing a function f:\mathbb F_2^n\to\mathbb R is a rooted binary tree whose internal nodes are labelled by coordinates i\in[n], whose two outgoing edges at every internal node are labelled 0 and 1, and whose leaves are labelled by real numbers. No coordinate may occur more than once on a root-to-leaf path.

On input x\in\mathbb F_2^n, computation starts at the root. At an internal node labelled i, the tree queries x_i and follows the outgoing edge labelled x_i. The output is the label of the leaf reached. The tree computes f when this output equals f(x) for every input x.

Lean code for Definition3.2.10●7 declarations
  • inductive(2 constructors, 3 parameters)defined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    inductive FABL.F₂DecisionTree.{u_1} (n : ℕ) (α : Type u_1) :
  Finset (Fin n) → Type u_1
    inductive FABL.F₂DecisionTree.{u_1} (n : ℕ)
  (α : Type u_1) :
  Finset (Fin n) → Type u_1
    O'Donnell, Definition 3.13: a binary decision tree whose index records the coordinates still
available for query. Removing the queried coordinate from both child indices enforces that no
coordinate occurs twice on a root-to-leaf path.

    Constructors

    FABL.F₂DecisionTree.leaf.{u_1} {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)} (value : α) :
  FABL.F₂DecisionTree n α available
    A leaf returns its stored value without querying another coordinate. 
    FABL.F₂DecisionTree.query.{u_1} {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)} (coordinate : Fin n)
  (mem_available : coordinate ∈ available)
  (zeroChild oneChild :
    FABL.F₂DecisionTree n α (available.erase coordinate)) :
  FABL.F₂DecisionTree n α available
    Query one available coordinate, then remove it from both child indices.
  • abbrevdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    abbrev FABL.DecisionTree.{u_1} (n : ℕ) (α : Type u_1) : Type u_1
    abbrev FABL.DecisionTree.{u_1} (n : ℕ)
  (α : Type u_1) : Type u_1
    A complete decision tree starts with every coordinate available.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    def FABL.F₂DecisionTree.eval.{u_1} {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)} :
  FABL.F₂DecisionTree n α available → FABL.F₂Cube n → α
    def FABL.F₂DecisionTree.eval.{u_1} {n : ℕ}
  {α : Type u_1}
  {available : Finset (Fin n)} :
  FABL.F₂DecisionTree n α available →
    FABL.F₂Cube n → α
    Execute a decision tree on a binary-cube input.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    def FABL.F₂DecisionTree.Computes.{u_1} {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)} (T : FABL.F₂DecisionTree n α available)
  (f : FABL.F₂Cube n → α) : Prop
    def FABL.F₂DecisionTree.Computes.{u_1} {n : ℕ}
  {α : Type u_1}
  {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available)
  (f : FABL.F₂Cube n → α) : Prop
    A tree computes `f` when execution agrees with `f` on every input.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.computes_iff.{u_1} {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)} (T : FABL.F₂DecisionTree n α available)
  (f : FABL.F₂Cube n → α) :
  T.Computes f ↔ ∀ (x : FABL.F₂Cube n), T.eval x = f x
    theorem FABL.F₂DecisionTree.computes_iff.{u_1}
  {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available)
  (f : FABL.F₂Cube n → α) :
  T.Computes f ↔
    ∀ (x : FABL.F₂Cube n), T.eval x = f x
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    def FABL.F₂DecisionTree.completeTree.{u_1} {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α) : FABL.DecisionTree n α
    def FABL.F₂DecisionTree.completeTree.{u_1}
  {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α) :
  FABL.DecisionTree n α
    Canonical complete decision tree representing a function on the binary cube.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.completeTree_computes.{u_1} {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α) :
  FABL.F₂DecisionTree.Computes (FABL.F₂DecisionTree.completeTree f) f
    theorem FABL.F₂DecisionTree.completeTree_computes.{u_1}
  {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α) :
  FABL.F₂DecisionTree.Computes
    (FABL.F₂DecisionTree.completeTree f) f
    Every function on the finite binary cube is represented by the complete decision tree.
Definition3.2.11
uses 1
Used by 3
Reverse dependency previews
Preview
Lemma 3.2.12
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-3-2fidelity-exact

Definition 3.14. The size s of a decision tree T is its number of leaves. Its depth k is the maximum length of a root-to-leaf path. For decision trees over \mathbb F_2^n, k\le n, \qquad s\le2^k. For f:\mathbb F_2^n\to\mathbb R, write \operatorname{DT}(f) for the least depth and \operatorname{DT}_{\mathrm{size}}(f) for the least size of a decision tree computing f. The two quantities are optimized independently, and each minimum has its own attaining tree.

Lean code for Definition3.2.11●10 declarations
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    def FABL.F₂DecisionTree.leafCount.{u_1} {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)} : FABL.F₂DecisionTree n α available → ℕ
    def FABL.F₂DecisionTree.leafCount.{u_1}
  {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)} :
  FABL.F₂DecisionTree n α available → ℕ
    O'Donnell, Definition 3.14: the number of leaves.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    def FABL.F₂DecisionTree.depth.{u_1} {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)} : FABL.F₂DecisionTree n α available → ℕ
    def FABL.F₂DecisionTree.depth.{u_1} {n : ℕ}
  {α : Type u_1}
  {available : Finset (Fin n)} :
  FABL.F₂DecisionTree n α available → ℕ
    O'Donnell, Definition 3.14: maximum root-to-leaf path length.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.depth_le_dimension.{u_1} {n : ℕ} {α : Type u_1}
  (T : FABL.DecisionTree n α) : FABL.F₂DecisionTree.depth T ≤ n
    theorem FABL.F₂DecisionTree.depth_le_dimension.{u_1}
  {n : ℕ} {α : Type u_1}
  (T : FABL.DecisionTree n α) :
  FABL.F₂DecisionTree.depth T ≤ n
    Every decision tree over `n` coordinates has depth at most `n`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.leafCount_le_two_pow_depth.{u_1} {n : ℕ}
  {α : Type u_1} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available) : T.leafCount ≤ 2 ^ T.depth
    theorem FABL.F₂DecisionTree.leafCount_le_two_pow_depth.{u_1}
  {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)}
  (T :
    FABL.F₂DecisionTree n α available) :
  T.leafCount ≤ 2 ^ T.depth
    A binary tree of depth `k` has at most `2ᵏ` leaves.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    def FABL.F₂DecisionTree.decisionTreeDepth.{u_1} {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α) : ℕ
    def FABL.F₂DecisionTree.decisionTreeDepth.{u_1}
  {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α) : ℕ
    O'Donnell, Definition 3.14: the least depth of a decision tree computing `f`.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    def FABL.F₂DecisionTree.decisionTreeSize.{u_1} {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α) : ℕ
    def FABL.F₂DecisionTree.decisionTreeSize.{u_1}
  {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α) : ℕ
    O'Donnell, Definition 3.14: the least number of leaves of a decision tree computing `f`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.exists_computingTree_depth_eq_decisionTreeDepth.{u_1}
  {n : ℕ} {α : Type u_1} (f : FABL.F₂Cube n → α) :
  ∃ T,
    FABL.F₂DecisionTree.Computes T f ∧
      FABL.F₂DecisionTree.depth T =
        FABL.F₂DecisionTree.decisionTreeDepth f
    theorem FABL.F₂DecisionTree.exists_computingTree_depth_eq_decisionTreeDepth.{u_1}
  {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α) :
  ∃ T,
    FABL.F₂DecisionTree.Computes T f ∧
      FABL.F₂DecisionTree.depth T =
        FABL.F₂DecisionTree.decisionTreeDepth
          f
    A depth-optimal decision tree exists.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.exists_computingTree_leafCount_eq_decisionTreeSize.{u_1}
  {n : ℕ} {α : Type u_1} (f : FABL.F₂Cube n → α) :
  ∃ T,
    FABL.F₂DecisionTree.Computes T f ∧
      FABL.F₂DecisionTree.leafCount T =
        FABL.F₂DecisionTree.decisionTreeSize f
    theorem FABL.F₂DecisionTree.exists_computingTree_leafCount_eq_decisionTreeSize.{u_1}
  {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α) :
  ∃ T,
    FABL.F₂DecisionTree.Computes T f ∧
      FABL.F₂DecisionTree.leafCount T =
        FABL.F₂DecisionTree.decisionTreeSize
          f
    A size-optimal decision tree exists.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.decisionTreeDepth_le_of_computes.{u_1} {n : ℕ}
  {α : Type u_1} (f : FABL.F₂Cube n → α) (T : FABL.DecisionTree n α)
  (hT : FABL.F₂DecisionTree.Computes T f) :
  FABL.F₂DecisionTree.decisionTreeDepth f ≤ FABL.F₂DecisionTree.depth T
    theorem FABL.F₂DecisionTree.decisionTreeDepth_le_of_computes.{u_1}
  {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α)
  (T : FABL.DecisionTree n α)
  (hT :
    FABL.F₂DecisionTree.Computes T f) :
  FABL.F₂DecisionTree.decisionTreeDepth
      f ≤
    FABL.F₂DecisionTree.depth T
    `decisionTreeDepth` is no larger than the depth of any computing tree.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.decisionTreeSize_le_of_computes.{u_1} {n : ℕ}
  {α : Type u_1} (f : FABL.F₂Cube n → α) (T : FABL.DecisionTree n α)
  (hT : FABL.F₂DecisionTree.Computes T f) :
  FABL.F₂DecisionTree.decisionTreeSize f ≤
    FABL.F₂DecisionTree.leafCount T
    theorem FABL.F₂DecisionTree.decisionTreeSize_le_of_computes.{u_1}
  {n : ℕ} {α : Type u_1}
  (f : FABL.F₂Cube n → α)
  (T : FABL.DecisionTree n α)
  (hT :
    FABL.F₂DecisionTree.Computes T f) :
  FABL.F₂DecisionTree.decisionTreeSize f ≤
    FABL.F₂DecisionTree.leafCount T
    `decisionTreeSize` is no larger than the size of any computing tree.
Lemma3.2.12
Statement uses 3
Statement dependency previews
Preview
Lemma 3.2.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-3-2supportfidelity-exact

Path subcubes of a decision tree. Let T compute f:\mathbb F_2^n\to\mathbb R, and let P be a root-to-leaf path. The set C_P of inputs following P is a subcube whose codimension is the length of P. The function f is constant on C_P; denote this value by f(P). Every input follows exactly one path, so \{C_P:P\text{ is a root-to-leaf path of }T\} is a partition of \mathbb F_2^n.

Lean code for Lemma3.2.12●12 declarations
  • structure(2 fields)defined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    structure FABL.F₂DecisionTree.Path.{u_2} (n : ℕ) (α : Type u_2) : Type u_2
    structure FABL.F₂DecisionTree.Path.{u_2} (n : ℕ)
  (α : Type u_2) : Type u_2
    A root-to-leaf path records the queried partial assignment and the leaf label.

    Fields

    assignment : Fin n → Option FABL.𝔽₂
    The branch value fixed at each queried coordinate. 
    output : α
    The label at the terminal leaf.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    def FABL.F₂DecisionTree.Path.support.{u_1} {n : ℕ} {α : Type u_1}
  (path : FABL.F₂DecisionTree.Path n α) : Finset (Fin n)
    def FABL.F₂DecisionTree.Path.support.{u_1}
  {n : ℕ} {α : Type u_1}
  (path : FABL.F₂DecisionTree.Path n α) :
  Finset (Fin n)
    Coordinates queried along a path.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    def FABL.F₂DecisionTree.Path.length.{u_1} {n : ℕ} {α : Type u_1}
  (path : FABL.F₂DecisionTree.Path n α) : ℕ
    def FABL.F₂DecisionTree.Path.length.{u_1}
  {n : ℕ} {α : Type u_1}
  (path : FABL.F₂DecisionTree.Path n α) :
  ℕ
    Root-to-leaf path length.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    def FABL.F₂DecisionTree.Path.Matches.{u_1} {n : ℕ} {α : Type u_1}
  (path : FABL.F₂DecisionTree.Path n α) (x : FABL.F₂Cube n) : Prop
    def FABL.F₂DecisionTree.Path.Matches.{u_1}
  {n : ℕ} {α : Type u_1}
  (path : FABL.F₂DecisionTree.Path n α)
  (x : FABL.F₂Cube n) : Prop
    An input follows a path when it has every queried branch value.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    def FABL.F₂DecisionTree.Path.cylinder.{u_1} {n : ℕ} {α : Type u_1}
  (path : FABL.F₂DecisionTree.Path n α) : Set (FABL.F₂Cube n)
    def FABL.F₂DecisionTree.Path.cylinder.{u_1}
  {n : ℕ} {α : Type u_1}
  (path : FABL.F₂DecisionTree.Path n α) :
  Set (FABL.F₂Cube n)
    The subcube of inputs following a root-to-leaf path.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    def FABL.F₂DecisionTree.paths.{u_1} {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)} :
  FABL.F₂DecisionTree n α available →
    List (FABL.F₂DecisionTree.Path n α)
    def FABL.F₂DecisionTree.paths.{u_1} {n : ℕ}
  {α : Type u_1}
  {available : Finset (Fin n)} :
  FABL.F₂DecisionTree n α available →
    List (FABL.F₂DecisionTree.Path n α)
    The finite list of root-to-leaf paths of a decision tree.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.path_length_le_depth.{u_1} {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)} (T : FABL.F₂DecisionTree n α available)
  (path : FABL.F₂DecisionTree.Path n α) (hpath : path ∈ T.paths) :
  path.length ≤ T.depth
    theorem FABL.F₂DecisionTree.path_length_le_depth.{u_1}
  {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available)
  (path : FABL.F₂DecisionTree.Path n α)
  (hpath : path ∈ T.paths) :
  path.length ≤ T.depth
    Every root-to-leaf path length is bounded by the tree depth.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.length_paths_eq_leafCount.{u_1} {n : ℕ}
  {α : Type u_1} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available) : T.paths.length = T.leafCount
    theorem FABL.F₂DecisionTree.length_paths_eq_leafCount.{u_1}
  {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)}
  (T :
    FABL.F₂DecisionTree n α available) :
  T.paths.length = T.leafCount
    The number of enumerated paths is the number of leaves.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.existsUnique_path_mem_and_matches.{u_1} {n : ℕ}
  {α : Type u_1} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available) (x : FABL.F₂Cube n) :
  ∃! path, path ∈ T.paths ∧ path.Matches x
    theorem FABL.F₂DecisionTree.existsUnique_path_mem_and_matches.{u_1}
  {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available)
  (x : FABL.F₂Cube n) :
  ∃! path, path ∈ T.paths ∧ path.Matches x
    The path subcubes form a partition: every input follows exactly one listed path.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.Path.cylinder_eq_coordinateSubcube.{u_1} {n : ℕ}
  {α : Type u_1} (path : FABL.F₂DecisionTree.Path n α) :
  path.cylinder =
    FABL.F₂DecisionTree.coordinateSubcube path.support path.base
    theorem FABL.F₂DecisionTree.Path.cylinder_eq_coordinateSubcube.{u_1}
  {n : ℕ} {α : Type u_1}
  (path : FABL.F₂DecisionTree.Path n α) :
  path.cylinder =
    FABL.F₂DecisionTree.coordinateSubcube
      path.support path.base
    A path cylinder is the coordinate subcube specified by its partial assignment.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.Path.codimension_coordinateZeroSubspace_eq_length.{u_1}
  {n : ℕ} {α : Type u_1} (path : FABL.F₂DecisionTree.Path n α) :
  FABL.f₂Codimension
      (FABL.F₂DecisionTree.coordinateZeroSubspace path.support) =
    path.length
    theorem FABL.F₂DecisionTree.Path.codimension_coordinateZeroSubspace_eq_length.{u_1}
  {n : ℕ} {α : Type u_1}
  (path : FABL.F₂DecisionTree.Path n α) :
  FABL.f₂Codimension
      (FABL.F₂DecisionTree.coordinateZeroSubspace
        path.support) =
    path.length
    A path subcube has codimension equal to its root-to-leaf path length.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.computes_eq_path_output_of_matches.{u_1} {n : ℕ}
  {α : Type u_1} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available) (f : FABL.F₂Cube n → α)
  (hT : T.Computes f) (path : FABL.F₂DecisionTree.Path n α)
  (hpath : path ∈ T.paths) (x : FABL.F₂Cube n)
  (hmatches : path.Matches x) : f x = path.output
    theorem FABL.F₂DecisionTree.computes_eq_path_output_of_matches.{u_1}
  {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available)
  (f : FABL.F₂Cube n → α)
  (hT : T.Computes f)
  (path : FABL.F₂DecisionTree.Path n α)
  (hpath : path ∈ T.paths)
  (x : FABL.F₂Cube n)
  (hmatches : path.Matches x) :
  f x = path.output
    If `T` computes `f`, then `f` is constant on every path subcube, with the leaf label as its
value.
Lemma3.2.13
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 3.2.14
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-3-2fidelity-exact

Fact 3.15. If f:\mathbb F_2^n\to\mathbb R is computed by a decision tree T, then f=\sum_{\text{paths }P\text{ of }T}f(P)\mathbf1_{C_P}.

Lean code for Lemma3.2.13●3 declarations
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    def FABL.F₂DecisionTree.pathExpansion {n : ℕ}
  (pathList : List (FABL.F₂DecisionTree.Path n ℝ)) : FABL.F₂Cube n → ℝ
    def FABL.F₂DecisionTree.pathExpansion {n : ℕ}
  (pathList :
    List (FABL.F₂DecisionTree.Path n ℝ)) :
  FABL.F₂Cube n → ℝ
    The linear combination of path-subcube indicators with their leaf labels.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.eval_eq_pathExpansion {n : ℕ}
  {available : Finset (Fin n)} (T : FABL.F₂DecisionTree n ℝ available) :
  T.eval = FABL.F₂DecisionTree.pathExpansion T.paths
    theorem FABL.F₂DecisionTree.eval_eq_pathExpansion
  {n : ℕ} {available : Finset (Fin n)}
  (T :
    FABL.F₂DecisionTree n ℝ available) :
  T.eval =
    FABL.F₂DecisionTree.pathExpansion
      T.paths
    Fact 3.15 expressed using the reusable path-expansion function.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.computes_eq_pathExpansion {n : ℕ}
  {available : Finset (Fin n)} (T : FABL.F₂DecisionTree n ℝ available)
  (f : FABL.F₂Cube n → ℝ) (hT : T.Computes f) :
  f = FABL.F₂DecisionTree.pathExpansion T.paths
    theorem FABL.F₂DecisionTree.computes_eq_pathExpansion
  {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  (f : FABL.F₂Cube n → ℝ)
  (hT : T.Computes f) :
  f =
    FABL.F₂DecisionTree.pathExpansion
      T.paths
    Fact 3.15 for a function represented by a decision tree.
Lemma3.2.14
Statement uses 5
Statement dependency previews
Preview
Definition 3.2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-3-2supportfidelity-exact

Exercise 3.21. Let f:\mathbb F_2^n\to\mathbb R be computed by a decision tree of size s and depth k. Using the path-subcube expansion, prove \deg(f)\le k, \qquad \operatorname{sparsity}(\widehat f)\le s2^k\le4^k, and \lVert\widehat f\rVert_1 \le\lVert f\rVert_\infty s \le\lVert f\rVert_\infty2^k. If f:\mathbb F_2^n\to\mathbb Z, also prove that \widehat f is 2^{-k}-granular.

Lean code for Lemma3.2.14●10 theorems
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.Path.indicator_eq_binaryAffineSubspace.{u_1} {n : ℕ}
  {α : Type u_1} (path : FABL.F₂DecisionTree.Path n α) :
  path.indicator =
    FABL.setIndicator
      ↑(FABL.binaryAffineSubspace
          (FABL.F₂DecisionTree.coordinateZeroSubspace path.support)
          path.base)
    theorem FABL.F₂DecisionTree.Path.indicator_eq_binaryAffineSubspace.{u_1}
  {n : ℕ} {α : Type u_1}
  (path : FABL.F₂DecisionTree.Path n α) :
  path.indicator =
    FABL.setIndicator
      ↑(FABL.binaryAffineSubspace
          (FABL.F₂DecisionTree.coordinateZeroSubspace
            path.support)
          path.base)
    The path indicator is definitionally the indicator of its affine coordinate subcube.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.Path.spectralSparsity_indicator.{u_1} {n : ℕ}
  {α : Type u_1} (path : FABL.F₂DecisionTree.Path n α) :
  FABL.spectralSparsity path.indicator = 2 ^ path.length
    theorem FABL.F₂DecisionTree.Path.spectralSparsity_indicator.{u_1}
  {n : ℕ} {α : Type u_1}
  (path : FABL.F₂DecisionTree.Path n α) :
  FABL.spectralSparsity path.indicator =
    2 ^ path.length
    A path indicator has Fourier sparsity `2` raised to its path length.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.Path.spectralPNorm_one_indicator.{u_1} {n : ℕ}
  {α : Type u_1} (path : FABL.F₂DecisionTree.Path n α) :
  FABL.spectralPNorm 1 path.indicator = 1
    theorem FABL.F₂DecisionTree.Path.spectralPNorm_one_indicator.{u_1}
  {n : ℕ} {α : Type u_1}
  (path : FABL.F₂DecisionTree.Path n α) :
  FABL.spectralPNorm 1 path.indicator = 1
    The Fourier one-norm of a path indicator is one.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.Path.isVectorFourierGranular_indicator.{u_1} {n : ℕ}
  {α : Type u_1} (path : FABL.F₂DecisionTree.Path n α) :
  FABL.IsVectorFourierGranular path.indicator path.inversePathSize
    theorem FABL.F₂DecisionTree.Path.isVectorFourierGranular_indicator.{u_1}
  {n : ℕ} {α : Type u_1}
  (path : FABL.F₂DecisionTree.Path n α) :
  FABL.IsVectorFourierGranular
    path.indicator path.inversePathSize
    A path indicator is granular at the scale determined by its length.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.Path.vectorFourierDegree_indicator_le_length.{u_1}
  {n : ℕ} {α : Type u_1} (path : FABL.F₂DecisionTree.Path n α) :
  FABL.vectorFourierDegree path.indicator ≤ path.length
    theorem FABL.F₂DecisionTree.Path.vectorFourierDegree_indicator_le_length.{u_1}
  {n : ℕ} {α : Type u_1}
  (path : FABL.F₂DecisionTree.Path n α) :
  FABL.vectorFourierDegree
      path.indicator ≤
    path.length
    A path-subcube indicator has Fourier degree at most the path length.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.vectorFourierCoeff_pathExpansion {n : ℕ}
  (pathList : List (FABL.F₂DecisionTree.Path n ℝ))
  (gamma : FABL.F₂Cube n) :
  FABL.vectorFourierCoeff (FABL.F₂DecisionTree.pathExpansion pathList)
      gamma =
    (List.map
        (fun path =>
          path.output * FABL.vectorFourierCoeff path.indicator gamma)
        pathList).sum
    theorem FABL.F₂DecisionTree.vectorFourierCoeff_pathExpansion
  {n : ℕ}
  (pathList :
    List (FABL.F₂DecisionTree.Path n ℝ))
  (gamma : FABL.F₂Cube n) :
  FABL.vectorFourierCoeff
      (FABL.F₂DecisionTree.pathExpansion
        pathList)
      gamma =
    (List.map
        (fun path =>
          path.output *
            FABL.vectorFourierCoeff
              path.indicator gamma)
        pathList).sum
    Fourier coefficients of a path expansion are the corresponding finite linear combination.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.vectorFourierDegree_pathExpansion_le {n : ℕ}
  (pathList : List (FABL.F₂DecisionTree.Path n ℝ)) (k : ℕ)
  (hlength : ∀ path ∈ pathList, path.length ≤ k) :
  FABL.vectorFourierDegree
      (FABL.F₂DecisionTree.pathExpansion pathList) ≤
    k
    theorem FABL.F₂DecisionTree.vectorFourierDegree_pathExpansion_le
  {n : ℕ}
  (pathList :
    List (FABL.F₂DecisionTree.Path n ℝ))
  (k : ℕ)
  (hlength :
    ∀ path ∈ pathList, path.length ≤ k) :
  FABL.vectorFourierDegree
      (FABL.F₂DecisionTree.pathExpansion
        pathList) ≤
    k
    A sum of path indicators of length at most `k` has Fourier degree at most `k`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.spectralSparsity_pathExpansion_le_sum {n : ℕ}
  (pathList : List (FABL.F₂DecisionTree.Path n ℝ)) :
  FABL.spectralSparsity (FABL.F₂DecisionTree.pathExpansion pathList) ≤
    (List.map (fun path => 2 ^ path.length) pathList).sum
    theorem FABL.F₂DecisionTree.spectralSparsity_pathExpansion_le_sum
  {n : ℕ}
  (pathList :
    List (FABL.F₂DecisionTree.Path n ℝ)) :
  FABL.spectralSparsity
      (FABL.F₂DecisionTree.pathExpansion
        pathList) ≤
    (List.map
        (fun path => 2 ^ path.length)
        pathList).sum
    The sparsity of a path expansion is bounded by the sum of the sparsities of its path
indicators.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.spectralPNorm_one_pathExpansion_le_sum_abs_output
  {n : ℕ} (pathList : List (FABL.F₂DecisionTree.Path n ℝ)) :
  FABL.spectralPNorm 1 (FABL.F₂DecisionTree.pathExpansion pathList) ≤
    (List.map (fun path => |path.output|) pathList).sum
    theorem FABL.F₂DecisionTree.spectralPNorm_one_pathExpansion_le_sum_abs_output
  {n : ℕ}
  (pathList :
    List (FABL.F₂DecisionTree.Path n ℝ)) :
  FABL.spectralPNorm 1
      (FABL.F₂DecisionTree.pathExpansion
        pathList) ≤
    (List.map (fun path => |path.output|)
        pathList).sum
    The Fourier one-norm of a path expansion is bounded by the sum of the absolute leaf
labels.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.isVectorFourierGranular_pathExpansion {n : ℕ}
  (pathList : List (FABL.F₂DecisionTree.Path n ℝ)) (k : ℕ)
  (hlength : ∀ path ∈ pathList, path.length ≤ k)
  (hinteger : ∀ path ∈ pathList, ∃ z, path.output = ↑z) :
  FABL.IsVectorFourierGranular
    (FABL.F₂DecisionTree.pathExpansion pathList) (2 ^ k)⁻¹
    theorem FABL.F₂DecisionTree.isVectorFourierGranular_pathExpansion
  {n : ℕ}
  (pathList :
    List (FABL.F₂DecisionTree.Path n ℝ))
  (k : ℕ)
  (hlength :
    ∀ path ∈ pathList, path.length ≤ k)
  (hinteger :
    ∀ path ∈ pathList,
      ∃ z, path.output = ↑z) :
  FABL.IsVectorFourierGranular
    (FABL.F₂DecisionTree.pathExpansion
      pathList)
    (2 ^ k)⁻¹
    A path expansion with integer leaf labels and path length at most `k` is `2⁻ᵏ`-granular.
Proposition3.2.15
Statement uses 4
Statement dependency previews
Preview
Proposition 3.2.9
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Lemma 3.2.16
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-3-2fidelity-exact

Proposition 3.16. Let f:\mathbb F_2^n\to\mathbb R be computed by a decision tree T of size s and depth k. Then

  • \deg(f)\le k;

  • \operatorname{sparsity}(\widehat f)\le s2^k\le4^k;

  • \lVert\widehat f\rVert_1 \le\lVert f\rVert_\infty s \le\lVert f\rVert_\infty2^k;

  • if f:\mathbb F_2^n\to\mathbb Z, then \widehat f is 2^{-k}-granular.

Lean code for Proposition3.2.15●5 theorems
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.vectorFourierDegree_le_depth_of_computes {n : ℕ}
  {available : Finset (Fin n)} (T : FABL.F₂DecisionTree n ℝ available)
  (f : FABL.F₂Cube n → ℝ) (hT : T.Computes f) :
  FABL.vectorFourierDegree f ≤ T.depth
    theorem FABL.F₂DecisionTree.vectorFourierDegree_le_depth_of_computes
  {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  (f : FABL.F₂Cube n → ℝ)
  (hT : T.Computes f) :
  FABL.vectorFourierDegree f ≤ T.depth
    Exercise 3.21: a function computed by a tree has degree at most that tree's depth.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.spectralSparsity_le_of_computes {n : ℕ}
  {available : Finset (Fin n)} (T : FABL.F₂DecisionTree n ℝ available)
  (f : FABL.F₂Cube n → ℝ) (hT : T.Computes f) :
  FABL.spectralSparsity f ≤ T.leafCount * 2 ^ T.depth ∧
    FABL.spectralSparsity f ≤ 4 ^ T.depth
    theorem FABL.F₂DecisionTree.spectralSparsity_le_of_computes
  {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  (f : FABL.F₂Cube n → ℝ)
  (hT : T.Computes f) :
  FABL.spectralSparsity f ≤
      T.leafCount * 2 ^ T.depth ∧
    FABL.spectralSparsity f ≤ 4 ^ T.depth
    Exercise 3.21 spectral-sparsity bounds for a represented function.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.spectralPNorm_one_le_infinityNorm_mul_leafCount_of_computes
  {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available) (f : FABL.F₂Cube n → ℝ)
  (hT : T.Computes f) :
  FABL.spectralPNorm 1 f ≤
    FABL.binaryFunctionInfinityNorm f * ↑T.leafCount
    theorem FABL.F₂DecisionTree.spectralPNorm_one_le_infinityNorm_mul_leafCount_of_computes
  {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  (f : FABL.F₂Cube n → ℝ)
  (hT : T.Computes f) :
  FABL.spectralPNorm 1 f ≤
    FABL.binaryFunctionInfinityNorm f *
      ↑T.leafCount
    Exercise 3.21: the Fourier one-norm is at most the infinity norm times tree size.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.spectralPNorm_one_le_infinityNorm_mul_two_pow_depth_of_computes
  {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available) (f : FABL.F₂Cube n → ℝ)
  (hT : T.Computes f) :
  FABL.spectralPNorm 1 f ≤
    FABL.binaryFunctionInfinityNorm f * ↑(2 ^ T.depth)
    theorem FABL.F₂DecisionTree.spectralPNorm_one_le_infinityNorm_mul_two_pow_depth_of_computes
  {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  (f : FABL.F₂Cube n → ℝ)
  (hT : T.Computes f) :
  FABL.spectralPNorm 1 f ≤
    FABL.binaryFunctionInfinityNorm f *
      ↑(2 ^ T.depth)
    Exercise 3.21: replacing size by `2^depth` in the Fourier one-norm bound.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.isVectorFourierGranular_inverseTwoPowDepth_of_computes_int
  {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available) (f : FABL.F₂Cube n → ℤ)
  (hT : T.Computes fun x => ↑(f x)) :
  FABL.IsVectorFourierGranular (fun x => ↑(f x)) (2 ^ T.depth)⁻¹
    theorem FABL.F₂DecisionTree.isVectorFourierGranular_inverseTwoPowDepth_of_computes_int
  {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  (f : FABL.F₂Cube n → ℤ)
  (hT : T.Computes fun x => ↑(f x)) :
  FABL.IsVectorFourierGranular
    (fun x => ↑(f x)) (2 ^ T.depth)⁻¹
    Exercise 3.21: an integer-valued function computed by a depth-`k` tree has a
`2⁻ᵏ`-granular Fourier transform.
Lemma3.2.16
Statement uses 3
Statement dependency previews
Preview
Definition 3.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-3-2supportfidelity-log-base-two-and-ceiling-explicit

Exercise 3.22. Let f:\mathbb F_2^n\to\{-1,1\} be computed by a decision tree T of size s, and let \epsilon\in(0,1]. Truncate every path, if necessary, so that its length is at most k=\left\lceil\log_2(s/\epsilon)\right\rceil, creating new leaves labelled -1 or 1 as necessary. Show that the resulting decision tree T' computes a function \epsilon-close to f; that is, \Pr_{\boldsymbol x\sim\mathbb F_2^n} [T'(\boldsymbol x)\ne f(\boldsymbol x)]\le\epsilon. The Hamming-distance conclusion holds for any choice of the new sign labels. For the Fourier-tail estimate used in Proposition 3.17, the production proof separately truncates the real-valued tree with new leaves labelled 0 and applies Parseval to its squared approximation error. The book writes \log(s/\epsilon) and suppresses the integer rounding; the displayed base-two ceiling is the exact convention used by the Lean declaration.

Lean code for Lemma3.2.16●9 declarations
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    def FABL.F₂DecisionTree.truncate.{u_1} {n : ℕ} {α : Type u_1} (fallback : α)
  {available : Finset (Fin n)} :
  FABL.F₂DecisionTree n α available →
    ℕ → FABL.F₂DecisionTree n α available
    def FABL.F₂DecisionTree.truncate.{u_1} {n : ℕ}
  {α : Type u_1} (fallback : α)
  {available : Finset (Fin n)} :
  FABL.F₂DecisionTree n α available →
    ℕ → FABL.F₂DecisionTree n α available
    Truncate every root-to-leaf computation after at most `k` queries, labeling each newly
created leaf by `fallback`. Existing leaves are preserved.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.depth_truncate_le.{u_1} {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)} (T : FABL.F₂DecisionTree n α available)
  (fallback : α) (k : ℕ) :
  (FABL.F₂DecisionTree.truncate fallback T k).depth ≤ k
    theorem FABL.F₂DecisionTree.depth_truncate_le.{u_1}
  {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available)
  (fallback : α) (k : ℕ) :
  (FABL.F₂DecisionTree.truncate fallback T
        k).depth ≤
    k
    A depth-`k` truncation has depth at most `k`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTrees.lean
    complete
    theorem FABL.F₂DecisionTree.exists_long_path_of_eval_truncate_ne.{u_1} {n : ℕ}
  {α : Type u_1} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available) (fallback : α) (k : ℕ)
  (x : FABL.F₂Cube n)
  (hne :
    (FABL.F₂DecisionTree.truncate fallback T k).eval x ≠ T.eval x) :
  ∃ path ∈ T.paths, path.Matches x ∧ k < path.length
    theorem FABL.F₂DecisionTree.exists_long_path_of_eval_truncate_ne.{u_1}
  {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available)
  (fallback : α) (k : ℕ)
  (x : FABL.F₂Cube n)
  (hne :
    (FABL.F₂DecisionTree.truncate fallback
            T k).eval
        x ≠
      T.eval x) :
  ∃ path ∈ T.paths,
    path.Matches x ∧ k < path.length
    If truncation changes the value at an input, that input follows an original path longer
than the truncation depth.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    def FABL.F₂DecisionTree.longPathIndicatorSum.{u_1} {n : ℕ} {α : Type u_1}
  (pathList : List (FABL.F₂DecisionTree.Path n α)) (k : ℕ) :
  FABL.F₂Cube n → ℝ
    def FABL.F₂DecisionTree.longPathIndicatorSum.{u_1}
  {n : ℕ} {α : Type u_1}
  (pathList :
    List (FABL.F₂DecisionTree.Path n α))
  (k : ℕ) : FABL.F₂Cube n → ℝ
    Sum of the indicators of paths whose length is strictly larger than `k`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.relativeHammingDist_eval_truncate_le.{u_1} {n : ℕ}
  {α : Type u_1} [DecidableEq α] {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available) (fallback : α) (k : ℕ) :
  FABL.relativeHammingDist T.eval
      (FABL.F₂DecisionTree.truncate fallback T k).eval ≤
    ↑T.leafCount * (2 ^ k)⁻¹
    theorem FABL.F₂DecisionTree.relativeHammingDist_eval_truncate_le.{u_1}
  {n : ℕ} {α : Type u_1} [DecidableEq α]
  {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available)
  (fallback : α) (k : ℕ) :
  FABL.relativeHammingDist T.eval
      (FABL.F₂DecisionTree.truncate
          fallback T k).eval ≤
    ↑T.leafCount * (2 ^ k)⁻¹
    Union-bound form of Exercise 3.22: depth-`k` truncation changes the original function on at
most `s 2⁻ᵏ` of the cube, independently of the chosen fallback label.
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    def FABL.F₂DecisionTree.decisionTreeTruncationDegree (s : ℕ) (ε : ℝ) : ℕ
    def FABL.F₂DecisionTree.decisionTreeTruncationDegree
  (s : ℕ) (ε : ℝ) : ℕ
    Explicit base-two cutoff `⌈log₂(s / ε)⌉`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.mul_inverseTwoPow_decisionTreeTruncationDegree_le
  (s : ℕ) {ε : ℝ} (hs : 0 < s) (hε : 0 < ε) :
  ↑s * (2 ^ FABL.F₂DecisionTree.decisionTreeTruncationDegree s ε)⁻¹ ≤ ε
    theorem FABL.F₂DecisionTree.mul_inverseTwoPow_decisionTreeTruncationDegree_le
  (s : ℕ) {ε : ℝ} (hs : 0 < s)
  (hε : 0 < ε) :
  ↑s *
      (2 ^
          FABL.F₂DecisionTree.decisionTreeTruncationDegree
            s ε)⁻¹ ≤
    ε
    The explicit cutoff satisfies `s 2⁻ᵏ ≤ ε`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.relativeHammingDist_eval_truncate_decisionTreeTruncationDegree_le.{u_1}
  {n : ℕ} {α : Type u_1} [DecidableEq α] {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available) (fallback : α) {ε : ℝ}
  (hε : 0 < ε) :
  FABL.relativeHammingDist T.eval
      (FABL.F₂DecisionTree.truncate fallback T
          (FABL.F₂DecisionTree.decisionTreeTruncationDegree T.leafCount
            ε)).eval ≤
    ε
    theorem FABL.F₂DecisionTree.relativeHammingDist_eval_truncate_decisionTreeTruncationDegree_le.{u_1}
  {n : ℕ} {α : Type u_1} [DecidableEq α]
  {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n α available)
  (fallback : α) {ε : ℝ} (hε : 0 < ε) :
  FABL.relativeHammingDist T.eval
      (FABL.F₂DecisionTree.truncate
          fallback T
          (FABL.F₂DecisionTree.decisionTreeTruncationDegree
            T.leafCount ε)).eval ≤
    ε
    Exercise 3.22 with its explicit cutoff: arbitrary fallback labels give an `ε`-close
truncation.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.exists_truncatedTree_close.{u_1} {n : ℕ}
  {α : Type u_1} {available : Finset (Fin n)} [DecidableEq α]
  (T : FABL.F₂DecisionTree n α available) (fallback : α) {ε : ℝ}
  (hε : 0 < ε) :
  ∃ T',
    T'.depth ≤
        FABL.F₂DecisionTree.decisionTreeTruncationDegree T.leafCount ε ∧
      FABL.relativeHammingDist T.eval T'.eval ≤ ε
    theorem FABL.F₂DecisionTree.exists_truncatedTree_close.{u_1}
  {n : ℕ} {α : Type u_1}
  {available : Finset (Fin n)}
  [DecidableEq α]
  (T : FABL.F₂DecisionTree n α available)
  (fallback : α) {ε : ℝ} (hε : 0 < ε) :
  ∃ T',
    T'.depth ≤
        FABL.F₂DecisionTree.decisionTreeTruncationDegree
          T.leafCount ε ∧
      FABL.relativeHammingDist T.eval
          T'.eval ≤
        ε
    Exercise 3.22 in existential form, including the depth guarantee on the truncated tree.
Proposition3.2.17
Statement uses 4
Statement dependency previews
Preview
Theorem 1.4.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-3-2fidelity-log-base-two-and-ceiling-explicit

Proposition 3.17. Let f:\mathbb F_2^n\to\{-1,1\} be computable by a decision tree of size s, and let \epsilon\in(0,1]. Then the Fourier spectrum of f is \epsilon-concentrated on degree up to the explicit integer cutoff k=\left\lceil\log_2(s/\epsilon)\right\rceil. Equivalently, \sum_{\substack{\gamma\in\widehat{\mathbb F_2^n}\\ |\gamma|>k}} \widehat f(\gamma)^2 \le\epsilon, where |\gamma| is the Hamming weight of \gamma. This makes explicit the base-two logarithm and ceiling convention suppressed in the book's phrase “degree up to \log(s/\epsilon)”.

Lean code for Proposition3.2.17●5 declarations
  • defdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    def FABL.F₂DecisionTree.vectorFourierWeightAbove {n : ℕ} (k : ℕ)
  (f : FABL.F₂Cube n → ℝ) : ℝ
    def FABL.F₂DecisionTree.vectorFourierWeightAbove
  {n : ℕ} (k : ℕ)
  (f : FABL.F₂Cube n → ℝ) : ℝ
    Fourier weight strictly above a natural cutoff, in vector indexing.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.vectorFourierWeightAbove_le_expect_sq_sub_of_degree_le
  {n : ℕ} (f g : FABL.F₂Cube n → ℝ) (k : ℕ)
  (hdegree : FABL.vectorFourierDegree g ≤ k) :
  FABL.F₂DecisionTree.vectorFourierWeightAbove k f ≤
    Finset.univ.expect fun x => (f x - g x) ^ 2
    theorem FABL.F₂DecisionTree.vectorFourierWeightAbove_le_expect_sq_sub_of_degree_le
  {n : ℕ} (f g : FABL.F₂Cube n → ℝ)
  (k : ℕ)
  (hdegree :
    FABL.vectorFourierDegree g ≤ k) :
  FABL.F₂DecisionTree.vectorFourierWeightAbove
      k f ≤
    Finset.univ.expect fun x =>
      (f x - g x) ^ 2
    Parseval: the tail above `k` is controlled by squared approximation error to any function
of degree at most `k`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.vectorFourierWeightAbove_eval_le_leafCount_mul_inverseTwoPow
  {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available) (k : ℕ)
  (hsign : ∀ (x : FABL.F₂Cube n), T.eval x = -1 ∨ T.eval x = 1) :
  FABL.F₂DecisionTree.vectorFourierWeightAbove k T.eval ≤
    ↑T.leafCount * (2 ^ k)⁻¹
    theorem FABL.F₂DecisionTree.vectorFourierWeightAbove_eval_le_leafCount_mul_inverseTwoPow
  {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  (k : ℕ)
  (hsign :
    ∀ (x : FABL.F₂Cube n),
      T.eval x = -1 ∨ T.eval x = 1) :
  FABL.F₂DecisionTree.vectorFourierWeightAbove
      k T.eval ≤
    ↑T.leafCount * (2 ^ k)⁻¹
    Fourier-tail form of depth truncation: a sign-valued size-`s` tree has weight above `k`
at most `s 2⁻ᵏ`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.vectorFourierWeightAbove_decisionTreeTruncationDegree_le
  {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available) {ε : ℝ} (hε : ε ∈ Set.Ioc 0 1)
  (hsign : ∀ (x : FABL.F₂Cube n), T.eval x = -1 ∨ T.eval x = 1) :
  FABL.F₂DecisionTree.vectorFourierWeightAbove
      (FABL.F₂DecisionTree.decisionTreeTruncationDegree T.leafCount ε)
      T.eval ≤
    ε
    theorem FABL.F₂DecisionTree.vectorFourierWeightAbove_decisionTreeTruncationDegree_le
  {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  {ε : ℝ} (hε : ε ∈ Set.Ioc 0 1)
  (hsign :
    ∀ (x : FABL.F₂Cube n),
      T.eval x = -1 ∨ T.eval x = 1) :
  FABL.F₂DecisionTree.vectorFourierWeightAbove
      (FABL.F₂DecisionTree.decisionTreeTruncationDegree
        T.leafCount ε)
      T.eval ≤
    ε
    Proposition 3.17 in vector indexing at the exact integer cutoff. The book writes
`log(s / ε)` and suppresses the integer rounding; the executable convention here is
`k = ⌈log₂(s / ε)⌉`.
  • theoremdefined in FABL/Chapter03/SubspacesAndDecisionTrees/DecisionTreeFourier.lean
    complete
    theorem FABL.F₂DecisionTree.isFourierSpectrumConcentratedUpTo_of_decisionTree
  {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available) (f : FABL.F₂Cube n → ℝ)
  (hT : T.Computes f) {ε : ℝ} (hε : ε ∈ Set.Ioc 0 1)
  (hsign : ∀ (x : FABL.F₂Cube n), f x = -1 ∨ f x = 1) :
  FABL.IsFourierSpectrumConcentratedUpTo
    (FABL.binaryFunctionOnSignCube f) ε
    ↑(FABL.F₂DecisionTree.decisionTreeTruncationDegree T.leafCount ε)
    theorem FABL.F₂DecisionTree.isFourierSpectrumConcentratedUpTo_of_decisionTree
  {n : ℕ} {available : Finset (Fin n)}
  (T : FABL.F₂DecisionTree n ℝ available)
  (f : FABL.F₂Cube n → ℝ)
  (hT : T.Computes f) {ε : ℝ}
  (hε : ε ∈ Set.Ioc 0 1)
  (hsign :
    ∀ (x : FABL.F₂Cube n),
      f x = -1 ∨ f x = 1) :
  FABL.IsFourierSpectrumConcentratedUpTo
    (FABL.binaryFunctionOnSignCube f) ε
    ↑(FABL.F₂DecisionTree.decisionTreeTruncationDegree
        T.leafCount ε)
    Proposition 3.17 in the Chapter 3 spectral-concentration API, with explicit base-two
ceiling and the book's boundary condition `ε ∈ (0, 1]`.