Analysis of Boolean Functions in Lean

8.2. Generalized Fourier formulas🔗

Theorem8.2.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.
uses 1
Used by 6
Reverse dependency previews
Preview
Theorem 8.2.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-8-2fidelity-exact

Proposition 8.16. For f,g\in L^2(\Omega^n,\pi^{\otimes n}) and any fixed product Fourier basis, \mathbb E[f]=\widehat f(0), \qquad \mathbb E[f^2]=\sum_\alpha\widehat f(\alpha)^2, \qquad \operatorname{Var}[f]=\sum_{\alpha\ne0}\widehat f(\alpha)^2, \langle f,g\rangle =\sum_\alpha\widehat f(\alpha)\widehat g(\alpha), \qquad \operatorname{Cov}[f,g] =\sum_{\alpha\ne0}\widehat f(\alpha)\widehat g(\alpha).

Lean code for Theorem8.2.1●14 declarations
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productMean.{u_1} {Ω : Type u_1} [Fintype Ω] (π : PMF Ω) {n : ℕ}
  (f : FABL.ProductL2 Ω n) : ℝ
    def FABL.productMean.{u_1} {Ω : Type u_1}
  [Fintype Ω] (π : PMF Ω) {n : ℕ}
  (f : FABL.ProductL2 Ω n) : ℝ
    Mean under a finite product law.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productSecondMoment.{u_1} {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f : FABL.ProductL2 Ω n) : ℝ
    def FABL.productSecondMoment.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f : FABL.ProductL2 Ω n) : ℝ
    Second moment under a finite product law.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productVariance.{u_1} {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f : FABL.ProductL2 Ω n) : ℝ
    def FABL.productVariance.{u_1} {Ω : Type u_1}
  [Fintype Ω] (π : PMF Ω) {n : ℕ}
  (f : FABL.ProductL2 Ω n) : ℝ
    Variance under a finite product law.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productCovariance.{u_1} {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f g : FABL.ProductL2 Ω n) : ℝ
    def FABL.productCovariance.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f g : FABL.ProductL2 Ω n) : ℝ
    Covariance under a finite product law.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.fourierCoeff_zeroMultiIndex.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n) :
  B.fourierCoeff f (B.zeroMultiIndex n) = FABL.productMean π f
    theorem FABL.FiniteFourierBasis.fourierCoeff_zeroMultiIndex.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n) :
  B.fourierCoeff f (B.zeroMultiIndex n) =
    FABL.productMean π f
    The product Fourier coefficient at the zero multi-index is the mean.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.plancherel.{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) :
  FABL.productInner π n f g =
    ∑ a, B.fourierCoeff f a * B.fourierCoeff g a
    theorem FABL.FiniteFourierBasis.plancherel.{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) :
  FABL.productInner π n f g =
    ∑ a,
      B.fourierCoeff f a *
        B.fourierCoeff g a
    Proposition 8.16, Plancherel: the weighted product inner product is the dot product of
