Analysis of Boolean Functions in Lean

8.3. Orthogonal decomposition🔗

Lemma8.3.1
Group: Chapter 8: Generalized domains (128)
Group member previews
Preview
Definition 8.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 8.2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-8-3fidelity-exact

Lemma 8.34. Suppose f depends only on coordinates I and g depends only on coordinates J. Then \langle f,g\rangle =\left\langle f^{\subseteq I\cap J}, g^{\subseteq I\cap J} \right\rangle.

Lean code for Lemma8.3.1●2 theorems
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.productInner_eq_project_inter_of_dependsOnly.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} {f g : FABL.ProductL2 Ω n}
  {I J : Finset (Fin n)} (hf : FABL.DependsOnlyOnCoordinates f I)
  (hg : FABL.DependsOnlyOnCoordinates g J) :
  FABL.productInner π n f g =
    FABL.productInner π n (FABL.projectOnCoordinates π (I ∩ J) f)
      (FABL.projectOnCoordinates π (I ∩ J) g)
    theorem FABL.productInner_eq_project_inter_of_dependsOnly.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} {f g : FABL.ProductL2 Ω n}
  {I J : Finset (Fin n)}
  (hf : FABL.DependsOnlyOnCoordinates f I)
  (hg :
    FABL.DependsOnlyOnCoordinates g J) :
  FABL.productInner π n f g =
    FABL.productInner π n
      (FABL.projectOnCoordinates π (I ∩ J)
        f)
      (FABL.projectOnCoordinates π (I ∩ J)
        g)
    Lemma 8.34: the inner product of an `I`-junta and a `J`-junta is already determined by
their projections onto `I ∩ J`.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.projectOnCoordinates_projectOnCoordinates.{u_1, u_2} {Ω : Type u_1}
  [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι] (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (I J : Finset (Fin n)) (f : FABL.ProductL2 Ω n) :
  FABL.projectOnCoordinates π I (FABL.projectOnCoordinates π J f) =
    FABL.projectOnCoordinates π (I ∩ J) f
    theorem FABL.projectOnCoordinates_projectOnCoordinates.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (I J : Finset (Fin n))
  (f : FABL.ProductL2 Ω n) :
  FABL.projectOnCoordinates π I
      (FABL.projectOnCoordinates π J f) =
    FABL.projectOnCoordinates π (I ∩ J) f
    Nested coordinate projections satisfy the tower law.
Theorem8.3.2
Group: Chapter 8: Generalized domains (128)
Group member previews
Preview
Definition 8.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 8.2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 11
Reverse dependency previews
Preview
Theorem 8.3.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-8-3fidelity-exact

Theorem 8.35. Every f\in L^2(\Omega^n,\pi^{\otimes n}) has a unique orthogonal decomposition f=\sum_{S\subseteq[n]}f^{=S} such that f^{=S} depends only on S and is orthogonal to every function depending on a proper subset of S. More precisely:

  • if S\nsubseteq T and g depends only on T, then \langle f^{=S},g\rangle=0;

  • S\ne T implies \langle f^{=S},f^{=T}\rangle=0;

  • \sum_{S\subseteq T}f^{=S}=f^{\subseteq T};

  • for fixed S, the map f\mapsto f^{=S} is linear;

  • the explicit Möbius formula is f^{=S}=\sum_{J\subseteq S}(-1)^{|S|-|J|}f^{\subseteq J}.

Lean code for Theorem8.3.2●14 declarations
  • defdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    def FABL.FiniteFourierBasis.orthogonalComponent.{u_1, u_2} {Ω : Type u_1}
  [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι] (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n) (S : Finset (Fin n)) :
  FABL.ProductL2 Ω n
    def FABL.FiniteFourierBasis.orthogonalComponent.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (S : Finset (Fin n)) :
  FABL.ProductL2 Ω n
    O'Donnell's `f^{=S}`.  Proposition 8.36 identifies this exact-support Fourier sum with the
basis-free component characterized in Theorem 8.35.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.FiniteFourierBasis.orthogonalComponent_dependsOnly.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (S : Finset (Fin n)) :
  FABL.DependsOnlyOnCoordinates (B.orthogonalComponent f S) S
    theorem FABL.FiniteFourierBasis.orthogonalComponent_dependsOnly.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (S : Finset (Fin n)) :
  FABL.DependsOnlyOnCoordinates
    (B.orthogonalComponent f S) S
    Theorem 8.35(1): `f^{=S}` depends only on the coordinates in `S`.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.FiniteFourierBasis.sum_orthogonalComponent.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n) :
  ∑ S, B.orthogonalComponent f S = f
    theorem FABL.FiniteFourierBasis.sum_orthogonalComponent.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n) :
  ∑ S, B.orthogonalComponent f S = f
    Theorem 8.35's decomposition equation.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.FiniteFourierBasis.productInner_orthogonalComponent_eq_zero_of_not_subset.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  {S T : Finset (Fin n)} {g : FABL.ProductL2 Ω n}
  (hg : FABL.DependsOnlyOnCoordinates g T) (hST : ¬S ⊆ T) :
  FABL.productInner π n (B.orthogonalComponent f S) g = 0
    theorem FABL.FiniteFourierBasis.productInner_orthogonalComponent_eq_zero_of_not_subset.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  {S T : Finset (Fin n)}
  {g : FABL.ProductL2 Ω n}
  (hg : FABL.DependsOnlyOnCoordinates g T)
  (hST : ¬S ⊆ T) :
  FABL.productInner π n
      (B.orthogonalComponent f S) g =
    0
    Theorem 8.35(3), in its stronger useful form: `f^{=S}` is orthogonal to every function
