Coarse-graining support:

Support.Book.Ch05.Theorems.Section52.PositiveExcessLowerAndIntegrability.LowerVariants

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

Section 5.2 internals: PositiveExcessLowerAndIntegrability

Lower large-scale estimates and factor integrability from P4.

theorem HCPolySupport.Book.Ch05.Section52.lowerLargeScalePositiveExcessRoot_le_largeScaleRootCoeff {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; (Ch04.annealedMomentRoot P hP4.xi fun (a : RegCoeffField d) => section52LargeScaleWeight hP4.sLower m n * parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm ((hP.barSigmaStarAtScale hStruct 0)⁻¹ • 1)) 0) ≤ ↑(Fintype.card (Fin d)) * ↑(Fintype.card (Fin d)) * section52LargeScaleRootCoeff d hP4.xi hP4.sLower m n * Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi

theorem HCPolySupport.Book.Ch05.Section52.lowerLargeScalePositiveExcessRoot_le_largeScaleRootCoeff_source {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {sSource r : ℝ} {ξ : ℕ} (hsSource : 0 < sSource) (hr_nonneg : 0 ≤ r) (hξ_one : 1 ≤ ξ) (hξ_two : 2 ≤ ξ) (hLowerSourceInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => (Ch04.lambdaSqCoeffField (originCube d 0) sSource (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ ξ) P) {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; (Ch04.annealedMomentRoot P ξ fun (a : RegCoeffField d) => section52LargeScaleWeight r m n * parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm ((hP.barSigmaStarAtScale hStruct 0)⁻¹ • 1)) 0) ≤ ↑(Fintype.card (Fin d)) * ↑(Fintype.card (Fin d)) * section52LargeScaleRootCoeff d ξ r m n * Ch04.lambdaInvMomentAtScale P 0 sSource ξ

theorem HCPolySupport.Book.Ch05.Section52.lowerLargeScalePositiveExcess_integrable_abs_pow {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; MeasureTheory.Integrable (fun (a : RegCoeffField d) => ‖section52LargeScaleWeight hP4.sLower m n * parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm ((hP.barSigmaStarAtScale hStruct 0)⁻¹ • 1)) 0‖ ^ hP4.xi) P

theorem HCPolySupport.Book.Ch05.Section52.lowerLargeScalePositiveExcess_integrable_abs_pow_source {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {sSource r : ℝ} {ξ : ℕ} (hsSource : 0 < sSource) (hξ_one : 1 ≤ ξ) (hξ_two : 2 ≤ ξ) (hLowerSourceInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => (Ch04.lambdaSqCoeffField (originCube d 0) sSource (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ ξ) P) {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; MeasureTheory.Integrable (fun (a : RegCoeffField d) => ‖section52LargeScaleWeight r m n * parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm ((hP.barSigmaStarAtScale hStruct 0)⁻¹ • 1)) 0‖ ^ ξ) P

theorem HCPolySupport.Book.Ch05.Section52.lowerLargeScalePositiveExcess_aemeasurable {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; AEMeasurable (fun (a : RegCoeffField d) => section52LargeScaleWeight hP4.sLower m n * parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm ((hP.barSigmaStarAtScale hStruct 0)⁻¹ • 1)) 0) P

theorem HCPolySupport.Book.Ch05.Section52.lowerLargeScalePositiveExcess_aemeasurable_source {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {r : ℝ} {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; AEMeasurable (fun (a : RegCoeffField d) => section52LargeScaleWeight r m n * parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm ((hP.barSigmaStarAtScale hStruct 0)⁻¹ • 1)) 0) P

theorem HCPolySupport.Book.Ch05.Section52.lowerLargeScalePositiveExcess_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) (a : RegCoeffField d) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; 0 ≤ section52LargeScaleWeight hP4.sLower m n * parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm ((hP.barSigmaStarAtScale hStruct 0)⁻¹ • 1)) 0

theorem HCPolySupport.Book.Ch05.Section52.lowerLargeScalePositiveExcess_nonneg_source {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {r : ℝ} (hr_nonneg : 0 ≤ r) {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) (a : RegCoeffField d) : let parents := descendantsAtScale (originCube d ↑m) n; have hparents := ⋯; 0 ≤ section52LargeScaleWeight r m n * parents.sup' hparents fun (Q : TriadicCube d) => max (Ch02.matrixNorm (coarseBlockMatrix (cubeSet Q) a.toFun).lowerRight - Ch02.matrixNorm ((hP.barSigmaStarAtScale hStruct 0)⁻¹ • 1)) 0