Coarse-graining support: Support.CoarseGraining.CoarseBounds.LawObservable

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

Law-level measurability and integrability of the coarse observable (item C3)

The scalar coarse observable a ↦ P · 𝐀(cubeSet (originCube d n); a) P is almost-everywhere-strongly-measurable under any Chapter 4 RestrictionLawCarrier, and — under a ThetaEllipticLaw — almost surely lands in [0, 2(Θ|p|² + |q|²)] and is integrable.

The RestrictionLawCarrier a.e.-measurability of every coarse block-matrix entry is already available (RestrictionLawCarrier.aemeasurable_coarseBlockMatrix_{upperLeft,upperRight,lowerLeft, lowerRight}_apply_cubeSet, all polarizations of aemeasurable_Mu_cubeSet); we wrap those into the scalar quadratic observable. The a.s. deterministic bound comes from feeding the a.e.-elliptic realizations through the C2 bridge to an everywhere-elliptic representative and applying the C1′ scalar sandwich.

Measurability

theorem HCPolySupport.aestronglyMeasurable_coarseBlockQuadratic_cubeSet {d : ℕ} {L : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier L) (n : ℤ) (P : BlockVec d) : MeasureTheory.AEStronglyMeasurable (fun (a : RegCoeffField d) => blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d n)) a.toFun) P)) L

C3 (measurability). The scalar coarse observable a ↦ P · 𝐀(cubeSet (originCube d n); a) P is a.e.-strongly-measurable under any RestrictionLawCarrier.

A.s. bounds and integrability

The ThetaEllipticLaw hypothesis provides only a.e.-in-x ellipticity of the realizations, with no spatial measurability, so it cannot be turned into a per-realization IsEllipticFieldOn without an additional measurable-representative construction (which would descend through IsAEEllipticFieldOn and the C2 truncation with a chosen strongly-measurable representative). We therefore deliver the bounds/integrability against the pointwise substitute ∀ᵐ a ∂L, IsEllipticFieldOn 1 Θ (cubeSet (originCube d n)) a, from which the deterministic C1′ sandwich transfers realization-by-realization.

theorem HCPolySupport.coarseBlockQuadratic_ae_bounds_of_ae_isEllipticFieldOn {d : ℕ} [NeZero d] {L : Book.Ch04.RestrictionCoeffLaw d} {Θ : ℝ} (n : ℤ) (P : BlockVec d) (hell : ∀ᵐ (a : RegCoeffField d) ∂L, IsEllipticFieldOn 1 Θ (cubeSet (originCube d n)) a.toFun) : ∀ᵐ (a : RegCoeffField d) ∂L, 0 ≤ blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d n)) a.toFun) P) ∧ blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d n)) a.toFun) P) ≤ 2 * (Θ * vecNormSq P.1 + vecNormSq P.2)

C3 (a.s. bounds). Under an a.s.-(1, Θ)-elliptic law, the coarse observable a.s. lands in [0, 2(Θ|p|² + |q|²)].

theorem HCPolySupport.integrable_coarseBlockQuadratic_of_ae_isEllipticFieldOn {d : ℕ} [NeZero d] {L : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier L) {Θ : ℝ} (n : ℤ) (P : BlockVec d) (hell : ∀ᵐ (a : RegCoeffField d) ∂L, IsEllipticFieldOn 1 Θ (cubeSet (originCube d n)) a.toFun) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d n)) a.toFun) P)) L

C3 (integrability). Under a RestrictionLawCarrier (for measurability) and an a.s.-(1, Θ)-elliptic law (for the deterministic bound), the coarse observable is integrable.