Coarse-graining support: Support.Book.Ch04.Internal.AEESliceAssembly.CarrierMuFamily

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

Carrier Mu measurability (Packet P5 centrepiece)

This file re-aims the raw AEE-slice Mu measurability spine onto the honest carrier RegCoeffField d. The raw spine (AEESliceAssembly/MuFamily.lean, BlockEnergyAverage.lean, FixedCompetitorEnergyMeasurability/**) proves measurability of the coarse-grained energy Mu on the raw slice subtype for the fine local σ-algebra AEEQuantitativeEllipticSlice.localMeasurableSpace, which is a comap of the powerset-fine PointwiseLocalSigma. The carrier redesign needs Mu measurable for the honest entry-test local σ-algebra LocalSigmaR (P4b), and the carrier's toFun does not reflect fine local events into LocalSigmaR (pointwise evaluations are not entry-test measurable — the Rao obstruction), so the fine spine cannot be reused as a black box.

The honest route re-derived here:

• every measurability step of the raw spine factors through the L² coefficient realization toHilbertMatrixL2 (the block-energy averages and hence Mu are Borel functions of it); the raw building blocks (measurable_l2WeightedHilbertMatrixLipschitzIntegral, measurable_blockEnergyAverage_comp_of_measurable_weightedFullBlockCoeffEntryIntegrals, measurable_Mu_comp_of_measurable_blockEnergyAverage_affineField_denseSeq) are domain-generic, taking the L² realization's measurability as an input;
• the one genuinely new fact is that the L² realization of a carrier field is LocalSigmaR-measurable — proved by the dense-probe inner-product criterion, whose inner products are exactly the localized entry-test generators entryTestR of the carrier (measurable_entryTestR_localSigmaR), not the fine pointwise data.

The result measurable_Mu_comp_aeeSlice_of_measurable_entryTest is the generic engine consumed by Theorems/Mu.lean.

Reference: the paper (Armstrong–Kuusi–Loher, to appear).

def HCPolySupport.rawSlice {Ω : Type u_1} {d : ℕ} {U : Set (Vec d)} {k : ℕ} (A : Ω → RegCoeffField d) (hSlice : ∀ (ω : Ω), AEEQuantitativeEllipticSlice U k (A ω).toFun) (ω : Ω) : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }

The raw AEE-slice element attached to a carrier source.

Equations

• HCPolySupport.rawSlice A hSlice ω = ⟨(A ω).toFun, ⋯⟩

theorem HCPolySupport.measurable_inner_toScalarL2_hilbertMatrixL2Entry_carrier {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {A : Ω → RegCoeffField d} {hSlice : ∀ (ω : Ω), AEEQuantitativeEllipticSlice U k (A ω).toFun} (hU : MeasurableSet U) (hEntry : ∀ (i j : Fin d) {φ : Vec d → ℝ}, ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → Measurable fun (ω : Ω) => entryTestR i j φ (A ω)) (i j : Fin d) {φ : Vec d → ℝ} (hφL2 : MemScalarL2 U φ) (hφ_cont : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_support : tsupport φ ⊆ U) : Measurable fun (ω : Ω) => inner ℝ (toScalarL2 hφL2) ((QuantitativeEllipticSlice.hilbertMatrixL2Entry i j) (AEEQuantitativeEllipticSlice.toHilbertMatrixL2 (rawSlice A hSlice ω)))

Scalar-entry inner product of the carrier L² realization against a smooth, compactly supported scalar probe supported in U is a localized entry-test generator of the carrier field, hence mΩ-measurable.

theorem HCPolySupport.measurable_inner_hilbertMatrixSmoothProbe_toHilbertMatrixL2_carrier {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {A : Ω → RegCoeffField d} {hSlice : ∀ (ω : Ω), AEEQuantitativeEllipticSlice U k (A ω).toFun} (hU : MeasurableSet U) (hEntry : ∀ (i j : Fin d) {φ : Vec d → ℝ}, ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → Measurable fun (ω : Ω) => entryTestR i j φ (A ω)) {g : Vec d → HilbertMat d} (hgL2 : MeasureTheory.MemLp g 2 (volumeMeasureOn U)) (hg_cont : ContDiff ℝ (↑⊤) g) (hg_compact : HasCompactSupport g) (hg_support : tsupport g ⊆ U) : Measurable fun (ω : Ω) => inner ℝ (MeasureTheory.MemLp.toLp g hgL2) (AEEQuantitativeEllipticSlice.toHilbertMatrixL2 (rawSlice A hSlice ω))

Smooth HilbertMat-valued probe inner product of the carrier L² realization is mΩ-measurable: it decomposes into a finite sum of localized scalar entry-test generators of the carrier field.

theorem HCPolySupport.measurable_toHilbertMatrixL2_carrier {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {A : Ω → RegCoeffField d} {hSlice : ∀ (ω : Ω), AEEQuantitativeEllipticSlice U k (A ω).toFun} (hU : MeasurableSet U) (hEntry : ∀ (i j : Fin d) {φ : Vec d → ℝ}, ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → Measurable fun (ω : Ω) => entryTestR i j φ (A ω)) (hUopen : IsOpen U) (hUfinite : MeasureTheory.volume U ≠ ⊤) : Measurable fun (ω : Ω) => AEEQuantitativeEllipticSlice.toHilbertMatrixL2 (rawSlice A hSlice ω)

The carrier L² coefficient realization is mΩ-measurable. Proved by the dense smooth-probe inner-product criterion; each inner product is a finite sum of localized entry-test generators of the carrier field.

Block-energy averages and Mu from the carrier L² realization

These lemmas take the carrier L² realization's measurability hF (produced by measurable_toHilbertMatrixL2_carrier) and thread the domain-generic raw block-energy → Mu spine. The weighted-integral atoms mirror BlockEnergyAverage.lean, replacing the subtype L² realization with hF.

theorem HCPolySupport.measurable_l2WeightedFullBlockCoeffEntry_carrier {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {A : Ω → RegCoeffField d} {hSlice : ∀ (ω : Ω), AEEQuantitativeEllipticSlice U k (A ω).toFun} (hF : Measurable fun (ω : Ω) => AEEQuantitativeEllipticSlice.toHilbertMatrixL2 (rawSlice A hSlice ω)) {w : Vec d → ℝ} (hw : MemScalarL2 U w) (α β : BlockCoord d) : Measurable fun (ω : Ω) => ∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (A ω).toFun x) α β

Carrier version of the L²-weighted full-block coefficient-entry integral measurability, for an L² weight.

theorem HCPolySupport.measurable_integrableWeightedFullBlockCoeffEntry_carrier_of_measurable {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {A : Ω → RegCoeffField d} {hSlice : ∀ (ω : Ω), AEEQuantitativeEllipticSlice U k (A ω).toFun} (hF : Measurable fun (ω : Ω) => AEEQuantitativeEllipticSlice.toHilbertMatrixL2 (rawSlice A hSlice ω)) {w : Vec d → ℝ} (hw_meas : Measurable w) (hw_int : MeasureTheory.Integrable w (volumeMeasureOn U)) (α β : BlockCoord d) : Measurable fun (ω : Ω) => ∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (A ω).toFun x) α β

Carrier version of the L²-weighted full-block coefficient-entry integral measurability, for an integrable weight (L² weights are dense; simple-function approximation upgrades the previous lemma).

theorem HCPolySupport.measurable_integrableWeightedFullBlockCoeffEntry_carrier {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {A : Ω → RegCoeffField d} {hSlice : ∀ (ω : Ω), AEEQuantitativeEllipticSlice U k (A ω).toFun} (hF : Measurable fun (ω : Ω) => AEEQuantitativeEllipticSlice.toHilbertMatrixL2 (rawSlice A hSlice ω)) {w : Vec d → ℝ} (hw : MeasureTheory.Integrable w (volumeMeasureOn U)) (α β : BlockCoord d) : Measurable fun (ω : Ω) => ∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (A ω).toFun x) α β

Carrier version, for a general integrable weight (drop the measurability of w by passing to a measurable representative).

theorem HCPolySupport.measurable_blockEnergyAverage_carrier {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {A : Ω → RegCoeffField d} {hSlice : ∀ (ω : Ω), AEEQuantitativeEllipticSlice U k (A ω).toFun} (hF : Measurable fun (ω : Ω) => AEEQuantitativeEllipticSlice.toHilbertMatrixL2 (rawSlice A hSlice ω)) (X : BlockState d) (hX : MemBlockL2 U X.eval) : Measurable fun (ω : Ω) => blockEnergyAverage U (A ω).toFun X

Carrier block-energy average measurability from hF.

The generic engine

theorem HCPolySupport.measurable_toHilbertMatrixL2_carrier_cubeSet {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {d k : ℕ} (Q : TriadicCube d) {A : Ω → RegCoeffField d} (hSlice : ∀ (ω : Ω), AEEQuantitativeEllipticSlice (cubeSet Q) k (A ω).toFun) (hEntry : ∀ (i j : Fin d) {φ : Vec d → ℝ}, ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ cubeSet Q → Measurable fun (ω : Ω) => entryTestR i j φ (A ω)) : Measurable fun (ω : Ω) => AEEQuantitativeEllipticSlice.toHilbertMatrixL2 (rawSlice A hSlice ω)

Carrier L² realization measurability on a triadic cube. The half-open cube is not open, so density of smooth probes is imported from the open core (the two restricted volume measures agree).

theorem HCPolySupport.measurable_Mu_comp_aeeSlice_of_measurable_entryTest {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {d k : ℕ} (Q : TriadicCube d) {A : Ω → RegCoeffField d} (hSlice : ∀ (ω : Ω), AEEQuantitativeEllipticSlice (cubeSet Q) k (A ω).toFun) (hEntry : ∀ (i j : Fin d) {φ : Vec d → ℝ}, ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ cubeSet Q → Measurable fun (ω : Ω) => entryTestR i j φ (A ω)) (P : BlockVec d) : Measurable fun (ω : Ω) => Mu (cubeSet Q) P (A ω).toFun

The generic carrier Mu measurability engine. Given a carrier source A landing a.e.-elliptically in the AEE quantitative k-slice of a triadic cube, whose localized entry-test generators are mΩ-measurable, the coarse-grained energy ω ↦ Mu (cubeSet Q) P (A ω).toFun is mΩ-measurable. This is the P5 carrier re-aim of the raw Mu-slice measurability spine.