Fourier coefficients.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.parseval.{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.productSecondMoment π f = ∑ a, B.fourierCoeff f a ^ 2
    theorem FABL.FiniteFourierBasis.parseval.{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.productSecondMoment π f =
    ∑ a, B.fourierCoeff f a ^ 2
    Proposition 8.16, Parseval.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.variance_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) :
  FABL.productVariance π f =
    ∑ a with a ≠ B.zeroMultiIndex n, B.fourierCoeff f a ^ 2
    theorem FABL.FiniteFourierBasis.variance_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) :
  FABL.productVariance π f =
    ∑ a with a ≠ B.zeroMultiIndex n,
      B.fourierCoeff f a ^ 2
    Proposition 8.16, variance formula.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.covariance_eq_sum_fourierCoeff_mul.{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) :
  FABL.productCovariance π f g =
    ∑ a with a ≠ B.zeroMultiIndex n,
      B.fourierCoeff f a * B.fourierCoeff g a
    theorem FABL.FiniteFourierBasis.covariance_eq_sum_fourierCoeff_mul.{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) :
  FABL.productCovariance π f g =
    ∑ a with a ≠ B.zeroMultiIndex n,
      B.fourierCoeff f a *
        B.fourierCoeff g a
    Proposition 8.16, covariance formula.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.productMean_uniformSign {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.productMean (FABL.uniformPMF FABL.Sign) f = FABL.mean f
    theorem FABL.productMean_uniformSign {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.productMean
      (FABL.uniformPMF FABL.Sign) f =
    FABL.mean f
    Product mean under uniform signs is the existing canonical mean.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.productSecondMoment_uniformSign {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.productSecondMoment (FABL.uniformPMF FABL.Sign) f =
    Finset.univ.expect fun x => f x ^ 2
    theorem FABL.productSecondMoment_uniformSign
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.productSecondMoment
      (FABL.uniformPMF FABL.Sign) f =
    Finset.univ.expect fun x => f x ^ 2
    Product second moment under uniform signs is the canonical normalized second moment.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.productVariance_uniformSign {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.productVariance (FABL.uniformPMF FABL.Sign) f = FABL.variance f
    theorem FABL.productVariance_uniformSign {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.productVariance
      (FABL.uniformPMF FABL.Sign) f =
    FABL.variance f
    Product variance specializes to Chapter 1's canonical variance.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.productCovariance_uniformSign {n : ℕ} (f g : FABL.SignCube n → ℝ) :
  FABL.productCovariance (FABL.uniformPMF FABL.Sign) f g =
    FABL.covariance f g
    theorem FABL.productCovariance_uniformSign {n : ℕ}
  (f g : FABL.SignCube n → ℝ) :
  FABL.productCovariance
      (FABL.uniformPMF FABL.Sign) f g =
    FABL.covariance f g
    Product covariance specializes to Chapter 1's canonical covariance.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.productInner_uniformSign {n : ℕ} (f g : FABL.SignCube n → ℝ) :
  FABL.productInner (FABL.uniformPMF FABL.Sign) n f g =
    FABL.uniformInner f g
    theorem FABL.productInner_uniformSign {n : ℕ}
  (f g : FABL.SignCube n → ℝ) :
  FABL.productInner
      (FABL.uniformPMF FABL.Sign) n f g =
    FABL.uniformInner f g
    The product weighted inner product under uniform signs is FABL's canonical normalized inner
product.
Definition8.2.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.
uses 1
Used by 9
Reverse dependency previews
Preview
Lemma 8.2.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-8-2fidelity-exact

Definition 8.17. Let J\subseteq[n] and \bar J=[n]\setminus J. The projection of f onto coordinates J is f^{\subseteq J}(x) =\mathbb E_{x'\sim\pi^{\otimes\bar J}}[f(x_J,x')]. Equivalently, the coordinates outside J are independently rerandomized. Write E_{\bar J}f=f^{\subseteq J} and E_i when the rerandomized set is the singleton \{i\}.

Lean code for Definition8.2.2●5 declarations
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.mergeOnCoordinates.{u_1} {Ω : Type u_1} {n : ℕ}
  (J : Finset (Fin n)) (x y : Fin n → Ω) : Fin n → Ω
    def FABL.mergeOnCoordinates.{u_1}
  {Ω : Type u_1} {n : ℕ}
  (J : Finset (Fin n)) (x y : Fin n → Ω) :
  Fin n → Ω
    Combine the retained coordinates of `x` on `J` with fresh coordinates from `y` outside
`J`.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.DependsOnlyOnCoordinates.{u_1} {Ω : Type u_1} {n : ℕ}
  (f : FABL.ProductL2 Ω n) (J : Finset (Fin n)) : Prop
    def FABL.DependsOnlyOnCoordinates.{u_1}
  {Ω : Type u_1} {n : ℕ}
  (f : FABL.ProductL2 Ω n)
  (J : Finset (Fin n)) : Prop
    A function depends only on coordinates in `J` when agreeing on `J` forces equal outputs.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.projectOnCoordinates.{u_1} {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (J : Finset (Fin n)) (f : FABL.ProductL2 Ω n) :
  FABL.ProductL2 Ω n
    def FABL.projectOnCoordinates.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (J : Finset (Fin n))
  (f : FABL.ProductL2 Ω n) :
  FABL.ProductL2 Ω n
    O'Donnell, Definition 8.17: projection onto the coordinates `J`, obtained by rerandomizing
all coordinates outside `J`.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.projectOnCoordinates_dependsOnly.{u_1} {Ω : Type u_1} [Fintype Ω]
  (π : PMF Ω) {n : ℕ} (J : Finset (Fin n)) (f : FABL.ProductL2 Ω n) :
  FABL.DependsOnlyOnCoordinates (FABL.projectOnCoordinates π J f) J
    theorem FABL.projectOnCoordinates_dependsOnly.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (J : Finset (Fin n))
  (f : FABL.ProductL2 Ω n) :
  FABL.DependsOnlyOnCoordinates
    (FABL.projectOnCoordinates π J f) J
    The output of coordinate projection depends only on retained coordinates.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.projectOnCoordinates_eq_self_of_dependsOnly.{u_1} {Ω : Type u_1}
  [Fintype Ω] (π : PMF Ω) {n : ℕ} {J : Finset (Fin n)}
  {f : FABL.ProductL2 Ω n} (hf : FABL.DependsOnlyOnCoordinates f J) :
  FABL.projectOnCoordinates π J f = f
    theorem FABL.projectOnCoordinates_eq_self_of_dependsOnly.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} {J : Finset (Fin n)}
  {f : FABL.ProductL2 Ω n}
  (hf :
    FABL.DependsOnlyOnCoordinates f J) :
  FABL.projectOnCoordinates π J f = f
    Projection fixes every function already depending only on the retained coordinates.
Lemma8.2.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
Definition 2.2.13
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-8-2fidelity-exact

Remark 8.18. This E_i agrees with the coordinate-expectation operator of Definition 2.23. More generally E_J is a linear, idempotent, self-adjoint projection.

Lean code for Lemma8.2.3●3 theorems
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.projectOnCoordinates_idempotent.{u_1, u_2} {Ω : Type u_1}
  [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι] (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (J : Finset (Fin n)) (f : FABL.ProductL2 Ω n) :
  FABL.projectOnCoordinates π J (FABL.projectOnCoordinates π J f) =
    FABL.projectOnCoordinates π J f
    theorem FABL.projectOnCoordinates_idempotent.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (J : Finset (Fin n))
  (f : FABL.ProductL2 Ω n) :
  FABL.projectOnCoordinates π J
      (FABL.projectOnCoordinates π J f) =
    FABL.projectOnCoordinates π J f
    Exercise 8.7: coordinate projection is idempotent.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.projectOnCoordinates_selfAdjoint.{u_1, u_2} {Ω : Type u_1}
  [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι] (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (J : Finset (Fin n)) (f g : FABL.ProductL2 Ω n) :
  FABL.productInner π n f (FABL.projectOnCoordinates π J g) =
    FABL.productInner π n (FABL.projectOnCoordinates π J f) g
    theorem FABL.projectOnCoordinates_selfAdjoint.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (J : Finset (Fin n))
  (f g : FABL.ProductL2 Ω n) :
  FABL.productInner π n f
      (FABL.projectOnCoordinates π J g) =
    FABL.productInner π n
      (FABL.projectOnCoordinates π J f) g
    Exercise 8.7: coordinate projection is self-adjoint.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.coordinateProjection_uniformSign_eq_coordinateExpectation {n : ℕ}
  (i : Fin n) (f : FABL.SignCube n → ℝ) :
  FABL.coordinateProjection (FABL.uniformPMF FABL.Sign) i f =
    (FABL.coordinateExpectation i) f
    theorem FABL.coordinateProjection_uniformSign_eq_coordinateExpectation
  {n : ℕ} (i : Fin n)
  (f : FABL.SignCube n → ℝ) :
  FABL.coordinateProjection
      (FABL.uniformPMF FABL.Sign) i f =
    (FABL.coordinateExpectation i) f
    Remark 8.18: Chapter 8 coordinate projection is exactly Chapter 2's
`coordinateExpectation`.
Theorem8.2.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
Definition 8.1.14
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Theorem 8.2.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-8-2fidelity-exact

Proposition 8.19. For every fixed product Fourier basis, f^{\subseteq J} =\sum_{\operatorname{supp}(\alpha)\subseteq J} \widehat f(\alpha)\phi_\alpha.

Lean code for Theorem8.2.4●3 theorems
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.projectOnCoordinates_productFunction.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (J : Finset (Fin n))
  (a : FABL.MultiIndex n ι) :
  FABL.projectOnCoordinates π J (B.productFunction a) =
    if FABL.multiIndexSupport B.zeroIndex a ⊆ J then B.productFunction a
    else 0
    theorem FABL.FiniteFourierBasis.projectOnCoordinates_productFunction.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (J : Finset (Fin n))
  (a : FABL.MultiIndex n ι) :
  FABL.projectOnCoordinates π J
      (B.productFunction a) =
    if
        FABL.multiIndexSupport B.zeroIndex
            a ⊆
          J then
      B.productFunction a
    else 0
    Proposition 8.19 on one basis vector: projection keeps precisely the product functions whose
support lies in the retained coordinate set.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.projectOnCoordinates_fourier_expansion.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (J : Finset (Fin n))
  (f : FABL.ProductL2 Ω n) (x : Fin n → Ω) :
  FABL.projectOnCoordinates π J f x =
    ∑ a with FABL.multiIndexSupport B.zeroIndex a ⊆ J,
      B.fourierCoeff f a * B.productFunction a x
    theorem FABL.FiniteFourierBasis.projectOnCoordinates_fourier_expansion.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (J : Finset (Fin n))
  (f : FABL.ProductL2 Ω n)
  (x : Fin n → Ω) :
  FABL.projectOnCoordinates π J f x =
    ∑ a with
      FABL.multiIndexSupport B.zeroIndex
          a ⊆
        J,
      B.fourierCoeff f a *
        B.productFunction a x
    Proposition 8.19: projection filters the Fourier expansion by support.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.fourierCoeff_projectOnCoordinates.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (J : Finset (Fin n))
  (f : FABL.ProductL2 Ω n) (a : FABL.MultiIndex n ι) :
  B.fourierCoeff (FABL.projectOnCoordinates π J f) a =
    if FABL.multiIndexSupport B.zeroIndex a ⊆ J then B.fourierCoeff f a
    else 0
    theorem FABL.FiniteFourierBasis.fourierCoeff_projectOnCoordinates.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (J : Finset (Fin n))
  (f : FABL.ProductL2 Ω n)
  (a : FABL.MultiIndex n ι) :
  B.fourierCoeff
      (FABL.projectOnCoordinates π J f)
      a =
    if
        FABL.multiIndexSupport B.zeroIndex
            a ⊆
          J then
      B.fourierCoeff f a
    else 0
    The coefficient of a projection is retained exactly on supported multi-indices.
Theorem8.2.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-2fidelity-exact

Corollary 8.20. If f depends only on the coordinates in J\subseteq[n], then \operatorname{supp}(\alpha)\nsubseteq J \quad\Longrightarrow\quad \widehat f(\alpha)=0.

Lean code for Theorem8.2.5●1 theorem
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.fourierCoeff_eq_zero_of_dependsOnly.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} {J : Finset (Fin n)}
  {f : FABL.ProductL2 Ω n} (hf : FABL.DependsOnlyOnCoordinates f J)
  {a : FABL.MultiIndex n ι}
  (ha : ¬FABL.multiIndexSupport B.zeroIndex a ⊆ J) :
  B.fourierCoeff f a = 0
    theorem FABL.FiniteFourierBasis.fourierCoeff_eq_zero_of_dependsOnly.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} {J : Finset (Fin n)}
  {f : FABL.ProductL2 Ω n}
  (hf : FABL.DependsOnlyOnCoordinates f J)
  {a : FABL.MultiIndex n ι}
  (ha :
    ¬FABL.multiIndexSupport B.zeroIndex
          a ⊆
        J) :
  B.fourierCoeff f a = 0
    Corollary 8.20: a function depending only on `J` has no Fourier support outside `J`.
Theorem8.2.6
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-2fidelity-exact

Corollary 8.21. For every coordinate i, E_i f=\sum_{\alpha:\alpha_i=0}\widehat f(\alpha)\phi_\alpha.

Lean code for Theorem8.2.6●2 declarations
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.coordinateProjection.{u_1} {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (i : Fin n) (f : FABL.ProductL2 Ω n) : FABL.ProductL2 Ω n
    def FABL.coordinateProjection.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (i : Fin n)
  (f : FABL.ProductL2 Ω n) :
  FABL.ProductL2 Ω n
    O'Donnell's `Eᵢ`: rerandomize coordinate `i` and retain every other coordinate.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.coordinateProjection_fourier_expansion.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (i : Fin n)
  (f : FABL.ProductL2 Ω n) (x : Fin n → Ω) :
  FABL.coordinateProjection π i f x =
    ∑ a with a i = B.zeroIndex,
      B.fourierCoeff f a * B.productFunction a x
    theorem FABL.FiniteFourierBasis.coordinateProjection_fourier_expansion.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (i : Fin n)
  (f : FABL.ProductL2 Ω n)
  (x : Fin n → Ω) :
  FABL.coordinateProjection π i f x =
    ∑ a with a i = B.zeroIndex,
      B.fourierCoeff f a *
        B.productFunction a x
    Corollary 8.21: coordinate expectation retains precisely the coefficients with zero `i`th
entry.
Definition8.2.7
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 1
Used by 9
Reverse dependency previews
Preview
Theorem 8.2.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-8-2fidelity-exact

Definition 8.22. The coordinate Laplacian is L_i f=f-E_i f. Define \operatorname{Inf}_i[f] =\langle f,L_i f\rangle =\langle L_i f,L_i f\rangle, \qquad \mathbf I[f]=\sum_{i=1}^n\operatorname{Inf}_i[f].

Lean code for Definition8.2.7●7 declarations
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productCoordinateLaplacian.{u_1} {Ω : Type u_1} [Fintype Ω]
  (π : PMF Ω) {n : ℕ} (i : Fin n) (f : FABL.ProductL2 Ω n) :
  FABL.ProductL2 Ω n
    def FABL.productCoordinateLaplacian.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (i : Fin n)
  (f : FABL.ProductL2 Ω n) :
  FABL.ProductL2 Ω n
    O'Donnell, Definition 8.22: the coordinate Laplacian `Lᵢ = I - Eᵢ`.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productInfluence.{u_1} {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f : FABL.ProductL2 Ω n) (i : Fin n) : ℝ
    def FABL.productInfluence.{u_1} {Ω : Type u_1}
  [Fintype Ω] (π : PMF Ω) {n : ℕ}
  (f : FABL.ProductL2 Ω n) (i : Fin n) : ℝ
    O'Donnell, Definition 8.22: influence is the squared weighted norm of the coordinate
Laplacian.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productTotalInfluence.{u_1} {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f : FABL.ProductL2 Ω n) : ℝ
    def FABL.productTotalInfluence.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f : FABL.ProductL2 Ω n) : ℝ
    O'Donnell, Definition 8.22: total influence.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.productInner_laplacian_eq_influence.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (i : Fin n) :
  FABL.productInner π n f (FABL.productCoordinateLaplacian π i f) =
    FABL.productInfluence π f i
    theorem FABL.FiniteFourierBasis.productInner_laplacian_eq_influence.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (i : Fin n) :
  FABL.productInner π n f
      (FABL.productCoordinateLaplacian π i
        f) =
    FABL.productInfluence π f i
    Definition 8.22's alternative formula `⟨f,Lᵢf⟩ = ‖Lᵢf‖₂²`.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.productCoordinateLaplacian_uniformSign_eq_coordinateLaplacian
  {n : ℕ} (i : Fin n) (f : FABL.SignCube n → ℝ) :
  FABL.productCoordinateLaplacian (FABL.uniformPMF FABL.Sign) i f =
    (FABL.coordinateLaplacian i) f
    theorem FABL.productCoordinateLaplacian_uniformSign_eq_coordinateLaplacian
  {n : ℕ} (i : Fin n)
  (f : FABL.SignCube n → ℝ) :
  FABL.productCoordinateLaplacian
      (FABL.uniformPMF FABL.Sign) i f =
    (FABL.coordinateLaplacian i) f
    Chapter 8 coordinate Laplacian specializes to the existing Chapter 2 Laplacian.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.productInfluence_uniformSign_eq_influence {n : ℕ}
  (f : FABL.SignCube n → ℝ) (i : Fin n) :
  FABL.productInfluence (FABL.uniformPMF FABL.Sign) f i =
    FABL.influence f i
    theorem FABL.productInfluence_uniformSign_eq_influence
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (i : Fin n) :
  FABL.productInfluence
      (FABL.uniformPMF FABL.Sign) f i =
    FABL.influence f i
    Chapter 8 influence specializes to the canonical Chapter 2 influence without changing the
old API.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.productTotalInfluence_uniformSign_eq_totalInfluence {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.productTotalInfluence (FABL.uniformPMF FABL.Sign) f =
    FABL.totalInfluence f
    theorem FABL.productTotalInfluence_uniformSign_eq_totalInfluence
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.productTotalInfluence
      (FABL.uniformPMF FABL.Sign) f =
    FABL.totalInfluence f
    Total influence also specializes definitionally through the coordinate bridge.
Theorem8.2.8
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 3
Statement dependency previews
Preview
Theorem 8.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-8-2fidelity-exact

Proposition 8.23. For every fixed product Fourier basis, L_i f=\sum_{\alpha:\alpha_i\ne0}\widehat f(\alpha)\phi_\alpha, \operatorname{Inf}_i[f] =\sum_{\alpha:\alpha_i\ne0}\widehat f(\alpha)^2, \qquad \mathbf I[f] =\sum_\alpha\#\alpha\,\widehat f(\alpha)^2.

Lean code for Theorem8.2.8●4 theorems
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.fourierCoeff_productCoordinateLaplacian.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (i : Fin n)
  (f : FABL.ProductL2 Ω n) (a : FABL.MultiIndex n ι) :
  B.fourierCoeff (FABL.productCoordinateLaplacian π i f) a =
    if a i ≠ B.zeroIndex then B.fourierCoeff f a else 0
    theorem FABL.FiniteFourierBasis.fourierCoeff_productCoordinateLaplacian.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (i : Fin n)
  (f : FABL.ProductL2 Ω n)
  (a : FABL.MultiIndex n ι) :
  B.fourierCoeff
      (FABL.productCoordinateLaplacian π i
        f)
      a =
    if a i ≠ B.zeroIndex then
      B.fourierCoeff f a
    else 0
    Proposition 8.23: the coordinate Laplacian retains a coefficient exactly when its `i`th
index is nonzero.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.productCoordinateLaplacian_fourier_expansion.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (i : Fin n)
  (f : FABL.ProductL2 Ω n) (x : Fin n → Ω) :
  FABL.productCoordinateLaplacian π i f x =
    ∑ a with a i ≠ B.zeroIndex,
      B.fourierCoeff f a * B.productFunction a x
    theorem FABL.FiniteFourierBasis.productCoordinateLaplacian_fourier_expansion.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (i : Fin n)
  (f : FABL.ProductL2 Ω n)
  (x : Fin n → Ω) :
  FABL.productCoordinateLaplacian π i f
      x =
    ∑ a with a i ≠ B.zeroIndex,
      B.fourierCoeff f a *
        B.productFunction a x
    Proposition 8.23: Fourier expansion of the coordinate Laplacian.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.productInfluence_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)
  (i : Fin n) :
  FABL.productInfluence π f i =
    ∑ a with a i ≠ B.zeroIndex, B.fourierCoeff f a ^ 2
    theorem FABL.FiniteFourierBasis.productInfluence_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)
  (i : Fin n) :
  FABL.productInfluence π f i =
    ∑ a with a i ≠ B.zeroIndex,
      B.fourierCoeff f a ^ 2
    Proposition 8.23: spectral formula for coordinate influence.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.productTotalInfluence_eq_sum_order_mul_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) :
  FABL.productTotalInfluence π f =
    ∑ a, ↑(FABL.multiIndexOrder B.zeroIndex a) * B.fourierCoeff f a ^ 2
    theorem FABL.FiniteFourierBasis.productTotalInfluence_eq_sum_order_mul_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) :
  FABL.productTotalInfluence π f =
    ∑ a,
      ↑(FABL.multiIndexOrder B.zeroIndex
            a) *
        B.fourierCoeff f a ^ 2
    Proposition 8.23: total influence weights each Fourier coefficient by support size.
Theorem8.2.9
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 1
Used by 3
Reverse dependency previews
Preview
Lemma 8.2.10
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-8-2fidelity-exact

Proposition 8.24. Coordinate influence is the expected conditional variance \operatorname{Inf}_i[f] =\mathbb E_{x\sim\pi^{\otimes n}} \left[ \operatorname{Var}_{x_i'\sim\pi} f(x_1,\ldots,x_{i-1},x_i',x_{i+1},\ldots,x_n) \right]. If f takes values in \{-1,1\}, then \operatorname{Inf}_i[f] =\mathbb E[|L_i f|] =2\Pr_{x,x_i'} [f(x)\ne f(x_1,\ldots,x_i',\ldots,x_n)].

