Coarse-graining support:

Support.Book.Ch05.Theorems.Section55.ShiftedWidetildeTheta.ScalarPreliminaries

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

theorem HCPolySupport.Book.Ch05.Section55.sUpper_add_beta_lt_one'_scalarPreliminaries {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : hP4.sUpper + Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 < 1

theorem HCPolySupport.Book.Ch05.Section55.sLower_add_beta_lt_one'_scalarPreliminaries {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : hP4.sLower + Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 < 1

theorem HCPolySupport.Book.Ch05.Section55.integrable_pow_of_nonneg_le_const_add_nonneg {d ξ : ℕ} {P : Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure P] {X E : RegCoeffField d → ℝ} {A : ℝ} (hξ : 1 ≤ ξ) (hA_nonneg : 0 ≤ A) (hX_nonneg : ∀ (a : RegCoeffField d), 0 ≤ X a) (hE_nonneg : ∀ (a : RegCoeffField d), 0 ≤ E a) (hX_le : ∀ (a : RegCoeffField d), X a ≤ A + E a) (hX_meas : AEMeasurable X P) (hE_meas : AEMeasurable E P) (hE_pow_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => E a ^ ξ) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => X a ^ ξ) P

theorem HCPolySupport.Book.Ch05.Section55.upperShiftedFactorPowerIntegrableAtScale_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 + Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4) (Ch02.MultiscaleExponent.finite 1) a ^ hP4.xi) P

theorem HCPolySupport.Book.Ch05.Section55.lowerShiftedFactorPowerIntegrableAtScale_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 + Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4) (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ hP4.xi) P

noncomputable def HCPolySupport.Book.Ch05.Section55.betaShiftedP4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) : QuantitativeCoarseGrainedEllipticity P

The quantitative ellipticity input with the Section 5.5 source exponents shifted by one β.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section55.thetaAtScale_le_betaShiftedWidetildeThetaAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (n : ℕ) : thetaAtScale hP hStruct ↑n ≤ betaShiftedWidetildeThetaAtScale P (↑n) hP4

Shifted scalar preliminary for Section 5.5: \Theta_n <= \widetilde\Theta_n^{(\beta)}.