Coarse-graining support: #
Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.CutoffOscillationUniform
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Uniform cutoff-oscillation absorption #
This file removes the non-uniform ratio argument from the cutoff-oscillation term in the third Section 5.3 lemma.
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.cutoffOscillation_special_expectedResponse_le_lowScaleTail_uniform
{d : ℕ}
[NeZero d]
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P) {k m : ℕ},
k < m →
∀ (e : Vec d),
vecNormSq e = 1 →
∀ {ε : ℝ},
0 < ε →
ε ≤ 1 →
have β := section53CoarseFluctuationBeta hP4;
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;
JUpperBoundWeakNorms.section53CutoffOscillationConstant Q * JUpperBoundWeakNorms.section53CutoffScaleSep Q j * Ch04.expectedResponseJCubeSet P Q p_e q_e ≤ C * ε⁻¹ * (β ^ 2)⁻¹ * Real.rpow 3 (-2 * β * ↑(m - k)) * coarseFluctuationScalarWeightAtScale hP hStruct m * (thetaAtScale hP hStruct ↑m - 1)
Uniform cutoff-oscillation absorption. The constant is chosen before the
law, scales, vector, and ε.