Lean code for Theorem8.2.9●7 declarations
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.coordinateConditionalVariance.{u_1} {Ω : Type u_1} [Fintype Ω]
  (π : PMF Ω) {n : ℕ} (f : FABL.ProductL2 Ω n) (i : Fin n)
  (x : Fin n → Ω) : ℝ
    def FABL.coordinateConditionalVariance.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (i : Fin n) (x : Fin n → Ω) : ℝ
    Conditional variance in coordinate `i`, with the other coordinates fixed by `x`.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.HasSignRange.{u_1} {Ω : Type u_1} (f : Ω → ℝ) : Prop
    def FABL.HasSignRange.{u_1} {Ω : Type u_1}
  (f : Ω → ℝ) : Prop
    A real function has sign range when every value is `-1` or `1`.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.productInfluence_eq_expect_coordinateConditionalVariance.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (i : Fin n) :
  FABL.productInfluence π f i =
    FABL.productMean π (FABL.coordinateConditionalVariance π f i)
    theorem FABL.FiniteFourierBasis.productInfluence_eq_expect_coordinateConditionalVariance.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (i : Fin n) :
  FABL.productInfluence π f i =
    FABL.productMean π
      (FABL.coordinateConditionalVariance
        π f i)
    Proposition 8.24: influence is the expectation of the conditional coordinate variance.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productLaplacianL1.{u_1} {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f : FABL.ProductL2 Ω n) (i : Fin n) : ℝ
    def FABL.productLaplacianL1.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (i : Fin n) : ℝ
    The global weighted `L¹` norm of a coordinate Laplacian.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.productLaplacianL1_eq_influence_of_hasSignRange.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (hf : FABL.HasSignRange f) (i : Fin n) :
  FABL.productLaplacianL1 π f i = FABL.productInfluence π f i
    theorem FABL.FiniteFourierBasis.productLaplacianL1_eq_influence_of_hasSignRange.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (hf : FABL.HasSignRange f) (i : Fin n) :
  FABL.productLaplacianL1 π f i =
    FABL.productInfluence π f i
    Proposition 8.24, Boolean-valued case: influence is also the `L¹` norm of the coordinate