depending on `T` whenever `S ⊈ T`.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.FiniteFourierBasis.productInner_orthogonalComponent_eq_zero_of_ssubset.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  {S T : Finset (Fin n)} {g : FABL.ProductL2 Ω n}
  (hg : FABL.DependsOnlyOnCoordinates g T) (hTS : T ⊂ S) :
  FABL.productInner π n (B.orthogonalComponent f S) g = 0
    theorem FABL.FiniteFourierBasis.productInner_orthogonalComponent_eq_zero_of_ssubset.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  {S T : Finset (Fin n)}
  {g : FABL.ProductL2 Ω n}
  (hg : FABL.DependsOnlyOnCoordinates g T)
  (hTS : T ⊂ S) :
  FABL.productInner π n
      (B.orthogonalComponent f S) g =
    0
    Theorem 8.35(2): strict lower-coordinate functions are orthogonal to `f^{=S}`.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.FiniteFourierBasis.orthogonalComponent_pairwise_orthogonal.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f g : FABL.ProductL2 Ω n)
  {S T : Finset (Fin n)} (hST : S ≠ T) :
  FABL.productInner π n (B.orthogonalComponent f S)
      (B.orthogonalComponent g T) =
    0
    theorem FABL.FiniteFourierBasis.orthogonalComponent_pairwise_orthogonal.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f g : FABL.ProductL2 Ω n)
  {S T : Finset (Fin n)} (hST : S ≠ T) :
  FABL.productInner π n
      (B.orthogonalComponent f S)
      (B.orthogonalComponent g T) =
    0
    Theorem 8.35(4): distinct exact-support components are orthogonal.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.FiniteFourierBasis.sum_orthogonalComponent_subset.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (T : Finset (Fin n)) :
  ∑ S ∈ T.powerset, B.orthogonalComponent f S =
    FABL.projectOnCoordinates π T f
    theorem FABL.FiniteFourierBasis.sum_orthogonalComponent_subset.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (T : Finset (Fin n)) :
  ∑ S ∈ T.powerset,
      B.orthogonalComponent f S =
    FABL.projectOnCoordinates π T f
    Exercise 8.14 / Theorem 8.35(5): the projection onto `T` is the sum of all exact-support
