Coarse-graining support: #
Support.Book.Ch05.Theorems.Section52.PositiveExcessLowerAndIntegrability.UnitDescendantSup
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Book.Ch05.Section52.section52_annealedMomentRoot_le_const_mul_of_ae_le
{d : ℕ}
{P : Ch04.RestrictionCoeffLaw d}
{ξ : ℕ}
{c : ℝ}
{X Y : RegCoeffField d → ℝ}
(hξ : 1 ≤ ξ)
(hc : 0 ≤ c)
(hX_nonneg : ∀ (a : RegCoeffField d), 0 ≤ X a)
(hY_nonneg : ∀ (a : RegCoeffField d), 0 ≤ Y a)
(hX_aemeas : AEMeasurable X P)
(hY_abs_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Y a| ^ ξ) P)
(hXY : X ≤ᵐ[P] fun (a : RegCoeffField d) => c * Y a)
:
theorem
HCPolySupport.Book.Ch05.Section52.upper_unitDescendantSup_integrable_abs_pow
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
{s : ℝ}
{ξ m : ℕ}
(hs : 0 < s)
(hξ_one : 1 ≤ ξ)
(hSourceInt :
MeasureTheory.Integrable
(fun (a : RegCoeffField d) => Ch04.LambdaSqCoeffField (originCube d 0) s (Ch02.MultiscaleExponent.finite 1) a ^ ξ)
P)
:
let D := descendantsAtScale (originCube d ↑m) 0;
have hD := ⋯;
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
|D.sup' hD fun (U : TriadicCube d) => Ch04.LambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a| ^ ξ)
P
theorem
HCPolySupport.Book.Ch05.Section52.upper_unitDescendantSup_aemeasurable
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
{s : ℝ}
{m : ℕ}
(hs : 0 < s)
:
let D := descendantsAtScale (originCube d ↑m) 0;
have hD := ⋯;
AEMeasurable
(fun (a : RegCoeffField d) =>
D.sup' hD fun (U : TriadicCube d) => Ch04.LambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a)
P
theorem
HCPolySupport.Book.Ch05.Section52.upper_unitDescendantSup_nonneg
{d : ℕ}
{s : ℝ}
{m : ℕ}
(hs : 0 < s)
(a : RegCoeffField d)
:
let D := descendantsAtScale (originCube d ↑m) 0;
have hD := ⋯;
0 ≤ D.sup' hD fun (U : TriadicCube d) => Ch04.LambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a
theorem
HCPolySupport.Book.Ch05.Section52.lower_unitDescendant_lambdaInv_integrable_abs_pow
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
{s : ℝ}
{ξ m : ℕ}
(hs : 0 < s)
(hSourceInt :
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
(Ch04.lambdaSqCoeffField (originCube d 0) s (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ ξ)
P)
{U : TriadicCube d}
(hU : U ∈ descendantsAtScale (originCube d ↑m) 0)
:
MeasureTheory.Integrable
(fun (a : RegCoeffField d) => |(Ch04.lambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a)⁻¹| ^ ξ) P
theorem
HCPolySupport.Book.Ch05.Section52.lower_unitDescendantSup_integrable_abs_pow
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
{s : ℝ}
{ξ m : ℕ}
(hs : 0 < s)
(hξ_one : 1 ≤ ξ)
(hSourceInt :
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
(Ch04.lambdaSqCoeffField (originCube d 0) s (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ ξ)
P)
:
let D := descendantsAtScale (originCube d ↑m) 0;
have hD := ⋯;
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
|D.sup' hD fun (U : TriadicCube d) => (Ch04.lambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a)⁻¹| ^ ξ)
P
theorem
HCPolySupport.Book.Ch05.Section52.lower_unitDescendantSup_aemeasurable
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
{s : ℝ}
{m : ℕ}
(hs : 0 < s)
:
let D := descendantsAtScale (originCube d ↑m) 0;
have hD := ⋯;
AEMeasurable
(fun (a : RegCoeffField d) =>
D.sup' hD fun (U : TriadicCube d) => (Ch04.lambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a)⁻¹)
P
theorem
HCPolySupport.Book.Ch05.Section52.lower_unitDescendantSup_nonneg
{d : ℕ}
{s : ℝ}
{m : ℕ}
(hs : 0 < s)
(a : RegCoeffField d)
:
let D := descendantsAtScale (originCube d ↑m) 0;
have hD := ⋯;
0 ≤ D.sup' hD fun (U : TriadicCube d) => (Ch04.lambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a)⁻¹
theorem
HCPolySupport.Book.Ch05.Section52.lowerFactorPowerIntegrableAtScale_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 (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ hP4.xi)
P