MOO / Influence Layer For The Cn^3 Formalization

This module contains the influence statistics and the base analytic estimates that feed the weak invariance theorem based on the Mossel-O'Donnell-Oleszkiewicz invariance principle.

Here MOO abbreviates Mossel, O'Donnell, and Oleszkiewicz; see "Noise stability of functions with low influences: Invariance and optimality", Annals of Mathematics 171 (2010), 295-341.

The public objects here are the influence quantities used in the comparison theorems:

• rowInfluence
• threeHalfInfluenceSum
• mooKernel
• paperThreeHalfInfluenceSum

The reusable discrete sign-moment machinery now lives in RequestProject.HadamardCn3DiscreteMoments.

Influence Quantities

These definitions give the matrix and edge-coordinate influence statistics that feed into the weak invariance estimates and the final threeHalfInfluenceSum bounds.

def maxInfluence (n : ℕ) (lam : Fin n → Fin n → ℝ) : ℝ

The max influence I_max(λ) = max_k Σ_{i≠k} λ_{ik}².

Equations

• maxInfluence n lam = if h : 0 < n then Finset.univ.sup' ⋯ fun (k : Fin n) => ∑ i : Fin n, if i ≠ k then lam (min i k) (max i k) ^ 2 else 0 else 0

def rowInfluence (n : ℕ) (lam : Fin n → Fin n → ℝ) (k : Fin n) : ℝ

Row influence I_k(λ) = Σ_{i≠k} λ_{ik}².

Equations

• rowInfluence n lam k = ∑ i : Fin n, if i ≠ k then lam (min i k) (max i k) ^ 2 else 0

def threeHalfInfluenceSum (n : ℕ) (lam : Fin n → Fin n → ℝ) : ℝ

The ℓ^{3/2}-row statistic J(λ) = Σ_k I_k(λ)^{3/2}, written using sqrt.

Equations

• threeHalfInfluenceSum n lam = ∑ k : Fin n, rowInfluence n lam k * √(rowInfluence n lam k)

theorem rowInfluence_nonneg (n : ℕ) (lam : Fin n → Fin n → ℝ) (k : Fin n) : 0 ≤ rowInfluence n lam k

theorem exists_rowInfluence_eq_maxInfluence (n : ℕ) (hn : 0 < n) (lam : Fin n → Fin n → ℝ) : ∃ (k : Fin n), rowInfluence n lam k = maxInfluence n lam

theorem le_of_mul_sqrt_le_mul_sqrt {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hxy : x * √x ≤ y * √y) : x ≤ y

def Q2Signs (n : ℕ) (f : Fin n → Fin n → ℝ) (σ : Fin n → Fin 2) : ℝ

Ordered-sum quadratic form in Rademacher variables. This matches the normalization used in the manuscript's degree-2 invariance principle.

Equations

• Q2Signs n f σ = ∑ i : Fin n, ∑ j : Fin n, f i j * ↑(signOf (σ i)) * ↑(signOf (σ j))

def Q2Gauss (n : ℕ) (f : Fin n → Fin n → ℝ) (x : Fin n → ℝ) : ℝ

Ordered-sum quadratic form in Gaussian variables. This matches the normalization used in the manuscript's degree-2 invariance principle.

Equations

• Q2Gauss n f x = ∑ i : Fin n, ∑ j : Fin n, f i j * x i * x j

def kernelInfluence (n : ℕ) (f : Fin n → Fin n → ℝ) (k : Fin n) : ℝ

Row influence for the ordered-sum kernel formulation of the degree-2 invariance principle.

Equations

• kernelInfluence n f k = ∑ j : Fin n, f k j ^ 2

def mooKernel (n : ℕ) (lam : Fin n → Fin n → ℝ) : Fin n → Fin n → ℝ

The symmetric kernel attached to lam in the manuscript normalization.

Equations

• mooKernel n lam i j = if i = j then 0 else lam (min i j) (max i j) / 2

theorem mooKernel_symm (n : ℕ) (lam : Fin n → Fin n → ℝ) (i j : Fin n) : mooKernel n lam i j = mooKernel n lam j i

theorem mooKernel_diag (n : ℕ) (lam : Fin n → Fin n → ℝ) (i : Fin n) : mooKernel n lam i i = 0

theorem q2Gauss_mooKernel_eq_gaussianInnerX (n : ℕ) (lam : Fin n → Fin n → ℝ) (x : Fin n → ℝ) : Q2Gauss n (mooKernel n lam) x = gaussianInnerX n lam x

