CombineFiniteTrace #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Quantitative trace channel #
The starred trace average is transported from the same-cutoff relative law to physical cutoff samples. Jensen reduces its square to the fourth moment of the physical child error, and translation stationarity identifies every child moment with the cutoff-scale origin moment.
theorem
Algsuperdiff.Section3.Provider.Homogenization.eight_mul_integral_relativeStarredBlockJTraceAverageSq_le
{d : ℕ}
[NeZero d]
(M : ABKModel d)
(L n : ℤ)
(hLn : L ≤ n)
{A D : ℝ}
(hLower :
Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2)
(HCPolySupport.IndependentSums.gammaSigma (1 / 2))
(Observable.cutoffHomogenizationError M L
⟨1 / 16, eight_mul_integral_relativeStarredBlockJTraceAverageSq_le._proof_1⟩)
A D)
:
have c := ↑(Cutoff.cutoffRelativeNormalizationShift d);
have h := L + c;
have P := Cutoff.relativeNormalizedCutoffLaw M L;
have a0 := Observable.isotropicComparatorMatrix (Annealed.sigmaBar M L);
have B := HCPolySupport.Book.Ch02.constantFullBlockMatrix a0;
have Q := HCPolySupport.originCube d (n - h);
have j := (n - L).toNat;
have fourthBudget :=
8 * ((HCPolySupport.IndependentSums.gammaMomentConst 2 * 4 ^ 2⁻¹ * A) ^ 4 + (HCPolySupport.IndependentSums.gammaMomentConst (1 / 2) * 4 ^ (1 / 2)⁻¹ * D) ^ 4);
MeasureTheory.Integrable (starredBlockJTraceAverageSq B Q j) P ∧ 8 * ∫ (a : HCPolySupport.RegCoeffField d), starredBlockJTraceAverageSq B Q j a ∂P ≤ 8 * (↑(Fintype.card (HCPolySupport.BlockCoord d)) ^ 2 * fourthBudget)
Quantitative fourth-moment control of the starred trace channel at every physical observation scale above the cutoff.