components indexed below `T`.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.FiniteFourierBasis.orthogonalComponent_add.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f g : FABL.ProductL2 Ω n)
  (S : Finset (Fin n)) :
  B.orthogonalComponent (f + g) S =
    B.orthogonalComponent f S + B.orthogonalComponent g S
    theorem FABL.FiniteFourierBasis.orthogonalComponent_add.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f g : FABL.ProductL2 Ω n)
  (S : Finset (Fin n)) :
  B.orthogonalComponent (f + g) S =
    B.orthogonalComponent f S +
      B.orthogonalComponent g S
    Theorem 8.35(6): exact-support decomposition is additive.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.FiniteFourierBasis.orthogonalComponent_smul.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (c : ℝ)
  (f : FABL.ProductL2 Ω n) (S : Finset (Fin n)) :
  B.orthogonalComponent (c • f) S = c • B.orthogonalComponent f S
    theorem FABL.FiniteFourierBasis.orthogonalComponent_smul.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (c : ℝ) (f : FABL.ProductL2 Ω n)
  (S : Finset (Fin n)) :
  B.orthogonalComponent (c • f) S =
    c • B.orthogonalComponent f S
    Theorem 8.35(6): exact-support decomposition respects real scalars.
  • defdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    def FABL.IsOrthogonalDecomposition.{u_1} {Ω : Type u_1} [Fintype Ω]
  (π : PMF Ω) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (component : Finset (Fin n) → FABL.ProductL2 Ω n) : Prop
    def FABL.IsOrthogonalDecomposition.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (component :
    Finset (Fin n) → FABL.ProductL2 Ω n) :
  Prop
    A family satisfies the two defining conditions in Theorem 8.35.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.FiniteFourierBasis.isOrthogonalDecomposition.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n) :
  FABL.IsOrthogonalDecomposition π f (B.orthogonalComponent f)
    theorem FABL.FiniteFourierBasis.isOrthogonalDecomposition.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n) :
  FABL.IsOrthogonalDecomposition π f
    (B.orthogonalComponent f)
    The canonical exact-support family satisfies the defining conditions of Theorem 8.35.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.FiniteFourierBasis.orthogonalDecomposition_unique.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} {f : FABL.ProductL2 Ω n}
  {component : Finset (Fin n) → FABL.ProductL2 Ω n}
  (hcomponent : FABL.IsOrthogonalDecomposition π f component) :
  component = B.orthogonalComponent f
    theorem FABL.FiniteFourierBasis.orthogonalDecomposition_unique.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} {f : FABL.ProductL2 Ω n}
  {component :
    Finset (Fin n) → FABL.ProductL2 Ω n}
  (hcomponent :
    FABL.IsOrthogonalDecomposition π f
      component) :
  component = B.orthogonalComponent f
    Theorem 8.35, uniqueness: every family satisfying the two defining conditions is the
exact-support family.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.FiniteFourierBasis.orthogonalComponent_eq_mobius.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (S : Finset (Fin n)) :
  B.orthogonalComponent f S =
    ∑ J ∈ S.powerset,
      (-1) ^ (S.card - J.card) • FABL.projectOnCoordinates π J f
    theorem FABL.FiniteFourierBasis.orthogonalComponent_eq_mobius.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (S : Finset (Fin n)) :
  B.orthogonalComponent f S =
    ∑ J ∈ S.powerset,
      (-1) ^ (S.card - J.card) •
        FABL.projectOnCoordinates π J f
    The explicit inclusion-exclusion formula in the proof of Theorem 8.35:
`f^{=S} = ∑_{J ⊆ S} (-1)^{|S|-|J|} f^{⊆J}`.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.orthogonalComponent_basis_independent.{u_1, u_2, u_3}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  {κ : Type u_3} [Fintype ι] [Nonempty ι] [DecidableEq ι] [Fintype κ]
  [Nonempty κ] [DecidableEq κ] (B : FABL.FiniteFourierBasis Ω π ι)
  (C : FABL.FiniteFourierBasis Ω π κ) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (S : Finset (Fin n)) :
  B.orthogonalComponent f S = C.orthogonalComponent f S
    theorem FABL.orthogonalComponent_basis_independent.{u_1,
    u_2, u_3}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2}
  {κ : Type u_3} [Fintype ι] [Nonempty ι]
  [DecidableEq ι] [Fintype κ] [Nonempty κ]
  [DecidableEq κ]
  (B : FABL.FiniteFourierBasis Ω π ι)
  (C : FABL.FiniteFourierBasis Ω π κ)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (S : Finset (Fin n)) :
  B.orthogonalComponent f S =
    C.orthogonalComponent f S
    The Möbius formula makes the orthogonal component independent of the auxiliary Fourier
basis used to construct the exact-support sum.
Theorem8.3.3
Group: Chapter 8: Generalized domains (128)
Group member previews
Preview
Definition 8.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 8.2.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-8-3fidelity-exact

