Analysis of Boolean Functions in Lean

9.4. Two-function hypercontractivity and induction🔗

Lemma9.4.1
Group: Chapter 9: Basics of hypercontractivity (100)
Group member previews
Preview
Theorem 9.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 2.4.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-9-4supportfidelity-exactreused-canonical-declaration

For all real parameters \rho,\sigma, the Boolean-cube noise operators form a multiplicative semigroup: T_\rho(T_\sigma f)=T_{\rho\sigma}f.

Lean code for Lemma9.4.1●1 theorem
  • theoremdefined in FABL/Chapter04/KKL.lean
    complete
    theorem FABL.noiseOperator_comp {n : ℕ} (rho sigma : ℝ)
  (f : FABL.SignCube n → ℝ) :
  (FABL.noiseOperator rho) ((FABL.noiseOperator sigma) f) =
    (FABL.noiseOperator (rho * sigma)) f
    theorem FABL.noiseOperator_comp {n : ℕ}
  (rho sigma : ℝ)
  (f : FABL.SignCube n → ℝ) :
  (FABL.noiseOperator rho)
      ((FABL.noiseOperator sigma) f) =
    (FABL.noiseOperator (rho * sigma)) f
    Noise operators form a multiplicative semigroup.
Lemma9.4.2
Group: Chapter 9: Basics of hypercontractivity (100)
Group member previews
Preview
Theorem 9.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N
Tagssection-9-4supportfidelity-exact

If (x,y) is a \rho-correlated pair, then \mathbb E[f(x)g(y)] \le\|f\|_{1+\rho}\|g\|_{1+\rho}. \tag{9.12}