Laplacian.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.coordinateResamplingDisagreementProbability.{u_1} {Ω : Type u_1}
  [Fintype Ω] (π : PMF Ω) {n : ℕ} (f : FABL.ProductL2 Ω n) (i : Fin n) :
  ℝ
    def FABL.coordinateResamplingDisagreementProbability.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (i : Fin n) : ℝ
    Probability that `f(x)` changes after independently resampling coordinate `i`.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.productInfluence_eq_two_mul_resamplingDisagreement.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (hf : FABL.HasSignRange f) (i : Fin n) :
  FABL.productInfluence π f i =
    2 * FABL.coordinateResamplingDisagreementProbability π f i
    theorem FABL.FiniteFourierBasis.productInfluence_eq_two_mul_resamplingDisagreement.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (hf : FABL.HasSignRange f) (i : Fin n) :
  FABL.productInfluence π f i =
    2 *
      FABL.coordinateResamplingDisagreementProbability
        π f i
    Proposition 8.24, Boolean-valued case: influence is twice the coordinate-resampling
disagreement probability.
Lemma8.2.10
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 3
Statement dependency previews
Preview
Lemma 8.1.15
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-8-2fidelity-exact

Example 8.25. For the point indicator from Example 8.15, \operatorname{Inf}_1[f]=\frac{2}{27}. This value is obtained both from conditional variance and from the six nonzero Fourier coefficients whose first multi-index coordinate is nonzero.

