Coarse-graining support: #
Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.FluctuationIntegrability
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.memLp_two_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.MemLp (Ch04.restrictionResponseJObservableCubeSet (originCube d ↑k) p q) 2 P
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.memLp_two_responseObservable
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hstat : Ch04.RestrictionStationaryLaw P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(R : TriadicCube d)
(hR_nonneg : 0 ≤ R.scale)
(p q : Vec d)
:
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.memLp_zeta_restrictionResponseJObservableCubeSet_cubeSet_from_P4_of_stationary
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hstat : Ch04.RestrictionStationaryLaw P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(R : TriadicCube d)
(hR_nonneg : 0 ≤ R.scale)
(p q : Vec d)
:
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.zeta_descendantResponseObservable_memLp_from_P4_of_stationarity
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hstat : Ch04.RestrictionStationaryLaw P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
{k m : ℤ}
(hk_nonneg : 0 ≤ k)
(hkm : k ≤ m)
(p q : Vec d)
:
MeasureTheory.MemLp
(fun (a : RegCoeffField d) =>
descendantsAverage (originCube d m) (m - k).toNat fun (R : TriadicCube d) =>
Ch04.restrictionResponseJObservableCubeSet R p q a)
(ENNReal.ofReal (section53CoarseFluctuationZeta hP4)) P
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integral_rpow_responseJ_cubeSet_eq_origin_of_stationarity
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hstat : Ch04.RestrictionStationaryLaw P)
(R : TriadicCube d)
(hR_nonneg : 0 ≤ R.scale)
{ζ : ℝ}
(hζ_nonneg : 0 ≤ ζ)
(p q : Vec d)
:
∫ (a : RegCoeffField d), (Ch04.restrictionResponseJObservableCubeSet R p q a).rpow ζ ∂P = ∫ (a : RegCoeffField d), (Ch04.restrictionResponseJObservableCubeSet (originCube d R.scale) p q a).rpow ζ ∂P
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integral_rpow_descendantMean_responseJObservableSet_cube_le_cube
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hstat : Ch04.RestrictionStationaryLaw P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
{k m : ℤ}
(hk_nonneg : 0 ≤ k)
(hkm : k ≤ m)
(p q : Vec d)
:
have ζ := section53CoarseFluctuationZeta hP4;
∫ (a : RegCoeffField d), (descendantsAverage (originCube d m) (m - k).toNat fun (R : TriadicCube d) =>
Ch04.restrictionResponseJObservableCubeSet R p q a).rpow
ζ ∂P ≤ ∫ (a : RegCoeffField d), (Ch04.restrictionResponseJObservableCubeSet (originCube d k) p q a).rpow ζ ∂P