Coarse-graining support: Support.Book.Ch05.Theorems.Section54.OneStepContraction.RHSCompression #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Compressing the Section 5.3 RHS at a good scale #
This file turns the public Section 5.3 coarse-fluctuation RHS, specialized to
k = 0 and to the Section 5.4 special vectors, into the one-step scale
quantity (\epsilon + \epsilon^{-1}\sqrt\delta) \Theta_0.
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.thetaAtScale_zero_le_widetildeThetaAtScale_zero_of_P4
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
:
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.coarseFluctuationMomentWeight_le_twoThetaZero
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(m : ℕ)
:
Section53.JUpperBoundCoarseFluctuations.coarseFluctuationUnitMomentWeightAtScale hP hStruct hP4 m ≤ 2 * widetildeThetaAtScale P 0 hP4
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepScaleSeparation_m_pos
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP4 : QuantitativeCoarseGrainedEllipticity P)
{C delta : ℝ}
{m : ℕ}
(hC : oneStepScaleSeparationConst hP4 ≤ C)
(hdelta_pos : 0 < delta)
(hsep : C * ↑hP4.xi * Real.log (2 + delta⁻¹ * ↑hP4.xi * widetildeThetaAtScale P 0 hP4) ≤ ↑m)
:
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.coarseFluctuationManuscriptRHSAtScale_zero_le_compressed
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
{C0 Csep delta epsilon : ℝ}
{m : ℕ}
(hC0_nonneg : 0 ≤ C0)
(hCsep : oneStepScaleSeparationConst hP4 ≤ Csep)
(hdelta_pos : 0 < delta)
(hdelta_le : delta ≤ 1 / 2)
(hsep : Csep * ↑hP4.xi * Real.log (2 + delta⁻¹ * ↑hP4.xi * widetildeThetaAtScale P 0 hP4) ≤ ↑m)
(hepsilon_pos : 0 < epsilon)
(hepsilon_le : epsilon ≤ 1)
(hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m)
(hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹)
(e : Vec d)
(he : Ch02.vecNorm e = 1)
:
have β := Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4;
have M :=
3 + β⁻¹ * oneStepCoarseFullBlockConst hP4 + (β ^ 2)⁻¹ * oneStepCoarseTauSumConst hP4 + ↑hP4.xi * (β ^ 3)⁻¹ * 4 + (β ^ 2)⁻¹ * 3;
Section53.JUpperBoundCoarseFluctuations.coarseFluctuationManuscriptRHSAtScale hP hStruct hP4 C0 epsilon 0 m e ≤ C0 * M * ((epsilon + epsilon⁻¹ * √delta) * thetaAtScale hP hStruct 0)