Lean code for Lemma8.2.10●1 theorem
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.productInfluence_threePointBothCIndicator :
  FABL.productInfluence (FABL.uniformPMF FABL.ThreePoint)
      FABL.threePointBothCIndicator 0 =
    2 / 27
    theorem FABL.productInfluence_threePointBothCIndicator :
  FABL.productInfluence
      (FABL.uniformPMF FABL.ThreePoint)
      FABL.threePointBothCIndicator 0 =
    2 / 27
    Example 8.25: either the conditional-variance formula or the six nonconstant first-coordinate
Fourier coefficients give influence `2 / 27` for the two-site point indicator.
Definition8.2.11
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 1
Used by 4
Reverse dependency previews
Preview
Definition 8.2.12
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-8-2fidelity-exact

Definition 8.26. For \rho\in[0,1] and x\in\Omega^n, draw y\sim N_\rho(x) independently by retaining x_i with probability \rho and otherwise resampling y_i from \pi. If x\sim\pi^{\otimes n}, the pair (x,y) is a \rho-correlated pair under \pi^{\otimes n}.

Lean code for Definition8.2.11●3 definitions
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productNoiseKeepPMF (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1) : PMF Bool
    def FABL.productNoiseKeepPMF (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc 0 1) : PMF Bool
    Bernoulli law used to decide whether a coordinate is retained or resampled.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productCoordinateNoisePMF.{u_1} {Ω : Type u_1} [Fintype Ω]
  (π : PMF Ω) (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1) (x : Ω) : PMF Ω
    def FABL.productCoordinateNoisePMF.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1) (x : Ω) :
  PMF Ω
    Definition 8.26, one coordinate: retain `x` with probability `ρ`, otherwise draw afresh
from `π`.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productNoiseKernel.{u_1} {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1) (x : Fin n → Ω) :
  PMF (Fin n → Ω)
    def FABL.productNoiseKernel.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (x : Fin n → Ω) : PMF (Fin n → Ω)
    Definition 8.26: independent coordinatewise product noise `Nρ(x)`.
Definition8.2.12
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 1
Used by 4
Reverse dependency previews
Preview
Theorem 8.2.13
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-8-2fidelity-exact

