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

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

Carrier canonical-minimizer measurability (Packet P5f)

This file re-aims the raw AEE-slice canonical doubled-Mu Hilbert-minimizer measurability spine (AEESliceAssembly/MuFamily.lean, measurable_energyBilin_fixed_..., stronglyMeasurable_canonicalAEEMuHilbertMinimizer_...) onto the honest carrier RegCoeffField d, exactly as CarrierMuFamily.lean re-aims the coarse-grained energy Mu.

As in CarrierMuFamily, the fine local σ-algebra of the raw slice subtype does not reflect into the honest entry-test carrier σ-algebra LocalSigmaR, so the raw primitives cannot be reused as black boxes. The honest route is identical: every measurability step factors through the L² coefficient realization, whose carrier measurability is measurable_toHilbertMatrixL2_carrier_cubeSet (a finite sum of localized entry-test generators). The Hilbert-space selection/limit scaffolding (dense generators, index selection, energy-gap limit) is entirely domain-generic and is transcribed here over a generic measurable source A : Ω → RegCoeffField d.

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

def HCPolySupport.slicePt {Ω : Type u_1} {d k : ℕ} (Q : TriadicCube d) (A : Ω → RegCoeffField d) (hSlice : ∀ (ω : Ω), AEEQuantitativeEllipticSlice (cubeSet Q) k (A ω).toFun) (ω : Ω) : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }

The raw AEE-slice element attached to a carrier source (public local copy of the CarrierMuFamily private helper).

Equations

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

theorem HCPolySupport.measurable_blockPairingAverage_carrier {Ω : 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 ω)) (X Y : BlockState d) (hX : MemBlockL2 (cubeSet Q) X.eval) (hY : MemBlockL2 (cubeSet Q) Y.eval) : Measurable fun (ω : Ω) => blockPairingAverage (cubeSet Q) (A ω).toFun X Y

Carrier block-pairing average measurability from hF (mirrors measurable_blockEnergyAverage_carrier).

theorem HCPolySupport.measurable_energyBilin_fixed_generator_carrier {Ω : 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) (Y : BlockState d) (hY : MemBlockL2 (cubeSet Q) Y.eval) (Z : ↥(canonicalMuBlockCorrectionGeneratorSubmodule (cubeSet Q))) : Measurable fun (ω : Ω) => ((canonicalAEEMuOperatorSystemData Q k (slicePt Q A hSlice ω)).toMuHilbertRealization.energyBilin (toHilbertBlockL2OfBlockField hY)) (blockVecToHilbertBlockL2Const P + ↑(canonicalMuCorrectionGeneratorEmbedding (cubeSet Q) Z))

Carrier version of the fixed-generator energy pairing measurability: it equals a fixed block-pairing average of the carrier field.

theorem HCPolySupport.stronglyMeasurable_canonicalMinimizer_carrier {Ω : 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) : MeasureTheory.StronglyMeasurable fun (ω : Ω) => (canonicalAEEMuOperatorSystemData Q k (slicePt Q A hSlice ω)).toMuHilbertRealization.minimizerMap P

Carrier canonical doubled-Mu Hilbert-minimizer strong measurability. Generic re-aim of stronglyMeasurable_canonicalAEEMuHilbertMinimizer_aeeQuantitativeSlice_cubeSet.

theorem HCPolySupport.measurable_energyBilin_fixed_canonicalMinimizer_carrier {Ω : 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) (Y : BlockState d) (hY : MemBlockL2 (cubeSet Q) Y.eval) : Measurable fun (ω : Ω) => ((canonicalAEEMuOperatorSystemData Q k (slicePt Q A hSlice ω)).toMuHilbertRealization.energyBilin (toHilbertBlockL2OfBlockField hY)) ((canonicalAEEMuOperatorSystemData Q k (slicePt Q A hSlice ω)).toMuHilbertRealization.minimizerMap P)

Carrier fixed-test energy-pairing measurability against the canonical minimizer. Generic re-aim of measurable_energyBilin_fixed_canonicalAEEMuHilbertMinimizer_aeeQuantitativeSlice_cubeSet.