theorem q2Signs_mooKernel_eq_innerX (n : ℕ) (lam : Fin n → Fin n → ℝ) (σ : Fin n → Fin 2) : Q2Signs n (mooKernel n lam) σ = innerX n lam σ

theorem kernelInfluence_mooKernel (n : ℕ) (lam : Fin n → Fin n → ℝ) (k : Fin n) : kernelInfluence n (mooKernel n lam) k = 1 / 4 * ∑ i : Fin n, if i ≠ k then lam (min i k) (max i k) ^ 2 else 0

theorem maxInfluence_nonneg (n : ℕ) (lam : Fin n → Fin n → ℝ) : 0 ≤ maxInfluence n lam

def rowInfluenceEdge (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) (k : Fin n) : ℝ

Edge-coordinate row influence, transported from the matrix model.

Equations

• rowInfluenceEdge n mu k = rowInfluence n (matrixOfEdge n mu) k

def rowInfluenceMaxEdge (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : ℝ

Edge-coordinate maximal row influence.

Equations

• rowInfluenceMaxEdge n mu = maxInfluence n (matrixOfEdge n mu)

def threeHalfInfluenceSumEdge (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : ℝ

Edge-coordinate ℓ^{3/2} row statistic.

Equations

• threeHalfInfluenceSumEdge n mu = threeHalfInfluenceSum n (matrixOfEdge n mu)

theorem rowInfluenceEdge_eq (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) (k : Fin n) : rowInfluenceEdge n mu k = rowInfluence n (matrixOfEdge n mu) k

theorem rowInfluenceMaxEdge_eq (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : rowInfluenceMaxEdge n mu = maxInfluence n (matrixOfEdge n mu)

theorem threeHalfInfluenceSumEdge_eq (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : threeHalfInfluenceSumEdge n mu = threeHalfInfluenceSum n (matrixOfEdge n mu)

theorem threeHalfInfluenceSumEdge_le_card_mul_maxInfluence (n : ℕ) (hn : 0 < n) (mu : Cn3Torus.Edge n → ℝ) : threeHalfInfluenceSumEdge n mu ≤ ↑n * (rowInfluenceMaxEdge n mu * √(rowInfluenceMaxEdge n mu))

theorem gaussianPsi_norm_bound (n : ℕ) (lam : Fin n → Fin n → ℝ) : ‖gaussianPsi n lam‖ ≤ (1 + 2 * sNorm n lam) ^ (-1 / 4)

The Gaussian characteristic-function bound used after the MOO comparison: |ψ_G(λ)| ≤ (1 + 2 sNorm(λ))^{-1/4}. This is the separate Gaussian calculation from the text, distinct from the invariance-principle input.

theorem avgSigns_sub (n : ℕ) (f g : (Fin n → Fin 2) → ℝ) : (avgSigns n fun (σ : Fin n → Fin 2) => f σ - g σ) = avgSigns n f - avgSigns n g

theorem avgSigns_mono (n : ℕ) {f g : (Fin n → Fin 2) → ℝ} (hfg : ∀ (σ : Fin n → Fin 2), f σ ≤ g σ) : avgSigns n f ≤ avgSigns n g

theorem psi_re_eq_avgSigns_cos (n : ℕ) (lam : Fin n → Fin n → ℝ) : (psi n lam).re = avgSigns n fun (σ : Fin n → Fin 2) => Real.cos (innerX n lam σ)

theorem psi_im_eq_avgSigns_sin (n : ℕ) (lam : Fin n → Fin n → ℝ) : (psi n lam).im = avgSigns n fun (σ : Fin n → Fin 2) => Real.sin (innerX n lam σ)

theorem abs_cos_sub_one_add_sq_div_two_le_pow_four_div_twentyfour (x : ℝ) : |Real.cos x - (1 - x ^ 2 / 2)| ≤ |x| ^ 4 / 24

theorem re_psi_taylor4_decomposition (n : ℕ) (lam : Fin n → Fin n → ℝ) : ∃ (eps : ℝ), (psi n lam).re = 1 - momentX n lam 2 / 2 + momentX n lam 4 / 24 + eps ∧ |eps| ≤ avgSigns n fun (σ : Fin n → Fin 2) => |innerX n lam σ| ^ 6 / 720

theorem im_psi_taylor5_decomposition (n : ℕ) (lam : Fin n → Fin n → ℝ) : ∃ (eps : ℝ), (psi n lam).im = momentX n lam 1 - momentX n lam 3 / 6 + momentX n lam 5 / 120 + eps ∧ |eps| ≤ avgSigns n fun (σ : Fin n → Fin 2) => |innerX n lam σ| ^ 7 / 5040