Moment Layer For The Cn^3 Formalization

This module packages the reusable discrete and Gaussian moment estimates that sit between the torus/count bridge and the weak invariance layer.

Its declarations are meant to support later modules rather than to provide the main reader-facing theorem surface.

DL10 Local Expansion Facts

These are from the proof of DL10 Lemma 3.1 and standard Rademacher moment computations.

theorem Cn3Torus.avgOver_mul_const_left (n : ℕ) (c : ℝ) (f : (Fin n → Bool) → ℝ) : (avgOver n fun (y : Fin n → Bool) => c * f y) = c * avgOver n f

Linearity of the Boolean-edge average in a scalar factor.

theorem Cn3Torus.sqNormEdge_nonneg (n : ℕ) (mu : Edge n → ℝ) : 0 ≤ sqNormEdge n mu

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

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

theorem Cn3Torus.avgOver_sum {α : Type u_1} [Fintype α] (n : ℕ) (f : α → (Fin n → Bool) → ℝ) : (avgOver n fun (y : Fin n → Bool) => ∑ a : α, f a y) = ∑ a : α, avgOver n fun (y : Fin n → Bool) => f a y

Pull a finite outer sum through the Boolean-edge average.

theorem Cn3Torus.avgOver_weighted_prod_Z_two (n : ℕ) (mu : Edge n → ℝ) (e : Edge n) : (avgOver n fun (y : Fin n → Bool) => W mu y * Z y e) = mu e

theorem volume_measurePreserving_funUnique_real : MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.funUnique Unit ℝ)) MeasureTheory.volume MeasureTheory.volume

The singleton-coordinate collapse on Unit → ℝ preserves volume.

theorem gaussian_integral_formula (d : ℕ) (a : ℝ) (ha : 0 < a) : ∫ (x : Fin d → ℝ), Real.exp (-a * ∑ i : Fin d, x i ^ 2) = (Real.pi / a) ^ (↑d / 2)

Gaussian integral: ∫_{ℝ^d} e^{-a‖x‖²} dx = (π/a)^{d/2} for a > 0.

theorem gaussian_integral_formula_edge (n : ℕ) (a : ℝ) (ha : 0 < a) : ∫ (mu : Cn3Torus.Edge n → ℝ), Real.exp (-a * Cn3Torus.sqNormEdge n mu) = (Real.pi / a) ^ (↑(dim n) / 2)

Edge-coordinate transport of gaussian_integral_formula.

Gaussian monomial moments (reusable for Section 5 / gaussianF comparisons).

theorem gaussian_one_dim_even_moment (k : ℕ) (a : ℝ) (ha : 0 < a) : ∫ (x : ℝ), x ^ (2 * k) * Real.exp (-a * x ^ 2) = ↑(2 * k - 1).doubleFactorial / (2 ^ k * a ^ k) * √(Real.pi / a)

1D even Gaussian moments (exact): (\int_{\mathbb R} x^{2k} e^{-a x^2},dx = \frac{(2k-1)!!}{2^k a^k}\sqrt{\pi/a}) for (a>0).

noncomputable def gaussianRadialMomentK (m : ℕ) : ℝ

Normalized radial kernel (\int |y|^{2m} e^{-y^2},dy) (shorthand for scaling identities).

Equations

• gaussianRadialMomentK m = ∫ (y : ℝ), y ^ (2 * m) * Real.exp (-1 * y ^ 2)

theorem gaussian_one_dim_scaled_moment (m : ℕ) (t : ℝ) (ht : 0 < t) : ∫ (x : ℝ), x ^ (2 * m) * Real.exp (-2 * t * x ^ 2) = ↑(2 * m - 1).doubleFactorial / (2 ^ m * (2 * t) ^ m) * √(Real.pi / (2 * t))

Exact 1D moment formula specialized to the kernel exp(-2 t x^2).

noncomputable def gaussianRadialMomentCoeff (m : ℕ) : ℝ

Explicit coefficient ((2m-1)!!/4^m) in (\mathbb R^d) radial moment bounds (matches (d^m/t^m) after absorbing powers of (2) from the kernel (\exp(-2t|x|^2))).

Equations

• gaussianRadialMomentCoeff m = ↑(2 * m - 1).doubleFactorial / 4 ^ m

theorem gaussian_radial_moments (d m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 1 ≤ t → ∫ (x : Fin d → ℝ), (∑ i : Fin d, x i ^ 2) ^ m * Real.exp (-2 * t * ∑ i : Fin d, x i ^ 2) ≤ C / t ^ m * gaussianF d t

Manuscript lem:gaussian-radial-moments in a form strong enough for the local core error estimates: the radial Gaussian moments cost a factor t^{-m} relative to gaussianF.

theorem gaussian_radial_moments_edge (n m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 1 ≤ t → ∫ (mu : Cn3Torus.Edge n → ℝ), Cn3Torus.sqNormEdge n mu ^ m * Real.exp (-2 * t * Cn3Torus.sqNormEdge n mu) ≤ C / t ^ m * gaussianF (dim n) t

Edge-coordinate transport of gaussian_radial_moments.

theorem coreMass_eq_edgeCoreRegion_gaussian_integral (n : ℕ) (t : ℝ) : coreMass (dim n) t = ∫ (mu : Cn3Torus.Edge n → ℝ) in edgeCoreRegion n t, Real.exp (-2 * t * Cn3Torus.sqNormEdge n mu)

The edge-core Gaussian mass is exactly coreMass after transport from Fin (dim n) coordinates.

theorem gaussian_tail_factoring (d : ℕ) (t : ℝ) (ht : 0 < t) : ∫ (x : Fin d → ℝ), {x : Fin d → ℝ | ∑ i : Fin d, x i ^ 2 > ↑d / t}.indicator (fun (x : Fin d → ℝ) => Real.exp (-2 * t * ∑ i : Fin d, x i ^ 2)) x ≤ Real.exp (-↑d) * (Real.pi / t) ^ (↑d / 2)

Gaussian tail: On {‖x‖² > d/t}, e^{-2t‖x‖²} ≤ e^{-d}·e^{-t‖x‖²}.