Coarse-graining support: Support.Book.Ch05.Theorems.Section55.ShiftedWidetildeTheta.TwoStep

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

theorem HCPolySupport.Book.Ch05.Section55.upperTwoBetaFactorPowerIntegrableAtScale_from_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.LambdaSqCoeffField (originCube d ↑m) (hP4.sUpper + 2 * Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4) (Ch02.MultiscaleExponent.finite 1) a ^ hP4.xi) P

theorem HCPolySupport.Book.Ch05.Section55.lowerTwoBetaFactorPowerIntegrableAtScale_from_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => (Ch04.lambdaSqCoeffField (originCube d ↑m) (hP4.sLower + 2 * Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4) (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ hP4.xi) P

theorem HCPolySupport.Book.Ch05.Section55.thetaAtScale_le_twoBetaShiftedWidetildeThetaAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (n : ℕ) : thetaAtScale hP hStruct ↑n ≤ shiftedWidetildeThetaAtScale P (↑n) hP4 (2 * Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4)

theorem HCPolySupport.Book.Ch05.Section55.twoBetaShiftedWidetildeThetaAtScale_zero_bound_homogenizationScale {d : ℕ} [NeZero d] (xi : ℕ) (β : ℝ) (hβ : 0 < β) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.xi = xi → Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 = β → ∀ (m : ℕ), shiftedWidetildeThetaAtScale P (↑m) hP4 (2 * β) ≤ thetaAtScale hP hStruct 0 + C * Real.rpow 3 (-β * ↑m) * shiftedWidetildeThetaAtScale P 0 hP4 β

One-window shifted localization with the source exponents already shifted by one β, hence with target exponents shifted by 2β.

theorem HCPolySupport.Book.Ch05.Section55.shiftedWidetildeThetaAtScale_restrictionScaleNormalizedLaw {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {η : ℝ} (hUpper : 0 < hP4.sUpper + η) (hLower : 0 < hP4.sLower + η) (k m : ℕ) : shiftedWidetildeThetaAtScale (Ch04.restrictionScaleNormalizedLaw k P) (↑m) (hP4.scaleNormalized hP hStruct k) η = shiftedWidetildeThetaAtScale P (↑(k + m)) hP4 η

theorem HCPolySupport.Book.Ch05.Section55.twoBetaShiftedWidetildeThetaAtScale_shifted_bound_homogenizationScale {d : ℕ} [NeZero d] (xi : ℕ) (β : ℝ) (hβ : 0 < β) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.xi = xi → Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 = β → ∀ {k n : ℕ}, k ≤ n → shiftedWidetildeThetaAtScale P (↑n) hP4 (2 * β) ≤ thetaAtScale hP hStruct ↑k + C * Real.rpow 3 (-β * ↑(n - k)) * shiftedWidetildeThetaAtScale P (↑k) hP4 β