Lean code for Lemma9.4.2●3 theorems
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.equation9_12_oneBit (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (f g : FABL.Sign → ℝ) :
  FABL.pmfCouplingInner (FABL.correlatedSignPairPMF ρ ⋯) f g ≤
    FABL.pmfLpNorm (FABL.uniformPMF FABL.Sign) (1 + ρ) f *
      FABL.pmfLpNorm (FABL.uniformPMF FABL.Sign) (1 + ρ) g
    theorem FABL.equation9_12_oneBit (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc 0 1)
  (f g : FABL.Sign → ℝ) :
  FABL.pmfCouplingInner
      (FABL.correlatedSignPairPMF ρ ⋯) f
      g ≤
    FABL.pmfLpNorm
        (FABL.uniformPMF FABL.Sign)
        (1 + ρ) f *
      FABL.pmfLpNorm
        (FABL.uniformPMF FABL.Sign)
        (1 + ρ) g
    Equation (9.12) on one sign.
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.equation9_12 (n : ℕ) (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (f g : FABL.SignCube n → ℝ) :
  FABL.iteratedCouplingInner (FABL.correlatedSignPairPMF ρ ⋯) n f g ≤
    FABL.iteratedPmfLpNorm (FABL.uniformPMF FABL.Sign) n (1 + ρ) f *
      FABL.iteratedPmfLpNorm (FABL.uniformPMF FABL.Sign) n (1 + ρ) g
    theorem FABL.equation9_12 (n : ℕ) (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc 0 1)
  (f g : FABL.SignCube n → ℝ) :
  FABL.iteratedCouplingInner
      (FABL.correlatedSignPairPMF ρ ⋯) n f
      g ≤
    FABL.iteratedPmfLpNorm
        (FABL.uniformPMF FABL.Sign) n
        (1 + ρ) f *
      FABL.iteratedPmfLpNorm
        (FABL.uniformPMF FABL.Sign) n
        (1 + ρ) g
    Equation (9.12) in the recursive finite-product presentation.
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.equation9_12_signCube (n : ℕ) (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1)
  (f g : FABL.SignCube n → ℝ) :
  (FABL.pmfExpectation (FABL.correlatedPairPMF ρ ⋯) fun xy =>
      f xy.1 * g xy.2) ≤
    FABL.uniformLpNorm (1 + ρ) f * FABL.uniformLpNorm (1 + ρ) g
    theorem FABL.equation9_12_signCube (n : ℕ) (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc 0 1)
  (f g : FABL.SignCube n → ℝ) :
  (FABL.pmfExpectation
      (FABL.correlatedPairPMF ρ ⋯)
      fun xy => f xy.1 * g xy.2) ≤
    FABL.uniformLpNorm (1 + ρ) f *
      FABL.uniformLpNorm (1 + ρ) g
    Equation (9.12) on the canonical Boolean cube.
Theorem9.4.3
Group: Chapter 9: Basics of hypercontractivity (100)
Group member previews
Preview
Theorem 9.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 9.3.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-9-4fidelity-exact

Weak Two-Function Hypercontractivity Theorem. Let f,g:\{-1,1\}^n\to\mathbb R, 0\le r,s\le1, and 0\le\rho\le\sqrt{rs}. Then \mathbb E_{(x,y)\ \rho\text{-correlated}}[f(x)g(y)] \le\|f\|_{1+r}\|g\|_{1+s}.

Lean code for Theorem9.4.3●3 theorems
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.weakTwoFunctionHypercontractivity_oneBit (r s ρ : ℝ)
  (hr : r ∈ Set.Icc 0 1) (hs : s ∈ Set.Icc 0 1) (hρ0 : 0 ≤ ρ)
  (hρ : ρ ≤ √(r * s)) (f g : FABL.Sign → ℝ) :
  FABL.pmfCouplingInner (FABL.correlatedSignPairPMF ρ ⋯) f g ≤
    FABL.pmfLpNorm (FABL.uniformPMF FABL.Sign) (1 + r) f *
      FABL.pmfLpNorm (FABL.uniformPMF FABL.Sign) (1 + s) g
    theorem FABL.weakTwoFunctionHypercontractivity_oneBit
  (r s ρ : ℝ) (hr : r ∈ Set.Icc 0 1)
  (hs : s ∈ Set.Icc 0 1) (hρ0 : 0 ≤ ρ)
  (hρ : ρ ≤ √(r * s))
  (f g : FABL.Sign → ℝ) :
  FABL.pmfCouplingInner
      (FABL.correlatedSignPairPMF ρ ⋯) f
      g ≤
    FABL.pmfLpNorm
        (FABL.uniformPMF FABL.Sign)
        (1 + r) f *
      FABL.pmfLpNorm
        (FABL.uniformPMF FABL.Sign)
        (1 + s) g
    The Weak Two-Function Hypercontractivity Theorem on one uniform sign.
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.weakTwoFunctionHypercontractivity (n : ℕ) (r s ρ : ℝ)
  (hr : r ∈ Set.Icc 0 1) (hs : s ∈ Set.Icc 0 1) (hρ0 : 0 ≤ ρ)
  (hρ : ρ ≤ √(r * s)) (f g : FABL.SignCube n → ℝ) :
  FABL.iteratedCouplingInner (FABL.correlatedSignPairPMF ρ ⋯) n f g ≤
    FABL.iteratedPmfLpNorm (FABL.uniformPMF FABL.Sign) n (1 + r) f *
      FABL.iteratedPmfLpNorm (FABL.uniformPMF FABL.Sign) n (1 + s) g
    theorem FABL.weakTwoFunctionHypercontractivity
  (n : ℕ) (r s ρ : ℝ)
  (hr : r ∈ Set.Icc 0 1)
  (hs : s ∈ Set.Icc 0 1) (hρ0 : 0 ≤ ρ)
  (hρ : ρ ≤ √(r * s))
  (f g : FABL.SignCube n → ℝ) :
  FABL.iteratedCouplingInner
      (FABL.correlatedSignPairPMF ρ ⋯) n f
      g ≤
    FABL.iteratedPmfLpNorm
        (FABL.uniformPMF FABL.Sign) n
        (1 + r) f *
      FABL.iteratedPmfLpNorm
        (FABL.uniformPMF FABL.Sign) n
        (1 + s) g
    The full Weak Two-Function Hypercontractivity Theorem in the recursive finite-product
presentation used by the restriction induction.
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.weakTwoFunctionHypercontractivity_signCube (n : ℕ) (r s ρ : ℝ)
  (hr : r ∈ Set.Icc 0 1) (hs : s ∈ Set.Icc 0 1) (hρ0 : 0 ≤ ρ)
  (hρ : ρ ≤ √(r * s)) (f g : FABL.SignCube n → ℝ) :
  (FABL.pmfExpectation (FABL.correlatedPairPMF ρ ⋯) fun xy =>
      f xy.1 * g xy.2) ≤
    FABL.uniformLpNorm (1 + r) f * FABL.uniformLpNorm (1 + s) g
    theorem FABL.weakTwoFunctionHypercontractivity_signCube
  (n : ℕ) (r s ρ : ℝ)
  (hr : r ∈ Set.Icc 0 1)
  (hs : s ∈ Set.Icc 0 1) (hρ0 : 0 ≤ ρ)
  (hρ : ρ ≤ √(r * s))
  (f g : FABL.SignCube n → ℝ) :
  (FABL.pmfExpectation
      (FABL.correlatedPairPMF ρ ⋯)
      fun xy => f xy.1 * g xy.2) ≤
    FABL.uniformLpNorm (1 + r) f *
      FABL.uniformLpNorm (1 + s) g
    The Weak Two-Function Hypercontractivity Theorem on the canonical Boolean cube.
Theorem9.4.4
Group: Chapter 9: Basics of hypercontractivity (100)
Group member previews
Preview
Theorem 9.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 9.1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-9-4fidelity-exact

Two-Function Hypercontractivity Induction Theorem. Suppose that on a probability space (\Omega,\pi) one has, for every f,g, \mathbb E_{\rho\text{-correlated}}[f(x)g(y)] \le\|f\|_p\|g\|_q. Then the same inequality holds for every pair of functions on (\Omega^n,\pi^{\otimes n}), for every n.

Lean code for Theorem9.4.4●8 declarations
  • defdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    def FABL.pmfCouplingInner.{u_1} {Ω : Type u_1} [Fintype Ω] (κ : PMF (Ω × Ω))
  (f g : Ω → ℝ) : ℝ
    def FABL.pmfCouplingInner.{u_1} {Ω : Type u_1}
  [Fintype Ω] (κ : PMF (Ω × Ω))
  (f g : Ω → ℝ) : ℝ
    The two-function expectation associated with a finite coupling on `Ω × Ω`.
  • defdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    def FABL.pmfProductLaw.{u_1, u_2} {A : Type u_1} {B : Type u_2} [Fintype A]
  [Fintype B] (lawA : PMF A) (lawB : PMF B) : PMF (A × B)
    def FABL.pmfProductLaw.{u_1, u_2}
  {A : Type u_1} {B : Type u_2}
  [Fintype A] [Fintype B] (lawA : PMF A)
  (lawB : PMF B) : PMF (A × B)
    Independent product of two finite PMFs, represented on an ordinary product type.
  • defdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    def FABL.pmfProductCoupling.{u_1, u_2} {A : Type u_1} {B : Type u_2}
  [Fintype A] [Fintype B] (κA : PMF (A × A)) (κB : PMF (B × B)) :
  PMF ((A × B) × A × B)
    def FABL.pmfProductCoupling.{u_1, u_2}
  {A : Type u_1} {B : Type u_2}
  [Fintype A] [Fintype B]
  (κA : PMF (A × A)) (κB : PMF (B × B)) :
  PMF ((A × B) × A × B)
    Product of two couplings, reordered as a coupling of ordinary product spaces.
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.twoFunctionHypercontractivity_product.{u_1, u_2} {A : Type u_1}
  {B : Type u_2} [Fintype A] [Fintype B] (lawA : PMF A) (lawB : PMF B)
  (κA : PMF (A × A)) (κB : PMF (B × B)) (p q : ℝ) (hp : 0 < p)
  (hq : 0 < q)
  (hA :
    ∀ (f g : A → ℝ),
      FABL.pmfCouplingInner κA f g ≤
        FABL.pmfLpNorm lawA p f * FABL.pmfLpNorm lawA q g)
  (hB :
    ∀ (f g : B → ℝ),
      FABL.pmfCouplingInner κB f g ≤
        FABL.pmfLpNorm lawB p f * FABL.pmfLpNorm lawB q g)
  (f g : A × B → ℝ) :
  FABL.pmfCouplingInner (FABL.pmfProductCoupling κA κB) f g ≤
    FABL.pmfLpNorm (FABL.pmfProductLaw lawA lawB) p f *
      FABL.pmfLpNorm (FABL.pmfProductLaw lawA lawB) q g
    theorem FABL.twoFunctionHypercontractivity_product.{u_1,
    u_2}
  {A : Type u_1} {B : Type u_2}
  [Fintype A] [Fintype B] (lawA : PMF A)
  (lawB : PMF B) (κA : PMF (A × A))
  (κB : PMF (B × B)) (p q : ℝ)
  (hp : 0 < p) (hq : 0 < q)
  (hA :
    ∀ (f g : A → ℝ),
      FABL.pmfCouplingInner κA f g ≤
        FABL.pmfLpNorm lawA p f *
          FABL.pmfLpNorm lawA q g)
  (hB :
    ∀ (f g : B → ℝ),
      FABL.pmfCouplingInner κB f g ≤
        FABL.pmfLpNorm lawB p f *
          FABL.pmfLpNorm lawB q g)
  (f g : A × B → ℝ) :
  FABL.pmfCouplingInner
      (FABL.pmfProductCoupling κA κB) f
      g ≤
    FABL.pmfLpNorm
        (FABL.pmfProductLaw lawA lawB) p
        f *
      FABL.pmfLpNorm
        (FABL.pmfProductLaw lawA lawB) q g
    Remark 9.20, binary heterogeneous tensor step: two base inequalities tensorize over the
product probability space.  Iterating this theorem gives the book's heterogeneous product.
  • defdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    def FABL.iteratedPmfLpNorm.{u_1} {Ω : Type u_1} [Fintype Ω] (law : PMF Ω)
  (n : ℕ) : ℝ → ((Fin n → Ω) → ℝ) → ℝ
    def FABL.iteratedPmfLpNorm.{u_1}
  {Ω : Type u_1} [Fintype Ω] (law : PMF Ω)
  (n : ℕ) : ℝ → ((Fin n → Ω) → ℝ) → ℝ
    The recursively nested `L^p` norm on `n` independent copies of `(Ω, law)`.
The last coordinate is integrated first in the induction step.
  • defdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    def FABL.iteratedCouplingInner.{u_1} {Ω : Type u_1} [Fintype Ω]
  (κ : PMF (Ω × Ω)) (n : ℕ) : ((Fin n → Ω) → ℝ) → ((Fin n → Ω) → ℝ) → ℝ
    def FABL.iteratedCouplingInner.{u_1}
  {Ω : Type u_1} [Fintype Ω]
  (κ : PMF (Ω × Ω)) (n : ℕ) :
  ((Fin n → Ω) → ℝ) →
    ((Fin n → Ω) → ℝ) → ℝ
    The recursively nested two-function expectation for `n` independent copies of a coupling.
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.twoFunctionHypercontractivity_induction.{u_1} {Ω : Type u_1}
  [Fintype Ω] (law : PMF Ω) (κ : PMF (Ω × Ω)) (p q : ℝ)
  (hbase :
    ∀ (f g : Ω → ℝ),
      FABL.pmfCouplingInner κ f g ≤
        FABL.pmfLpNorm law p f * FABL.pmfLpNorm law q g)
  (n : ℕ) (f g : (Fin n → Ω) → ℝ) :
  FABL.iteratedCouplingInner κ n f g ≤
    FABL.iteratedPmfLpNorm law n p f * FABL.iteratedPmfLpNorm law n q g
    theorem FABL.twoFunctionHypercontractivity_induction.{u_1}
  {Ω : Type u_1} [Fintype Ω] (law : PMF Ω)
  (κ : PMF (Ω × Ω)) (p q : ℝ)
  (hbase :
    ∀ (f g : Ω → ℝ),
      FABL.pmfCouplingInner κ f g ≤
        FABL.pmfLpNorm law p f *
          FABL.pmfLpNorm law q g)
  (n : ℕ) (f g : (Fin n → Ω) → ℝ) :
  FABL.iteratedCouplingInner κ n f g ≤
    FABL.iteratedPmfLpNorm law n p f *
      FABL.iteratedPmfLpNorm law n q g
    O'Donnell's Two-Function Hypercontractivity Induction Theorem for a finite base coupling.
No symmetry or special formula for the coupling is needed: positivity of its PMF is exactly what
makes the restriction induction tensorize.
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.twoFunctionHypercontractivity_product_induction.{u_1}
  {Ω : Type u_1} [Fintype Ω] (law : PMF Ω) (κ : PMF (Ω × Ω)) (p q : ℝ)
  (hp : 0 < p) (hq : 0 < q)
  (hbase :
    ∀ (f g : Ω → ℝ),
      FABL.pmfCouplingInner κ f g ≤
        FABL.pmfLpNorm law p f * FABL.pmfLpNorm law q g)
  (n : ℕ) (f g : (Fin n → Ω) → ℝ) :
  (FABL.pmfExpectation (FABL.productProbabilityPMF κ n) fun z =>
      f (FABL.pairVectorFst z) * g (FABL.pairVectorSnd z)) ≤
    FABL.productLpNorm law n p f * FABL.productLpNorm law n q g
    theorem FABL.twoFunctionHypercontractivity_product_induction.{u_1}
  {Ω : Type u_1} [Fintype Ω] (law : PMF Ω)
  (κ : PMF (Ω × Ω)) (p q : ℝ) (hp : 0 < p)
  (hq : 0 < q)
  (hbase :
    ∀ (f g : Ω → ℝ),
      FABL.pmfCouplingInner κ f g ≤
        FABL.pmfLpNorm law p f *
          FABL.pmfLpNorm law q g)
  (n : ℕ) (f g : (Fin n → Ω) → ℝ) :
  (FABL.pmfExpectation
      (FABL.productProbabilityPMF κ n)
      fun z =>
      f (FABL.pairVectorFst z) *
        g (FABL.pairVectorSnd z)) ≤
    FABL.productLpNorm law n p f *
      FABL.productLpNorm law n q g
    O'Donnell's Two-Function Hypercontractivity Induction Theorem in Chapter 8's standard
product-PMF presentation.
Lemma9.4.5
Group: Chapter 9: Basics of hypercontractivity (100)
Group member previews
Preview
Theorem 9.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
Tagssection-9-4fidelity-exact

Remark 9.20. The induction is heterogeneous: if the base inequality holds on each (\Omega_i,\pi_i), it holds on \prod_i\Omega_i \quad\text{with law}\quad \bigotimes_i\pi_i.

Lean code for Lemma9.4.5●4 theorems
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.pmfExpectation_productLaw.{u_1, u_2} {A : Type u_1} {B : Type u_2}
  [Fintype A] [Fintype B] (lawA : PMF A) (lawB : PMF B)
  (f : A × B → ℝ) :
  FABL.pmfExpectation (FABL.pmfProductLaw lawA lawB) f =
    FABL.pmfExpectation lawA fun a =>
      FABL.pmfExpectation lawB fun b => f (a, b)
    theorem FABL.pmfExpectation_productLaw.{u_1, u_2}
  {A : Type u_1} {B : Type u_2}
  [Fintype A] [Fintype B] (lawA : PMF A)
  (lawB : PMF B) (f : A × B → ℝ) :
  FABL.pmfExpectation
      (FABL.pmfProductLaw lawA lawB) f =
    FABL.pmfExpectation lawA fun a =>
      FABL.pmfExpectation lawB fun b =>
        f (a, b)
    Fubini's identity for the ordinary two-factor PMF product.
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.pmfLpNorm_productLaw.{u_1, u_2} {A : Type u_1} {B : Type u_2}
  [Fintype A] [Fintype B] (lawA : PMF A) (lawB : PMF B) (p : ℝ)
  (hp : 0 < p) (f : A × B → ℝ) :
  FABL.pmfLpNorm (FABL.pmfProductLaw lawA lawB) p f =
    FABL.pmfLpNorm lawA p fun a =>
      FABL.pmfLpNorm lawB p fun b => f (a, b)
    theorem FABL.pmfLpNorm_productLaw.{u_1, u_2}
  {A : Type u_1} {B : Type u_2}
  [Fintype A] [Fintype B] (lawA : PMF A)
  (lawB : PMF B) (p : ℝ) (hp : 0 < p)
  (f : A × B → ℝ) :
  FABL.pmfLpNorm
      (FABL.pmfProductLaw lawA lawB) p f =
    FABL.pmfLpNorm lawA p fun a =>
      FABL.pmfLpNorm lawB p fun b =>
        f (a, b)
    A same-exponent nested norm is the ordinary `L^p` norm for the two-factor product law.
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.iteratedPmfLpNorm_eq_productLpNorm.{u_1} {Ω : Type u_1} [Fintype Ω]
  (law : PMF Ω) (n : ℕ) (p : ℝ) (hp : 0 < p) (f : (Fin n → Ω) → ℝ) :
  FABL.iteratedPmfLpNorm law n p f = FABL.productLpNorm law n p f
    theorem FABL.iteratedPmfLpNorm_eq_productLpNorm.{u_1}
  {Ω : Type u_1} [Fintype Ω] (law : PMF Ω)
  (n : ℕ) (p : ℝ) (hp : 0 < p)
  (f : (Fin n → Ω) → ℝ) :
  FABL.iteratedPmfLpNorm law n p f =
    FABL.productLpNorm law n p f
    The recursively nested norm agrees with Chapter 8's product-law `L^p` norm.
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.iteratedCouplingInner_eq_productProbabilityPMF.{u_1} {Ω : Type u_1}
  [Fintype Ω] (κ : PMF (Ω × Ω)) (n : ℕ) (f g : (Fin n → Ω) → ℝ) :
  FABL.iteratedCouplingInner κ n f g =
    FABL.pmfExpectation (FABL.productProbabilityPMF κ n) fun z =>
      f (FABL.pairVectorFst z) * g (FABL.pairVectorSnd z)
    theorem FABL.iteratedCouplingInner_eq_productProbabilityPMF.{u_1}
  {Ω : Type u_1} [Fintype Ω]
  (κ : PMF (Ω × Ω)) (n : ℕ)
  (f g : (Fin n → Ω) → ℝ) :
  FABL.iteratedCouplingInner κ n f g =
    FABL.pmfExpectation
      (FABL.productProbabilityPMF κ n)
      fun z =>
      f (FABL.pairVectorFst z) *
        g (FABL.pairVectorSnd z)
    The recursively nested coupling expectation is expectation under the independent product
of the one-coordinate coupling.
Theorem9.4.6
Group: Chapter 9: Basics of hypercontractivity (100)
Group member previews
Preview
Theorem 9.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 9.3.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-9-4supportfidelity-exact

Taking g=f and r=s=\rho in the two-function inequality yields the full n-bit (p,2) theorem. Self-adjoint duality then yields the n-bit (2,q) theorem.

Lean code for Theorem9.4.6●4 theorems
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.productProbabilityPMF_correlatedSignPair_map (n : ℕ) (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1) :
  PMF.map (⇑(FABL.signPairVectorEquiv n))
      (FABL.productProbabilityPMF (FABL.correlatedSignPairPMF ρ hρ) n) =
    FABL.correlatedPairPMF ρ hρ
    theorem FABL.productProbabilityPMF_correlatedSignPair_map
  (n : ℕ) (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1) :
  PMF.map (⇑(FABL.signPairVectorEquiv n))
      (FABL.productProbabilityPMF
        (FABL.correlatedSignPairPMF ρ hρ)
        n) =
    FABL.correlatedPairPMF ρ hρ
    The independent product of the one-coordinate correlated-sign laws is Chapter 2's
canonical correlated-pair law on the sign cube.
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.iteratedCouplingInner_correlatedSign_eq_correlatedPair (n : ℕ)
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) (f g : FABL.SignCube n → ℝ) :
  FABL.iteratedCouplingInner (FABL.correlatedSignPairPMF ρ hρ) n f g =
    FABL.pmfExpectation (FABL.correlatedPairPMF ρ hρ) fun xy =>
      f xy.1 * g xy.2
    theorem FABL.iteratedCouplingInner_correlatedSign_eq_correlatedPair
  (n : ℕ) (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1)
  (f g : FABL.SignCube n → ℝ) :
  FABL.iteratedCouplingInner
      (FABL.correlatedSignPairPMF ρ hρ) n
      f g =
    FABL.pmfExpectation
      (FABL.correlatedPairPMF ρ hρ)
      fun xy => f xy.1 * g xy.2
    The recursively nested correlated expectation is the canonical Chapter 2 correlated-pair
expectation on the sign cube.
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.correlatedPairExpectation_eq_uniformInner_noiseOperator (n : ℕ)
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) (f g : FABL.SignCube n → ℝ) :
  (FABL.pmfExpectation (FABL.correlatedPairPMF ρ hρ) fun xy =>
      f xy.1 * g xy.2) =
    FABL.uniformInner f ((FABL.noiseOperator ρ) g)
    theorem FABL.correlatedPairExpectation_eq_uniformInner_noiseOperator
  (n : ℕ) (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1)
  (f g : FABL.SignCube n → ℝ) :
  (FABL.pmfExpectation
      (FABL.correlatedPairPMF ρ hρ)
      fun xy => f xy.1 * g xy.2) =
    FABL.uniformInner f
      ((FABL.noiseOperator ρ) g)
    The canonical correlated-pair expectation is the inner product with the noise operator.
  • theoremdefined in FABL/Chapter09/ProductHypercontractivity.lean
    complete
    theorem FABL.productLpNorm_uniformSign_eq_uniformLpNorm (n : ℕ) (p : ℝ)
  (f : FABL.SignCube n → ℝ) :
  FABL.productLpNorm (FABL.uniformPMF FABL.Sign) n p f =
    FABL.uniformLpNorm p f
    theorem FABL.productLpNorm_uniformSign_eq_uniformLpNorm
  (n : ℕ) (p : ℝ)
  (f : FABL.SignCube n → ℝ) :
  FABL.productLpNorm
      (FABL.uniformPMF FABL.Sign) n p f =
    FABL.uniformLpNorm p f
    Chapter 8's uniform-sign product norm is the established Boolean-cube uniform norm.