Proposition 8.36. Relative to every product Fourier basis, f^{=S} =\sum_{\operatorname{supp}(\alpha)=S} \widehat f(\alpha)\phi_\alpha.

Lean code for Theorem8.3.3●2 theorems
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.FiniteFourierBasis.orthogonalComponent_eq_fourierComponentAtSupport.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (S : Finset (Fin n)) :
  B.orthogonalComponent f S =
    ∑ a with FABL.multiIndexSupport B.zeroIndex a = S,
      B.fourierCoeff f a • B.productFunction a
    theorem FABL.FiniteFourierBasis.orthogonalComponent_eq_fourierComponentAtSupport.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (S : Finset (Fin n)) :
  B.orthogonalComponent f S =
    ∑ a with
      FABL.multiIndexSupport B.zeroIndex
          a =
        S,
      B.fourierCoeff f a •
        B.productFunction a
    Proposition 8.36: an orthogonal component is exactly the sum of the product-Fourier terms
whose multi-index has support `S`.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.FiniteFourierBasis.fourierCoeff_orthogonalComponent.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (S : Finset (Fin n)) (a : FABL.MultiIndex n ι) :
  B.fourierCoeff (B.orthogonalComponent f S) a =
    if FABL.multiIndexSupport B.zeroIndex a = S then B.fourierCoeff f a
    else 0
    theorem FABL.FiniteFourierBasis.fourierCoeff_orthogonalComponent.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (S : Finset (Fin n))
  (a : FABL.MultiIndex n ι) :
  B.fourierCoeff
      (B.orthogonalComponent f S) a =
    if
        FABL.multiIndexSupport B.zeroIndex
            a =
          S then
      B.fourierCoeff f a
    else 0
    The Fourier coefficient of `f^{=S}` is the coefficient of `f` exactly on support `S`.
Lemma8.3.4
Group: Chapter 8: Generalized domains (128)
Group member previews
Preview
Definition 8.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Lemma 8.1.15
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-8-3fidelity-exact

Example 8.37. For the point indicator of Example 8.15, f^{=\varnothing}=1/9. For i\in\{1,2\}, f^{=\{i\}}(x)= \begin{cases}2/9,&x_i=c,\\-1/9,&x_i\ne c,\end{cases} and f^{=\{1,2\}}(x)= \begin{cases} 4/9,&x_1=x_2=c,\\ -2/9,&\text{exactly one coordinate is }c,\\ 1/9,&x_1,x_2\ne c. \end{cases}

Lean code for Lemma8.3.4●5 declarations
  • defdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    def FABL.threePointSingletonOrthogonalValue (i : Fin 2)
  (x : Fin 2 → FABL.ThreePoint) : ℝ
    def FABL.threePointSingletonOrthogonalValue
  (i : Fin 2)
  (x : Fin 2 → FABL.ThreePoint) : ℝ
    Example 8.37's singleton component.
  • defdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    def FABL.threePointPairOrthogonalValue (x : Fin 2 → FABL.ThreePoint) : ℝ
    def FABL.threePointPairOrthogonalValue
  (x : Fin 2 → FABL.ThreePoint) : ℝ
    Example 8.37's two-coordinate component.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.threePointBothCIndicator_orthogonalComponent_empty :
  FABL.threePointFourierBasis.orthogonalComponent
      FABL.threePointBothCIndicator ∅ =
    fun x => 1 / 9
    theorem FABL.threePointBothCIndicator_orthogonalComponent_empty :
  FABL.threePointFourierBasis.orthogonalComponent
      FABL.threePointBothCIndicator ∅ =
    fun x => 1 / 9
    Example 8.37: the empty component is the constant mean `1/9`.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.threePointBothCIndicator_orthogonalComponent_singleton
  (i : Fin 2) :
  FABL.threePointFourierBasis.orthogonalComponent
      FABL.threePointBothCIndicator {i} =
    FABL.threePointSingletonOrthogonalValue i
    theorem FABL.threePointBothCIndicator_orthogonalComponent_singleton
  (i : Fin 2) :
  FABL.threePointFourierBasis.orthogonalComponent
      FABL.threePointBothCIndicator {i} =
    FABL.threePointSingletonOrthogonalValue
      i
    Example 8.37: each singleton component is `2/9` at `c` and `-1/9` elsewhere.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.threePointBothCIndicator_orthogonalComponent_pair :
  FABL.threePointFourierBasis.orthogonalComponent
      FABL.threePointBothCIndicator Finset.univ =
    FABL.threePointPairOrthogonalValue
    theorem FABL.threePointBothCIndicator_orthogonalComponent_pair :
  FABL.threePointFourierBasis.orthogonalComponent
      FABL.threePointBothCIndicator
      Finset.univ =
    FABL.threePointPairOrthogonalValue
    Example 8.37: the top component has values `4/9`, `-2/9`, and `1/9` in the three