Definition 8.27. The noise operator and noise stability are T_\rho f(x)=\mathbb E_{y\sim N_\rho(x)}[f(y)], \operatorname{Stab}_\rho[f] =\langle f,T_\rho f\rangle =\mathbb E_{(x,y)\ \rho\text{-correlated}}[f(x)f(y)].

Lean code for Definition8.2.12●5 declarations
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productNoiseOperator.{u_1} {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1) (f : FABL.ProductL2 Ω n) :
  FABL.ProductL2 Ω n
    def FABL.productNoiseOperator.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (f : FABL.ProductL2 Ω n) :
  FABL.ProductL2 Ω n
    Definition 8.27: the product-space noise operator as conditional expectation.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productNoiseStability.{u_1} {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1) (f : FABL.ProductL2 Ω n) : ℝ
    def FABL.productNoiseStability.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (f : FABL.ProductL2 Ω n) : ℝ
    Definition 8.27: noise stability.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.productNoiseKernel_uniformSign {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc 0 1) (x : FABL.SignCube n) :
  FABL.productNoiseKernel (FABL.uniformPMF FABL.Sign) ρ hρ x =
    FABL.resamplingNoiseKernel ρ hρ x
    theorem FABL.productNoiseKernel_uniformSign
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (x : FABL.SignCube n) :
  FABL.productNoiseKernel
      (FABL.uniformPMF FABL.Sign) ρ hρ x =
    FABL.resamplingNoiseKernel ρ hρ x
    The generic product noise kernel specializes to Chapter 2's resampling kernel.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.productNoiseOperator_uniformSign_eq_noiseOperator {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc 0 1) (f : FABL.SignCube n → ℝ) :
  FABL.productNoiseOperator (FABL.uniformPMF FABL.Sign) ρ hρ f =
    (FABL.noiseOperator ρ) f
    theorem FABL.productNoiseOperator_uniformSign_eq_noiseOperator
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (f : FABL.SignCube n → ℝ) :
  FABL.productNoiseOperator
      (FABL.uniformPMF FABL.Sign) ρ hρ f =
    (FABL.noiseOperator ρ) f
    The generic product noise operator is exactly Chapter 2's canonical Fourier multiplier on the
uniform sign cube.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.productNoiseStability_uniformSign_eq_noiseStability {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc 0 1) (f : FABL.SignCube n → ℝ) :
  FABL.productNoiseStability (FABL.uniformPMF FABL.Sign) ρ hρ f =
    FABL.noiseStability ρ ⋯ f
    theorem FABL.productNoiseStability_uniformSign_eq_noiseStability
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (f : FABL.SignCube n → ℝ) :
  FABL.productNoiseStability
      (FABL.uniformPMF FABL.Sign) ρ hρ f =
    FABL.noiseStability ρ ⋯ f
    Product noise stability specializes to Chapter 2's canonical stability.
Theorem8.2.13
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 3
Statement dependency previews
Preview
Theorem 8.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Lemma 8.2.14
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-8-2fidelity-exact

Proposition 8.28. Relative to any fixed product Fourier basis, T_\rho f =\sum_\alpha\rho^{\#\alpha}\widehat f(\alpha)\phi_\alpha, \qquad \operatorname{Stab}_\rho[f] =\sum_\alpha\rho^{\#\alpha}\widehat f(\alpha)^2.

Lean code for Theorem8.2.13●4 theorems
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.pmfExpectation_productNoiseKernel_productFunction.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc 0 1) (x : Fin n → Ω) (a : FABL.MultiIndex n ι) :
  FABL.pmfExpectation (FABL.productNoiseKernel π ρ hρ x)
      (B.productFunction a) =
    ρ ^ FABL.multiIndexOrder B.zeroIndex a * B.productFunction a x
    theorem FABL.FiniteFourierBasis.pmfExpectation_productNoiseKernel_productFunction.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (x : Fin n → Ω)
  (a : FABL.MultiIndex n ι) :
  FABL.pmfExpectation
      (FABL.productNoiseKernel π ρ hρ x)
      (B.productFunction a) =
    ρ ^
        FABL.multiIndexOrder B.zeroIndex
          a *
      B.productFunction a x
    Proposition 8.28 on a basis vector: product Fourier functions are eigenfunctions of product
noise, with eigenvalue `ρ ^ #α`.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.productNoiseOperator_fourier_expansion.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc 0 1) (f : FABL.ProductL2 Ω n) (x : Fin n → Ω) :
  FABL.productNoiseOperator π ρ hρ f x =
    ∑ a,
      ρ ^ FABL.multiIndexOrder B.zeroIndex a * B.fourierCoeff f a *
        B.productFunction a x
    theorem FABL.FiniteFourierBasis.productNoiseOperator_fourier_expansion.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (f : FABL.ProductL2 Ω n)
  (x : Fin n → Ω) :
  FABL.productNoiseOperator π ρ hρ f x =
    ∑ a,
      ρ ^
            FABL.multiIndexOrder
              B.zeroIndex a *
          B.fourierCoeff f a *
        B.productFunction a x
    Proposition 8.28: pointwise spectral expansion of the product noise operator.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.fourierCoeff_productNoiseOperator.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc 0 1) (f : FABL.ProductL2 Ω n)
  (a : FABL.MultiIndex n ι) :
  B.fourierCoeff (FABL.productNoiseOperator π ρ hρ f) a =
    ρ ^ FABL.multiIndexOrder B.zeroIndex a * B.fourierCoeff f a
    theorem FABL.FiniteFourierBasis.fourierCoeff_productNoiseOperator.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (f : FABL.ProductL2 Ω n)
  (a : FABL.MultiIndex n ι) :
  B.fourierCoeff
      (FABL.productNoiseOperator π ρ hρ f)
      a =
    ρ ^
        FABL.multiIndexOrder B.zeroIndex
          a *
      B.fourierCoeff f a
    The Fourier coefficient of product noise is multiplied by `ρ ^ #α`.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.productNoiseStability_eq_sum.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc 0 1) (f : FABL.ProductL2 Ω n) :
  FABL.productNoiseStability π ρ hρ f =
    ∑ a, ρ ^ FABL.multiIndexOrder B.zeroIndex a * B.fourierCoeff f a ^ 2
    theorem FABL.FiniteFourierBasis.productNoiseStability_eq_sum.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (f : FABL.ProductL2 Ω n) :
  FABL.productNoiseStability π ρ hρ f =
    ∑ a,
      ρ ^
          FABL.multiIndexOrder B.zeroIndex
            a *
        B.fourierCoeff f a ^ 2
    Proposition 8.28: spectral formula for product-space noise stability.
