CombineFiniteMean

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

Corrected finite-corridor mean estimate

This module bounds comparator-centered starred coarse quadratics under the same-cutoff relative-normalized law. It combines the relative-origin error comparison with real-stationary descendant averaging.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.starredComparatorQuadraticRaw {d : ℕ} (B : HCPolySupport.FullBlockMat d) (C : HCPolySupport.BlockMat d) (q : HCPolySupport.FullBlockVec d) (U : Set (HCPolySupport.Vec d)) (a : HCPolySupport.CoeffField d) : ℝ

The square-root-conjugated quadratic difference from a coarse comparator matrix.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.starredComparatorQuadratic {d : ℕ} (B : HCPolySupport.FullBlockMat d) (C : HCPolySupport.BlockMat d) (q : HCPolySupport.FullBlockVec d) (U : Set (HCPolySupport.Vec d)) (a : HCPolySupport.RegCoeffField d) : ℝ

The coarse comparator quadratic evaluated on a regular coefficient field.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.starredComparatorQuadratic B C q U a = Algsuperdiff.Section3.Provider.Homogenization.starredComparatorQuadraticRaw B C q U a.toFun

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.twoTermSecondFourthBudget (A D : ℝ) : ℝ

The combined second- and fourth-moment budget for two stretched-exponential tails.

Equations

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

theorem Algsuperdiff.Section3.Provider.Homogenization.relativeStarredComparator_origin_and_descendant_moment_bounds {d : ℕ} [NeZero d] (M : ABKModel d) (L n : ℤ) (hLn : L ≤ n) {s A D : ℝ} (hs : 0 < s) (hLower : Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationError M L ⟨s, hs⟩) A D) (q : HCPolySupport.FullBlockVec d) : have c := ↑(Cutoff.cutoffRelativeNormalizationShift d); have P := Cutoff.relativeNormalizedCutoffLaw M L; have sigma := Annealed.sigmaBar M L; have a0 := Observable.isotropicComparatorMatrix sigma; have B := HCPolySupport.Book.Ch02.constantFullBlockMatrix a0; have C0 := HCPolySupport.Book.Ch02.constantBlockMatrix a0; have X := fun (U : Set (HCPolySupport.Vec d)) (a : HCPolySupport.RegCoeffField d) => HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic (starredFluctuationMatrix B C0 U a) q; have parent := n - L - c; have N := ↑(HCPolySupport.descendantsAtScale (HCPolySupport.originCube d parent) (-c)).card; have budget := 2 * ((HCPolySupport.IndependentSums.gammaMomentConst 2 * 2 ^ 2⁻¹ * A) ^ 2 + (HCPolySupport.IndependentSums.gammaMomentConst (1 / 2) * 2 ^ (1 / 2)⁻¹ * D) ^ 2) + 8 * ((HCPolySupport.IndependentSums.gammaMomentConst 2 * 4 ^ 2⁻¹ * A) ^ 4 + (HCPolySupport.IndependentSums.gammaMomentConst (1 / 2) * 4 ^ (1 / 2)⁻¹ * D) ^ 4); have probeBudget := 6 * (q ⬝ᵥ q) ^ 2 * budget; have K := √probeBudget; MeasureTheory.Integrable (fun (a : HCPolySupport.RegCoeffField d) => X (HCPolySupport.cubeSet (HCPolySupport.originCube d (-c))) a ^ 2) P ∧ ∫ (a : HCPolySupport.RegCoeffField d), X (HCPolySupport.cubeSet (HCPolySupport.originCube d (-c))) a ^ 2 ∂P ≤ probeBudget ∧ MeasureTheory.Integrable (fun (a : HCPolySupport.RegCoeffField d) => |HCPolySupport.Book.Ch04.restrictionCenteredDescendantAverage P (-c) parent X a| ^ 2) P ∧ (∫ (a : HCPolySupport.RegCoeffField d), |HCPolySupport.Book.Ch04.restrictionCenteredDescendantAverage P (-c) parent X a| ^ 2 ∂P) ^ (1 / 2) ≤ N⁻¹ * (HCPolySupport.Book.Ch04.rosenthalDescendantsAtScaleLpConst d (-c) 2 * N ^ (1 / 2) * K + HCPolySupport.Book.Ch04.rosenthalDescendantsAtScaleSqrtConst d (-c) 2 * √N * K)

Raw relative-origin and centered descendant second-moment bounds used by the quantitative finite-corridor consumer.