displayed cases.
Definition8.3.5
Group: Chapter 8: Generalized domains (128)
Group member previews
Preview
Definition 8.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N
Tagssection-8-3fidelity-exact

Definition 8.38. Define the degree layers and weights by f^{=k}=\sum_{|S|=k}f^{=S}, \qquad W^k[f]=\|f^{=k}\|_2^2. Also set f^{\le k}=\sum_{|S|\le k}f^{=S}, \qquad W^{>k}[f]=\sum_{|S|>k}\|f^{=S}\|_2^2.

Lean code for Definition8.3.5●6 declarations
  • defdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    def FABL.FiniteFourierBasis.orthogonalDegreePart.{u_1, u_2} {Ω : Type u_1}
  [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι] (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n) (k : ℕ) : FABL.ProductL2 Ω n
    def FABL.FiniteFourierBasis.orthogonalDegreePart.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (k : ℕ) : FABL.ProductL2 Ω n
    Definition 8.38: the degree-`k` part `f^{=k}`.
  • defdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    def FABL.FiniteFourierBasis.orthogonalWeightAtDegree.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (k : ℕ) : ℝ
    def FABL.FiniteFourierBasis.orthogonalWeightAtDegree.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (k : ℕ) : ℝ
    Definition 8.38: the degree-`k` orthogonal weight.
  • defdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    def FABL.FiniteFourierBasis.orthogonalLowDegreePart.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (k : ℕ) : FABL.ProductL2 Ω n
    def FABL.FiniteFourierBasis.orthogonalLowDegreePart.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (k : ℕ) : FABL.ProductL2 Ω n
    Definition 8.38: the part of degree at most `k`.
  • defdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    def FABL.FiniteFourierBasis.orthogonalWeightAboveDegree.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (k : ℕ) : ℝ
    def FABL.FiniteFourierBasis.orthogonalWeightAboveDegree.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (k : ℕ) : ℝ
    Definition 8.38: the orthogonal weight strictly above degree `k`.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.FiniteFourierBasis.fourierCoeff_orthogonalDegreePart.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (k : ℕ) (a : FABL.MultiIndex n ι) :
  B.fourierCoeff (B.orthogonalDegreePart f k) a =
    if FABL.multiIndexOrder B.zeroIndex a = k then B.fourierCoeff f a
    else 0
    theorem FABL.FiniteFourierBasis.fourierCoeff_orthogonalDegreePart.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n) (k : ℕ)
  (a : FABL.MultiIndex n ι) :
  B.fourierCoeff
      (B.orthogonalDegreePart f k) a =
    if
        FABL.multiIndexOrder B.zeroIndex
            a =
          k then
      B.fourierCoeff f a
    else 0
    The coefficient of the degree-`k` part is retained exactly at support order `k`.
  • theoremdefined in FABL/Chapter08/OrthogonalDecomposition.lean
    complete
    theorem FABL.FiniteFourierBasis.orthogonalWeightAtDegree_eq_sum_sq_fourierCoeff.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (k : ℕ) :
  B.orthogonalWeightAtDegree f k =
    ∑ a with FABL.multiIndexOrder B.zeroIndex a = k,
      B.fourierCoeff f a ^ 2
    theorem FABL.FiniteFourierBasis.orthogonalWeightAtDegree_eq_sum_sq_fourierCoeff.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (k : ℕ) :
  B.orthogonalWeightAtDegree f k =
    ∑ a with
      FABL.multiIndexOrder B.zeroIndex a =
        k,
      B.fourierCoeff f a ^ 2
    Definition 8.38 in spectral form.