Coarse-graining support: #
Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.LowScaleTails
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Low-scale tails for the coarse-fluctuation lemma #
This proof-internal file owns the low-scale tail route in the final coarse-fluctuation assembly. The important point is that the weak-norm maximizer is instantiated with two buffers, so the ellipticity coefficients in the low-scale tails are shifted by one buffer.
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.paired_lowScaleTailSquares_special_le_baseline_add_positiveExcess
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
{k m : ℕ}
(e : Vec d)
(a : RegCoeffField d)
:
have β := section53CoarseFluctuationBeta hP4;
have s := hP4.sLower + 2 * β;
have s' := hP4.sLower + β;
have t := hP4.sUpper + 2 * β;
have t' := hP4.sUpper + β;
have Q := originCube d ↑m;
have p_e := specialPAtScale hP hStruct (↑m) e;
have q_e := specialQAtScale hP hStruct (↑m) e;
have σ := sigmaHatAtScale hP hStruct ↑m;
have Jm := Ch04.restrictionResponseJObservableCubeSet Q p_e q_e a;
have lowerCoeff := (Ch04.lambdaSqCoeffField Q s' (Ch02.MultiscaleExponent.finite 1) a)⁻¹;
have upperCoeff := Ch04.LambdaSqCoeffField Q t' (Ch02.MultiscaleExponent.finite 1) a;
have lowerBase := (hP.barSigmaStarAtScale hStruct 0)⁻¹;
have upperBase := hP.barSigmaAtScale hStruct 0;
have lowerExcess := max (lowerCoeff - lowerBase) 0;
have upperExcess := max (upperCoeff - upperBase) 0;
have tailFactor := (β ^ 2)⁻¹ * Real.rpow 3 (-2 * β * ↑(m - k));
σ * WeakNormsMaximizer.gradientLowScaleTailAtScale (↑m) (↑k) s s' p_e q_e a ^ 2 + σ⁻¹ * WeakNormsMaximizer.fluxLowScaleTailAtScale (↑m) (↑k) t t' p_e q_e a ^ 2 ≤ tailFactor * (coarseFluctuationScalarWeightAtScale hP hStruct m * Jm + (σ * lowerExcess + σ⁻¹ * upperExcess) * Jm)
Pointwise algebraic reduction of the paired low-scale tails. The
ellipticity coefficients are the shifted coefficients
sLower + beta and sUpper + beta, as required for the Section 5.2 moment
input.