Coarse-graining support: #
Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.PairedSquares
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Paired weak-norm square conversion #
This proof-internal file assembles the square estimates coming from the weak-norm maximizer theorem for the third Section 5.3 lemma.
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.paired_mismatchTermSquares_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 defectSum :=
∑ n ∈ Finset.Icc (↑k + 1) ↑m,
Real.rpow 3 (-β * ↑(↑m - n).toNat) * √(WeakNormsMaximizer.responseDefectAverageAtScale (↑m) n p_e q_e a);
have lowerExcess :=
max ((Ch04.lambdaSqCoeffField Q s' (Ch02.MultiscaleExponent.finite 1) a)⁻¹ - (hP.barSigmaStarAtScale hStruct 0)⁻¹) 0;
have upperExcess :=
max (Ch04.LambdaSqCoeffField Q t' (Ch02.MultiscaleExponent.finite 1) a - hP.barSigmaAtScale hStruct 0) 0;
σ * WeakNormsMaximizer.gradientMismatchTermAtScale (↑m) (↑k) s s' p_e q_e a ^ 2 + σ⁻¹ * WeakNormsMaximizer.fluxMismatchTermAtScale (↑m) (↑k) t t' p_e q_e a ^ 2 ≤ (coarseFluctuationScalarWeightAtScale hP hStruct m + (σ * lowerExcess + σ⁻¹ * upperExcess)) * defectSum ^ 2
Pointwise decomposition of the response-defect mismatch-square pair in the weak-norm maximizer RHS. The endpoint ellipticity factors are split into their scale-zero baseline plus the shifted positive excess.
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integral_paired_mismatchTermSquares_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),
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;
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
σ * WeakNormsMaximizer.gradientMismatchTermAtScale (↑m) (↑k) s s' p_e q_e a ^ 2 + σ⁻¹ * WeakNormsMaximizer.fluxMismatchTermAtScale (↑m) (↑k) t t' p_e q_e a ^ 2)
P ∧ ∫ (a : RegCoeffField d), σ * WeakNormsMaximizer.gradientMismatchTermAtScale (↑m) (↑k) s s' p_e q_e a ^ 2 + σ⁻¹ * WeakNormsMaximizer.fluxMismatchTermAtScale (↑m) (↑k) t t' p_e q_e a ^ 2 ∂P ≤ C * ((β ^ 2)⁻¹ * coarseFluctuationScalarWeightAtScale hP hStruct m * coarseFluctuationTauSumAtScale hP hStruct hP4 k m e + ↑hP4.xi * (β ^ 3)⁻¹ * Real.rpow 3 (-β * ↑m) * coarseFluctuationUnitMomentWeightAtScale hP hStruct hP4 m * coarseFluctuationResponseMomentAtScale hP hStruct hP4 k m e)
Expectation-level conversion for the paired response-defect mismatch squares in the weak-norm maximizer RHS.