Coarse-graining support: Support.Book.Ch04.Theorems.MomentFactorBounds.Apex #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Book.Ch04.RestrictionLawCarrier.integrable_coarseFullBlockMatrixAtCube_of_integrable_factor_observables
{d : ℕ}
[NeZero d]
{P : RestrictionCoeffLaw d}
(hP : RestrictionLawCarrier P)
(Q : TriadicCube d)
{sUpper sLower : ℝ}
{ξ : ℕ}
(hsUpper : 0 < sUpper)
(hsLower : 0 < sLower)
(hξ : 1 ≤ ξ)
(hUpperPowInt :
MeasureTheory.Integrable
(fun (a : RegCoeffField d) => LambdaSqCoeffField Q sUpper (Ch02.MultiscaleExponent.finite 1) a ^ ξ) P)
(hLowerPowInt :
MeasureTheory.Integrable
(fun (a : RegCoeffField d) => (lambdaSqCoeffField Q sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ ξ) P)
:
A full coarse block is integrable as soon as the two factor observables on
the same cube have finite ξ moments.
This is the Ch4 source theorem that prevents Ch5 from carrying a separate full-block integrability hypothesis once it has the factor moments.
theorem
HCPolySupport.Book.Ch04.RestrictionLawCarrier.integrable_coarseFullBlockMatrixAtCube_origin_of_integrable_factor_observables
{d : ℕ}
[NeZero d]
{P : RestrictionCoeffLaw d}
(hP : RestrictionLawCarrier P)
{sUpper sLower : ℝ}
{ξ : ℕ}
(hsUpper : 0 < sUpper)
(hsLower : 0 < sLower)
(hξ : 1 ≤ ξ)
(hUpperPowInt :
MeasureTheory.Integrable
(fun (a : RegCoeffField d) => LambdaSqCoeffField (originCube d 0) sUpper (Ch02.MultiscaleExponent.finite 1) a ^ ξ)
P)
(hLowerPowInt :
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
(lambdaSqCoeffField (originCube d 0) sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ ξ)
P)
:
The unit full coarse block is integrable as soon as the two unit factor
observables in (P4) have finite ξ moments.
theorem
HCPolySupport.Book.Ch04.RestrictionLawCarrier.barSigmaAtScale_le_LambdaMomentAtScale_of_integrable_factor_observables
{d : ℕ}
[NeZero d]
{P : RestrictionCoeffLaw d}
(hP : RestrictionLawCarrier P)
(hStruct : RestrictionStructuralLaw P)
{sUpper sLower : ℝ}
{ξ : ℕ}
(hsUpper : 0 < sUpper)
(hsLower : 0 < sLower)
(hξ : 1 ≤ ξ)
(hBlock : ∀ (n : ℕ), MeasureTheory.Integrable (coarseFullBlockMatrixAtCube (originCube d ↑n)) P)
(hUpperMeas :
∀ (n : ℕ),
AEMeasurable
(fun (a : RegCoeffField d) => LambdaSqCoeffField (originCube d ↑n) sUpper (Ch02.MultiscaleExponent.finite 1) a) P)
(hLowerMeas :
∀ (n : ℕ),
AEMeasurable
(fun (a : RegCoeffField d) =>
(lambdaSqCoeffField (originCube d ↑n) sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹)
P)
(hUpperPowInt :
∀ (n : ℕ),
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
LambdaSqCoeffField (originCube d ↑n) sUpper (Ch02.MultiscaleExponent.finite 1) a ^ ξ)
P)
(hLowerPowInt :
∀ (n : ℕ),
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
(lambdaSqCoeffField (originCube d ↑n) sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ ξ)
P)
(n : ℕ)
:
Structural-law upper scalar factor bound from integrable moment observables.
theorem
HCPolySupport.Book.Ch04.RestrictionLawCarrier.barSigmaStarAtScale_inv_le_lambdaInvMomentAtScale_of_integrable_factor_observables
{d : ℕ}
[NeZero d]
{P : RestrictionCoeffLaw d}
(hP : RestrictionLawCarrier P)
(hStruct : RestrictionStructuralLaw P)
{sUpper sLower : ℝ}
{ξ : ℕ}
(hsUpper : 0 < sUpper)
(hsLower : 0 < sLower)
(hξ : 1 ≤ ξ)
(hBlock : ∀ (n : ℕ), MeasureTheory.Integrable (coarseFullBlockMatrixAtCube (originCube d ↑n)) P)
(hUpperMeas :
∀ (n : ℕ),
AEMeasurable
(fun (a : RegCoeffField d) => LambdaSqCoeffField (originCube d ↑n) sUpper (Ch02.MultiscaleExponent.finite 1) a) P)
(hLowerMeas :
∀ (n : ℕ),
AEMeasurable
(fun (a : RegCoeffField d) =>
(lambdaSqCoeffField (originCube d ↑n) sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹)
P)
(hUpperPowInt :
∀ (n : ℕ),
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
LambdaSqCoeffField (originCube d ↑n) sUpper (Ch02.MultiscaleExponent.finite 1) a ^ ξ)
P)
(hLowerPowInt :
∀ (n : ℕ),
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
(lambdaSqCoeffField (originCube d ↑n) sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ ξ)
P)
(n : ℕ)
:
Structural-law lower inverse-star scalar factor bound from integrable moment observables.
theorem
HCPolySupport.Book.Ch04.RestrictionLawCarrier.thetaAtScale_le_widetildeThetaAtScale_of_integrable_factor_observables
{d : ℕ}
[NeZero d]
{P : RestrictionCoeffLaw d}
(hP : RestrictionLawCarrier P)
(hStruct : RestrictionStructuralLaw P)
{sUpper sLower : ℝ}
{ξ : ℕ}
(hsUpper : 0 < sUpper)
(hsLower : 0 < sLower)
(hξ : 1 ≤ ξ)
(hBlock : ∀ (n : ℕ), MeasureTheory.Integrable (coarseFullBlockMatrixAtCube (originCube d ↑n)) P)
(hUpperMeas :
∀ (n : ℕ),
AEMeasurable
(fun (a : RegCoeffField d) => LambdaSqCoeffField (originCube d ↑n) sUpper (Ch02.MultiscaleExponent.finite 1) a) P)
(hLowerMeas :
∀ (n : ℕ),
AEMeasurable
(fun (a : RegCoeffField d) =>
(lambdaSqCoeffField (originCube d ↑n) sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹)
P)
(hUpperPowInt :
∀ (n : ℕ),
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
LambdaSqCoeffField (originCube d ↑n) sUpper (Ch02.MultiscaleExponent.finite 1) a ^ ξ)
P)
(hLowerPowInt :
∀ (n : ℕ),
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
(lambdaSqCoeffField (originCube d ↑n) sLower (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ ξ)
P)
(n : ℕ)
:
Direct structural-law comparison Theta_n <= widetildeTheta_n from
integrable moment observables.