Coarse-graining support: Support.Book.Ch05.Theorems.Section56.SmallContrastJBound.Estimate

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.Book.Ch05.Section56.expectedResponseJCubeSet_special_le_two_smallContrastReducedRHSAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (hsmall : widetildeThetaAtScale P 0 hP4 ≤ 2) (C0 η : ℝ) (hC0_nonneg : 0 ≤ C0) (hC0_eta_le_quarter : 2 * C0 * η ≤ 1 / 4) {k m : ℕ} (hkm : k < m) (e : Vec d) (he : vecNormSq e = 1) (hyoung : expectedCenteredResponseJAtScale hP hStruct (↑m) (specialPAtScale hP hStruct (↑m) e) (specialQAtScale hP hStruct (↑m) e) ≤ Section53.JUpperBoundCoarseFluctuations.coarseFluctuationYoungManuscriptRHSAtScale hP hStruct hP4 C0 1 η k m e) (hlow_coeff : 32 * C0 * (Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 ^ 2)⁻¹ * Real.rpow 3 (-2 * Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 * ↑(m - k)) ≤ 1 / 4) : have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; Ch04.expectedResponseJCubeSet P (originCube d ↑m) p_e q_e ≤ 2 * smallContrastReducedRHSAtScale hP hStruct hP4 C0 η k m e

theorem HCPolySupport.Book.Ch05.Section56.two_smallContrastReducedRHSAtScale_le_smallContrastFinalRHSAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (C0 η C : ℝ) {k m : ℕ} (hkm : k ≤ m) (e : Vec d) (hKfluct : 8 * C0 * (Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4)⁻¹ ≤ C) (hKtau : 4 * C0 * (η + η⁻¹) + 80 * C0 * (Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 ^ 3)⁻¹ ≤ C) (hKtail : 64 * C0 * ↑hP4.xi * (Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 ^ 3)⁻¹ ≤ C) (hKtheta : 4 * C0 ≤ C) : 2 * smallContrastReducedRHSAtScale hP hStruct hP4 C0 η k m e ≤ smallContrastFinalRHSAtScale hP hStruct hP4 C k m e

theorem HCPolySupport.Book.Ch05.Section56.smallContrastJBound_homogenizationScale {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 → widetildeThetaAtScale P 0 hP4 ≤ 2 → ∀ (e : Vec d), vecNormSq e = 1 → ∀ {k m : ℕ}, C ≤ ↑(m - k) → have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; Ch04.expectedResponseJCubeSet P (originCube d ↑m) p_e q_e ≤ smallContrastFinalRHSAtScale hP hStruct hP4 C k m e