Coarse-graining support: #
Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.ResponseMomentIntegrability
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Response moment integrability #
This proof-internal file exposes the origin-cube ΞΆ-moment integrability of
the response observable from the L^2 response surface and (P4).
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integrable_rpow_restrictionResponseJObservableCubeSet_originCube_from_P4
{d : β}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(k : β)
(p q : Vec d)
:
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
(Ch04.restrictionResponseJObservableCubeSet (originCube d βk) p q a).rpow (section53CoarseFluctuationZeta hP4))
P