Coarse-graining support: Support.Book.Ch05.Theorems.Section52.P4Integrability

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

Section 5.2 internals: P4Integrability

Origin-block integrability consequences of P4.

theorem HCPolySupport.Book.Ch05.Section52.originBlockIntegrableAtScale_from_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d ↑m)) P

theorem HCPolySupport.Book.Ch05.Section52.memLp_two_coarseBlockMatrixEntry_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (n : ℕ) (α β : BlockCoord d) : MeasureTheory.MemLp (fun (a : RegCoeffField d) => blockMatEntry (coarseBlockMatrix (cubeSet (originCube d ↑n)) a.toFun) α β) 2 P

theorem HCPolySupport.Book.Ch05.Section52.integrable_fullBlockFluctuationNormSquare_of_P4_atOrigin {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℤ) (n : ℕ) : MeasureTheory.Integrable (Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct m (originCube d ↑n)) P