Coarse-graining support: #
Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.LowScaleExpectation
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Low-scale expectation estimates #
This proof-internal file owns the expectation-level conversion of the
low-scale tails in the third Section 5.3 lemma. The pointwise low-scale split
stays in LowScaleTails.lean.
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integral_paired_lowScaleTailSquares_special_le_rawLowScaleTerms
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hstat : Ch04.RestrictionStationaryLaw P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
{k m : ℕ}
(hkm : k < m)
(e : Vec 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 j := (↑m - ↑k).toNat;
have p_e := specialPAtScale hP hStruct (↑m) e;
have q_e := specialQAtScale hP hStruct (↑m) e;
have σ := sigmaHatAtScale hP hStruct ↑m;
have childAvg := fun (a : RegCoeffField d) =>
descendantsAverage Q j fun (R : TriadicCube d) => Ch04.restrictionResponseJObservableCubeSet R p_e q_e a;
have lowerExcess := fun (a : RegCoeffField d) =>
max ((Ch04.lambdaSqCoeffField Q s' (Ch02.MultiscaleExponent.finite 1) a)⁻¹ - (hP.barSigmaStarAtScale hStruct 0)⁻¹) 0;
have upperExcess := fun (a : RegCoeffField d) =>
max (Ch04.LambdaSqCoeffField Q t' (Ch02.MultiscaleExponent.finite 1) a - hP.barSigmaAtScale hStruct 0) 0;
have tailFactor := (β ^ 2)⁻¹ * Real.rpow 3 (-2 * β * ↑(m - k));
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
σ * WeakNormsMaximizer.gradientLowScaleTailAtScale (↑m) (↑k) s s' p_e q_e a ^ 2 + σ⁻¹ * WeakNormsMaximizer.fluxLowScaleTailAtScale (↑m) (↑k) t t' p_e q_e a ^ 2)
P ∧ ∫ (a : RegCoeffField d), σ * WeakNormsMaximizer.gradientLowScaleTailAtScale (↑m) (↑k) s s' p_e q_e a ^ 2 + σ⁻¹ * WeakNormsMaximizer.fluxLowScaleTailAtScale (↑m) (↑k) t t' p_e q_e a ^ 2 ∂P ≤ tailFactor * (coarseFluctuationScalarWeightAtScale hP hStruct m * Ch04.expectedResponseJCubeSet P Q p_e q_e + (σ * ∫ (a : RegCoeffField d), lowerExcess a * childAvg a ∂P + σ⁻¹ * ∫ (a : RegCoeffField d), upperExcess a * childAvg a ∂P))
Raw expectation-level low-scale reduction: the paired low-scale tails are bounded by the parent-response baseline plus the shifted positive-excess terms with the child-response average.
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integral_paired_lowScaleTailSquares_special_le_coarseFluctuationTerms_uniform
{d : ℕ}
[NeZero d]
(params : QuantitativeCoarseGrainedEllipticityParams d)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P),
Ch04.RestrictionStationaryLaw P →
∀ (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P),
hP4.params = params →
∀ {k m : ℕ},
k < m →
∀ (e : Vec d),
vecNormSq e = 1 →
have β := section53CoarseFluctuationBeta hP4;
have s := hP4.sLower + 2 * β;
have s' := hP4.sLower + β;
have t := hP4.sUpper + 2 * β;
have t' := hP4.sUpper + β;
have p_e := specialPAtScale hP hStruct (↑m) e;
have q_e := specialQAtScale hP hStruct (↑m) e;
have σ := sigmaHatAtScale hP hStruct ↑m;
have θ := thetaAtScale hP hStruct ↑m;
∫ (a : RegCoeffField d), σ * WeakNormsMaximizer.gradientLowScaleTailAtScale (↑m) (↑k) s s' p_e q_e a ^ 2 + σ⁻¹ * WeakNormsMaximizer.fluxLowScaleTailAtScale (↑m) (↑k) t t' p_e q_e a ^ 2 ∂P ≤ C * ((β ^ 2)⁻¹ * Real.rpow 3 (-2 * β * ↑(m - k)) * coarseFluctuationScalarWeightAtScale hP hStruct m * (θ - 1) + ↑hP4.xi * (β ^ 3)⁻¹ * Real.rpow 3 (-β * ↑m) * coarseFluctuationUnitMomentWeightAtScale hP hStruct hP4 m * coarseFluctuationResponseMomentAtScale hP hStruct hP4 k m e)
Final low-scale expectation conversion in manuscript form.