Lemma8.2.14
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 0✓L∃∀N
Tagssection-8-2fidelity-exact

Remark 8.29. The Fourier-multiplier formula in Proposition 8.28 extends the definition of T_\rho to real parameters outside [0,1], even when there is no associated resampling kernel.

Lean code for Lemma8.2.14●2 declarations
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.spectralProductNoiseOperator.{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.ProductL2 Ω n
    def FABL.spectralProductNoiseOperator.{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.ProductL2 Ω n
    The all-real spectral noise multiplier. It is introduced before the coordinatewise operators
because Exercise 8.11 identifies constant anisotropic parameters with this operator.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.spectralProductNoiseOperator_eq_productNoiseOperator.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc 0 1) (f : FABL.ProductL2 Ω n) :
  FABL.spectralProductNoiseOperator B ρ f =
    FABL.productNoiseOperator π ρ hρ f
    theorem FABL.spectralProductNoiseOperator_eq_productNoiseOperator.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (f : FABL.ProductL2 Ω n) :
  FABL.spectralProductNoiseOperator B ρ
      f =
    FABL.productNoiseOperator π ρ hρ f
    On `[0,1]`, the spectral extension agrees with the probabilistic product noise operator.
Definition8.2.15
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 3
Statement dependency previews
Preview
Definition 8.2.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 8.2.16
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-8-2fidelity-exact

Definition 8.30. For \rho\in(0,1], define \operatorname{Inf}_i^{(\rho)}[f] =\rho^{-1}\operatorname{Stab}_\rho[L_i f] =\sum_{\alpha:\alpha_i\ne0} \rho^{\#\alpha-1}\widehat f(\alpha)^2, and \mathbf I^{(\rho)}[f]=\sum_i\operatorname{Inf}_i^{(\rho)}[f].

Lean code for Definition8.2.15●5 declarations
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productStableInfluence.{u_1} {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Ioc 0 1) (f : FABL.ProductL2 Ω n)
  (i : Fin n) : ℝ
    def FABL.productStableInfluence.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Ioc 0 1)
  (f : FABL.ProductL2 Ω n) (i : Fin n) : ℝ
    Definition 8.30, basis-free form: `ρ⁻¹ Stabρ[Lᵢf]` for `ρ ∈ (0,1]`.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productTotalStableInfluence.{u_1} {Ω : Type u_1} [Fintype Ω]
  (π : PMF Ω) {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Ioc 0 1)
  (f : FABL.ProductL2 Ω n) : ℝ
    def FABL.productTotalStableInfluence.{u_1}
  {Ω : Type u_1} [Fintype Ω] (π : PMF Ω)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Ioc 0 1)
  (f : FABL.ProductL2 Ω n) : ℝ
    Total stable influence.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.stableInfluencePolynomial.{u_1, u_2} {Ω : Type u_1} [Fintype Ω]
  [Nonempty Ω] {π : PMF Ω} {ι : Type u_2} [Fintype ι] [Nonempty ι]
  [DecidableEq ι] (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (ρ : ℝ)
  (f : FABL.ProductL2 Ω n) (i : Fin n) : ℝ
    def FABL.stableInfluencePolynomial.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (ρ : ℝ) (f : FABL.ProductL2 Ω n)
  (i : Fin n) : ℝ
    The spectral stable-influence polynomial, defined for every real `ρ`. On `(0,1]` this is the
basis-free stable influence; at `ρ = 0` it gives Exercise 8.13's continuous extension.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.productStableInfluence_eq_polynomial.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Ioc 0 1) (f : FABL.ProductL2 Ω n) (i : Fin n) :
  FABL.productStableInfluence π ρ hρ f i =
    FABL.stableInfluencePolynomial B ρ f i
    theorem FABL.FiniteFourierBasis.productStableInfluence_eq_polynomial.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Ioc 0 1)
  (f : FABL.ProductL2 Ω n) (i : Fin n) :
  FABL.productStableInfluence π ρ hρ f i =
    FABL.stableInfluencePolynomial B ρ f i
    Definition 8.30: the basis-free stable influence has the expected spectral formula.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.productTotalStableInfluence_eq_sum.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (ρ : ℝ)
  (hρ : ρ ∈ Set.Ioc 0 1) (f : FABL.ProductL2 Ω n) :
  FABL.productTotalStableInfluence π ρ hρ f =
    ∑ a,
      ↑(FABL.multiIndexOrder B.zeroIndex a) *
          ρ ^ (FABL.multiIndexOrder B.zeroIndex a - 1) *
        B.fourierCoeff f a ^ 2
    theorem FABL.FiniteFourierBasis.productTotalStableInfluence_eq_sum.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Ioc 0 1)
  (f : FABL.ProductL2 Ω n) :
  FABL.productTotalStableInfluence π ρ hρ
      f =
    ∑ a,
      ↑(FABL.multiIndexOrder B.zeroIndex
              a) *
          ρ ^
            (FABL.multiIndexOrder
                B.zeroIndex a -
              1) *
        B.fourierCoeff f a ^ 2
    Total stable influence is the support-order weighted Fourier sum.
Theorem8.2.16
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.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-8-2fidelity-exact

Proposition 8.31. Suppose \operatorname{Var}[f]\le1, let 0<\delta<1, 0<\epsilon\le1, and set J=\{i:\operatorname{Inf}_i^{(1-\delta)}[f]\ge\epsilon\}. Then |J|\le\frac1{\delta\epsilon}.

Lean code for Theorem8.2.16●2 theorems
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.productTotalStableInfluence_one_sub_le_inv.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (hvar : FABL.productVariance π f ≤ 1) (δ : ℝ) (hδ : δ ∈ Set.Ioo 0 1) :
  FABL.productTotalStableInfluence π (1 - δ) ⋯ f ≤ 1 / δ
    theorem FABL.FiniteFourierBasis.productTotalStableInfluence_one_sub_le_inv.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (hvar : FABL.productVariance π f ≤ 1)
  (δ : ℝ) (hδ : δ ∈ Set.Ioo 0 1) :
  FABL.productTotalStableInfluence π
      (1 - δ) ⋯ f ≤
    1 / δ
    The total `(1-δ)`-stable influence is at most `1/δ` when variance is at most one. The
