Coarse-graining support: #
Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.HighScaleAverages
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
High-scale average terms for the coarse-fluctuation lemma #
This file contains the proof-internal deterministic conversion of the paired
high-scale average terms from WeakNormsMaximizer at the Section 5.3 special
vectors into the weighted descendant average of the normalized full-block
operator-norm-square fluctuation.
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.paired_highScaleAverageTerms_special_le_weighted_fullBlockNormalized_fluctuation
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(a : RegCoeffField d)
(ha : Ch04.AELocallyUniformlyEllipticField a)
{k m : ℕ}
(β s t : ℝ)
(hβs : β ≤ s)
(hβt : β ≤ t)
(e : Vec d)
(hb : 0 < hP.barSigmaAtScale hStruct ↑m)
(hc : 0 < hP.barSigmaStarAtScale hStruct ↑m)
(he : vecNormSq e = 1)
:
have p_e := specialPAtScale hP hStruct (↑m) e;
have q_e := specialQAtScale hP hStruct (↑m) e;
have p0_e := (hP.barSigmaStarAtScale hStruct ↑m)⁻¹ • q_e - p_e;
have q0_e := q_e - hP.barSigmaAtScale hStruct ↑m • p_e;
have σ := sigmaHatAtScale hP hStruct ↑m;
have θ := thetaAtScale hP hStruct ↑m;
have S := Finset.Icc (↑k + 1) ↑m;
have wβ := fun (n : ℤ) => Real.rpow 3 (-β * ↑(↑m - n).toNat);
σ * WeakNormsMaximizer.gradientAverageTermAtScale (↑m) (↑k) s p_e q_e p0_e a ^ 2 + σ⁻¹ * WeakNormsMaximizer.fluxAverageTermAtScale (↑m) (↑k) t p_e q_e q0_e a ^ 2 ≤ (∑ n ∈ S, wβ n) * ∑ n ∈ S,
wβ n * descendantsAverage (originCube d ↑m) (↑m - n).toNat fun (R : TriadicCube d) =>
2 * θ * fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) R a
Deterministic finite-sum/Cauchy conversion for the paired high-scale average terms at the Section 5.3 special vectors. The right side is the weighted descendant average of the normalized full-block operator-norm-square fluctuation.