CombineFiniteQuantitative #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Relative descendant fluctuation decomposition #
This module decomposes a relative-normalized descendant probe into its centered random part and its deterministic annealed-scale defect. It also transfers annealed block monotonicity across every integer relative scale.
theorem
Algsuperdiff.Section3.Provider.Homogenization.relativeStarredDescendantProbe_sq_integrable_and_le
{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 hP := ⋯;
have hStruct := ⋯;
have center := n - L - c;
have Q := HCPolySupport.originCube d center;
have j := (n - L).toNat;
have sigma := Annealed.sigmaBar M L;
have a0 := Observable.isotropicComparatorMatrix sigma;
have B := HCPolySupport.Book.Ch02.constantFullBlockMatrix a0;
have Cn := HCPolySupport.Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct center;
have Y := fun (a : HCPolySupport.RegCoeffField d) =>
HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic
(starredDescendantsAverageFluctuationMatrix B Cn Q j a) q;
have N := ↑(HCPolySupport.descendantsAtScale Q (-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 secondBudget :=
2 * ((HCPolySupport.IndependentSums.gammaMomentConst 2 * 2 ^ 2⁻¹ * A) ^ 2 + (HCPolySupport.IndependentSums.gammaMomentConst (1 / 2) * 2 ^ (1 / 2)⁻¹ * D) ^ 2);
have meanBudget := 4 * (q ⬝ᵥ q) ^ 2 * secondBudget ^ 2;
have K := √probeBudget;
have rootBound :=
N⁻¹ * (HCPolySupport.Book.Ch04.rosenthalDescendantsAtScaleLpConst d (-c) 2 * N ^ (1 / 2) * K + HCPolySupport.Book.Ch04.rosenthalDescendantsAtScaleSqrtConst d (-c) 2 * √N * K);
MeasureTheory.Integrable (fun (a : HCPolySupport.RegCoeffField d) => Y a ^ 2) P ∧ ∫ (a : HCPolySupport.RegCoeffField d), Y a ^ 2 ∂P ≤ 2 * rootBound ^ 2 + 2 * meanBudget
Second-moment control of an arbitrary quadratic probe of the actual relative descendant-average fluctuation matrix.