CombineFiniteVariance

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Quantitative finite-corridor two-plus-eight estimate

This module combines the descendant and trace estimates at the same-cutoff relative-normalized law. The observation cube at physical scale n is represented by the relative cube at scale n - L - c.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.finiteCorridorSecondConst : ℝ

The second-moment constant for the normalized finite-corridor tail bounds.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.finiteCorridorFourthConst : ℝ

The fourth-moment constant for the normalized finite-corridor tail bounds.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.finiteCorridorBudgetConst : ℝ

The combined second- and fourth-moment constant for the finite-corridor estimate.

Equations

• One or more equations did not get rendered due to their size.

The three constant-nonnegativity facts are proved once here. Each positivity call below sees only the smallest defining expression; the consumers reuse the resulting lemma instead of re-running positivity on an unfolded copy.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.finiteCorridorRosenthalConst (d : ℕ) : ℝ

The squared Rosenthal constant at the finite-corridor normalization shift.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.finiteCorridorProbeConst (d : ℕ) : ℝ

The common finite-probe moment budget in the finite-corridor estimate.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.finiteCorridorVarianceConst (d : ℕ) : ℝ

The dimension-dependent variance constant obtained from the finite-probe budgets.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Homogenization.exists_relativeCutoff_finiteCorridor_fluctuationVariance_bound (d : ℕ) : ∃ (Chom : ℝ) (Cvar : ℝ), 64 ≤ Chom ∧ 2 * (↑(Cutoff.cutoffRelativeNormalizationShift d) + 1) ≤ Chom ∧ 1 ≤ Cvar ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), (∀ k ≤ m - 1, ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1), Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationError M k ⟨s, ⋯⟩) (↑E * s⁻¹ * √M.gamma) (s⁻¹ ^ 2 * Real.exp (-((↑E)⁻¹ ^ 3 * M.gamma⁻¹)))) → ∀ epsilon ∈ Set.Ioc 0 (1 / 2), M.gamma ≤ Chom⁻¹ * (↑E)⁻¹ ^ 2 * epsilon → ∀ (L : ℤ), ↑L ≤ ↑m - Chom * |Real.log epsilon| → ∀ n ∈ Set.Icc L m, have hd := ⋯; have c := ↑(Cutoff.cutoffRelativeNormalizationShift d); have P := Cutoff.relativeNormalizedCutoffLaw M L; have hP := ⋯; have hStruct := ⋯; have center := n - L - c; have Q := HCPolySupport.originCube d (n - (L + c)); have B := HCPolySupport.Book.Ch02.constantFullBlockMatrix (Observable.isotropicComparatorMatrix (Annealed.sigmaBar M L)); have Cn := HCPolySupport.Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct center; have delta := ↑E ^ 2 * M.gamma + Real.exp (-(2 * (↑E)⁻¹ ^ 3 * M.gamma⁻¹)); have decay := Real.rpow 3 (-↑d * ↑(n - L).toNat); 2 * ∫ (a : HCPolySupport.RegCoeffField d), starredDescendantsAverageFluctuationOperatorNormSq B Cn Q (n - L).toNat a ∂P + 8 * ∫ (a : HCPolySupport.RegCoeffField d), starredBlockJTraceAverageSq B Q (n - L).toNat a ∂P ≤ Cvar * delta * (delta + decay)

Uniform quantitative literal two-plus-eight control along the physical integer corridor above the cutoff. The fixed relative buffer, the lower-clause specialization, and both channel bounds are discharged internally.