arithmetic kernel is reused from Chapter 2's `card_mul_one_sub_pow_le_inv`.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.card_stableInfluencePolynomial_ge_le.{u_1, u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2}
  [Fintype ι] [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι) {n : ℕ} (f : FABL.ProductL2 Ω n)
  (hvar : FABL.productVariance π f ≤ 1) (δ ε : ℝ) (hδ : δ ∈ Set.Ioo 0 1)
  (hε : ε ∈ Set.Ioc 0 1) :
  ↑{i | ε ≤ FABL.stableInfluencePolynomial B (1 - δ) f i}.card ≤
    1 / (δ * ε)
    theorem FABL.FiniteFourierBasis.card_stableInfluencePolynomial_ge_le.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n)
  (hvar : FABL.productVariance π f ≤ 1)
  (δ ε : ℝ) (hδ : δ ∈ Set.Ioo 0 1)
  (hε : ε ∈ Set.Ioc 0 1) :
  ↑{i |
          ε ≤
            FABL.stableInfluencePolynomial
              B (1 - δ) f i}.card ≤
    1 / (δ * ε)
    Proposition 8.31: at most `1/(δ ε)` coordinates have stable influence at least `ε`.
Definition8.2.17
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 1
Used by 3
Reverse dependency previews
Preview
Theorem 8.2.18
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-8-2fidelity-exact

Definition 8.32. For nonzero f\in L^2(\Omega^n,\pi^{\otimes n}), the degree \deg(f) is the least k\in\mathbb N for which f is a finite sum of functions depending on at most k coordinates.

Lean code for Definition8.2.17●4 declarations
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.IsSumOfJuntasAtMost.{u_1} {Ω : Type u_1} {n : ℕ}
  (f : FABL.ProductL2 Ω n) (k : ℕ) : Prop
    def FABL.IsSumOfJuntasAtMost.{u_1}
  {Ω : Type u_1} {n : ℕ}
  (f : FABL.ProductL2 Ω n) (k : ℕ) : Prop
    A function is a sum of `k`-juntas when it is the sum of one term for each coordinate set,
with the `J` term depending only on `J` and vanishing when `|J| > k`. This is a finite,
basis-free formulation of Definition 8.32.
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.productDegree.{u_1} {Ω : Type u_1} {n : ℕ}
  (f : FABL.ProductL2 Ω n) : ℕ
    def FABL.productDegree.{u_1} {Ω : Type u_1}
  {n : ℕ} (f : FABL.ProductL2 Ω n) : ℕ
    O'Donnell, Definition 8.32: the least junta size whose junta sums contain `f`.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.isSumOfJuntasAtMost_productDegree.{u_1} {Ω : Type u_1} {n : ℕ}
  (f : FABL.ProductL2 Ω n) :
  FABL.IsSumOfJuntasAtMost f (FABL.productDegree f)
    theorem FABL.isSumOfJuntasAtMost_productDegree.{u_1}
  {Ω : Type u_1} {n : ℕ}
  (f : FABL.ProductL2 Ω n) :
  FABL.IsSumOfJuntasAtMost f
    (FABL.productDegree f)
    The defining witness for basis-free degree.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.productDegree_le_of_isSumOfJuntasAtMost.{u_1} {Ω : Type u_1}
  {n : ℕ} {f : FABL.ProductL2 Ω n} {k : ℕ}
  (hf : FABL.IsSumOfJuntasAtMost f k) : FABL.productDegree f ≤ k
    theorem FABL.productDegree_le_of_isSumOfJuntasAtMost.{u_1}
  {Ω : Type u_1} {n : ℕ}
  {f : FABL.ProductL2 Ω n} {k : ℕ}
  (hf : FABL.IsSumOfJuntasAtMost f k) :
  FABL.productDegree f ≤ k
    Basis-free degree is minimal among all junta-sum bounds.
Theorem8.2.18
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 3
Statement dependency previews
Preview
Definition 8.1.14
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-8-2fidelity-exact

Proposition 8.33. For every fixed product Fourier basis and every nonzero f, \deg(f)=\max\{\#\alpha:\widehat f(\alpha)\ne0\}.

Lean code for Theorem8.2.18●3 declarations
  • defdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    def FABL.FiniteFourierBasis.spectralDegree.{u_1, u_2} {Ω : Type u_1}
  [Fintype Ω] [Nonempty Ω] {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι] (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n) : ℕ
    def FABL.FiniteFourierBasis.spectralDegree.{u_1,
    u_2}
  {Ω : Type u_1} [Fintype Ω] [Nonempty Ω]
  {π : PMF Ω} {ι : Type u_2} [Fintype ι]
  [Nonempty ι] [DecidableEq ι]
  (B : FABL.FiniteFourierBasis Ω π ι)
  {n : ℕ} (f : FABL.ProductL2 Ω n) : ℕ
    Spectral degree: maximum support order of a nonzero Fourier coefficient.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.spectralDegree_le_iff.{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.spectralDegree f ≤ k ↔
    ∀ (a : FABL.MultiIndex n ι),
      k < FABL.multiIndexOrder B.zeroIndex a → B.fourierCoeff f a = 0
    theorem FABL.FiniteFourierBasis.spectralDegree_le_iff.{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.spectralDegree f ≤ k ↔
    ∀ (a : FABL.MultiIndex n ι),
      k <
          FABL.multiIndexOrder B.zeroIndex
            a →
        B.fourierCoeff f a = 0
    Spectral degree is at most `k` exactly when all coefficients above order `k` vanish.
  • theoremdefined in FABL/Chapter08/GeneralizedFourierFormulas.lean
    complete
    theorem FABL.FiniteFourierBasis.productDegree_eq_spectralDegree.{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.productDegree f = B.spectralDegree f
    theorem FABL.FiniteFourierBasis.productDegree_eq_spectralDegree.{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.productDegree f =
    B.spectralDegree f
    Proposition 8.33: basis-free junta-sum degree equals maximum Fourier support order for every
product Fourier basis.