Coarse-graining support: #
Support.Book.Ch05.Theorems.Section52.PositiveExcessLowerAndIntegrability.PowIntegrable
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Book.Ch05.Section52.section52_integrable_abs_pow_of_ae_abs_le_nonneg
{d : ℕ}
{P : Ch04.RestrictionCoeffLaw d}
{ξ : ℕ}
{X Y : RegCoeffField d → ℝ}
(hX_aemeas : AEMeasurable X P)
(hY_nonneg : ∀ (a : RegCoeffField d), 0 ≤ Y a)
(hXY : ∀ᵐ (a : RegCoeffField d) ∂P, |X a| ≤ Y a)
(hY_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Y a| ^ ξ) P)
:
MeasureTheory.Integrable (fun (a : RegCoeffField d) => |X a| ^ ξ) P
theorem
HCPolySupport.Book.Ch05.Section52.section52_integrable_abs_finset_sum_pow_of_integrable_abs_pow
{d : ℕ}
{P : Ch04.RestrictionCoeffLaw d}
{ι : Type u_1}
{ξ : ℕ}
{s : Finset ι}
{G : ι → RegCoeffField d → ℝ}
(hξ : 1 ≤ ξ)
(hG_aemeas : ∀ i ∈ s, AEMeasurable (G i) P)
(hG_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (a : RegCoeffField d) => |G i a| ^ ξ) P)
:
MeasureTheory.Integrable (fun (a : RegCoeffField d) => |∑ i ∈ s, G i a| ^ ξ) P
theorem
HCPolySupport.Book.Ch05.Section52.section52_integrable_abs_positiveExcess_pow_of_ae_finset_sum_bound
{d : ℕ}
{P : Ch04.RestrictionCoeffLaw d}
{ι : Type u_1}
{ξ : ℕ}
{s : Finset ι}
{X : RegCoeffField d → ℝ}
{base : ℝ}
{G : ι → RegCoeffField d → ℝ}
(hξ : 1 ≤ ξ)
(hX_aemeas : AEMeasurable X P)
(hG_nonneg : ∀ i ∈ s, ∀ (a : RegCoeffField d), 0 ≤ G i a)
(hG_aemeas : ∀ i ∈ s, AEMeasurable (G i) P)
(hG_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (a : RegCoeffField d) => |G i a| ^ ξ) P)
(hPoint : ∀ᵐ (a : RegCoeffField d) ∂P, max (X a - base) 0 ≤ ∑ i ∈ s, G i a)
:
MeasureTheory.Integrable (fun (a : RegCoeffField d) => |max (X a - base) 0| ^ ξ) P
theorem
HCPolySupport.Book.Ch05.Section52.upper_unitDescendant_Lambda_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.upperFactorPowerIntegrableAtScale_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 (Ch02.MultiscaleExponent.finite 1) a ^ hP4.xi)
P