Discrete Sign Moment Layer For The Cn^3 Formalization

This module packages the reusable discrete sign-average identities and low-order moment estimates that feed the residual, local-gap, and fixed-n layers.

It contains the cubic and quintic pointwise controls for the discrete statistics attached to innerX, but it does not contain the Mossel-O'Donnell-Oleszkiewicz invariance-principle material itself.

theorem sNorm_nonneg (n : ℕ) (lam : Fin n → Fin n → ℝ) : 0 ≤ sNorm n lam

theorem avgSigns_const (n : ℕ) (c : ℝ) : (avgSigns n fun (x : Fin n → Fin 2) => c) = c

Basic Discrete Averages

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

theorem avgSigns_mul_const_left (n : ℕ) (c : ℝ) (f : (Fin n → Fin 2) → ℝ) : (avgSigns n fun (σ : Fin n → Fin 2) => c * f σ) = c * avgSigns n f

theorem avgSigns_sum {n : ℕ} {α : Type u_1} [DecidableEq α] (s : Finset α) (f : α → (Fin n → Fin 2) → ℝ) : (avgSigns n fun (σ : Fin n → Fin 2) => ∑ a ∈ s, f a σ) = ∑ a ∈ s, avgSigns n (f a)

theorem avgSigns_linearX_sq (n : ℕ) (x : Fin n → ℝ) : (avgSigns n fun (σ : Fin n → Fin 2) => linearX n x σ ^ 2) = ∑ i : Fin n, x i ^ 2

theorem avgSigns_linearX_four (n : ℕ) (x : Fin n → ℝ) : (avgSigns n fun (σ : Fin n → Fin 2) => linearX n x σ ^ 4) = 3 * (∑ i : Fin n, x i ^ 2) ^ 2 - 2 * ∑ i : Fin n, x i ^ 4

theorem linearX_sq_eq_diag_add_offdiag (n : ℕ) (x : Fin n → ℝ) (σ : Fin n → Fin 2) : linearX n x σ ^ 2 = ∑ i : Fin n, x i ^ 2 + 2 * ∑ i : Fin n, ∑ j : Fin n, if i < j then x i * x j * ↑(signOf (σ i)) * ↑(signOf (σ j)) else 0

theorem abs_avgSigns_le_avgSigns_abs (n : ℕ) (f : (Fin n → Fin 2) → ℝ) : |avgSigns n f| ≤ avgSigns n fun (σ : Fin n → Fin 2) => |f σ|

theorem momentX_four_peel_last (n : ℕ) (lam : Fin (n + 1) → Fin (n + 1) → ℝ) : momentX (n + 1) lam 4 = (momentX n (minorLamLast lam) 4 + 6 * avgSigns n fun (σ : Fin n → Fin 2) => innerX n (minorLamLast lam) σ ^ 2 * linearX n (lastColLam lam) σ ^ 2) + (3 * (∑ i : Fin n, lastColLam lam i ^ 2) ^ 2 - 2 * ∑ i : Fin n, lastColLam lam i ^ 4)

theorem fixedDegreeHC_degree2_W_fourth (n : ℕ) (mu : Cn3Torus.Edge n → ℝ) : (Cn3Torus.avgOver n fun (y : Fin n → Bool) => |Cn3Torus.W mu y| ^ 4) ≤ 3 ^ 4 * Cn3Torus.sqNormEdge n mu ^ 2

Internal proof of the degree-2 L^4 hypercontractive bound used downstream.

theorem Cn3Torus.avgOver_abs_five_le_1125_mul_sqNormEdge_fiveHalves (n : ℕ) (mu : Edge n → ℝ) : (avgOver n fun (y : Fin n → Bool) => |W mu y| ^ 5) ≤ 1125 * sqNormEdge n mu ^ (5 / 2)

theorem momentX_five_abs_le (n : ℕ) (lam : Fin n → Fin n → ℝ) : |momentX n lam 5| ≤ 1125 * sNorm n lam ^ (5 / 2)

Discrete Sign Moment Identities

These lemmas compute the low-order discrete sign moments used later in the cubic statistic cubicT and the quintic correction term quinticP5.

theorem momentX_one_eq_zero (n : ℕ) (lam : Fin n → Fin n → ℝ) : momentX n lam 1 = 0

theorem momentX_two_eq_sNorm (n : ℕ) (lam : Fin n → Fin n → ℝ) : momentX n lam 2 = sNorm n lam

theorem momentX_three_eq_six_cubicT (n : ℕ) (lam : Fin n → Fin n → ℝ) : momentX n lam 3 = 6 * cubicT n lam

theorem avgSigns_abs_innerX_six_eq_momentX_six (n : ℕ) (lam : Fin n → Fin n → ℝ) : (avgSigns n fun (σ : Fin n → Fin 2) => |innerX n lam σ| ^ 6) = momentX n lam 6

The sixth sign moment coincides with the sixth discrete moment momentX n lam 6.

theorem avgSigns_mul_const_right (n : ℕ) (f : (Fin n → Fin 2) → ℝ) (c : ℝ) : (avgSigns n fun (σ : Fin n → Fin 2) => f σ * c) = avgSigns n f * c

theorem avgSigns_div_const (n : ℕ) (f : (Fin n → Fin 2) → ℝ) (c : ℝ) : (avgSigns n fun (σ : Fin n → Fin 2) => f σ / c) = avgSigns n f / c

theorem fourth_cumulant_identity_of_mixed_peel (hmixed : ∀ (n : ℕ) (lam : Fin (n + 1) → Fin (n + 1) → ℝ), (avgSigns n fun (σ : Fin n → Fin 2) => innerX n (minorLamLast lam) σ ^ 2 * linearX n (lastColLam lam) σ ^ 2) = sNorm n (minorLamLast lam) * ∑ i : Fin n, lastColLam lam i ^ 2 + 4 * simpleCycle4LastCross n (minorLamLast lam) (lastColLam lam)) (n : ℕ) (lam : Fin n → Fin n → ℝ) : (momentX n lam 4 - 3 * sNorm n lam ^ 2) / 24 = quarticCorr n lam

theorem quinticP5_pointwise_bound (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (lam : Fin n → Fin n → ℝ), |quinticP5 n lam| ≤ C * sNorm n lam ^ (5 / 2)

Crude pointwise quintic control used later in the fixed-n and local-gap estimates.