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

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

Audit tag (Ch4 rebuild contract CH04_REBUILD_SURFACE_2026-05-16.md)

Internal claim: measurability of the Mu operator family restricted to AEEQuantitativeEllipticSlices, plus the progressive composition variants (raw Mu → composed Mu → a.e. Mu) needed by the Theorems/Mu.lean and Theorems/CanonicalSolutions.lean consumers. Combines AEESliceAssembly/BlockEnergyAverage.lean with the FixedCompetitorEnergyMeasurability chain on the AEE side of the slice predicate.

Consumed by:

• Theorems/Mu.lean :: aemeasurable_Mu_cubeSet and aemeasurable_Mu_cubeSet_of_measurable_aeeQuantitativeSlice
• Theorems/CanonicalSolutions.lean :: aestronglyMeasurable_canonicalMuHilbertMinimizer_cubeSet and the rest of the canonical-solution measurability surface.

If the single-claim summary above grows into three or more distinct claims, split or refactor per the rebuild contract.

theorem HCPolySupport.measurable_Mu_aeeQuantitativeSlice {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hToL2 : Measurable AEEQuantitativeEllipticSlice.toHilbertMatrixL2) (R : MuCorrectionSpaceRecoveryData U) [TopologicalSpace.SeparableSpace ↥R.correctionSpace] (system : (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a) (mu_eq_muCandidate : ∀ (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) (P : BlockVec d), Mu U P ↑a = ((system a).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) : Measurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) => Mu U P ↑a

theorem HCPolySupport.measurable_Mu_aeeQuantitativeSlice_canonical_cubeSet {d : ℕ} (Q : TriadicCube d) {k : ℕ} (P : BlockVec d) : Measurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) => Mu (cubeSet Q) P ↑a

Canonical AEE cube-slice measurability of Mu, with the Ch4 canonical operator/generator plumbing supplied internally.

theorem HCPolySupport.stronglyMeasurable_canonicalMuMinimizer {d : ℕ} (Q : TriadicCube d) {k : ℕ} (P : BlockVec d) : MeasureTheory.StronglyMeasurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) => (canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization.minimizerMap P

Canonical AEE cube-slice strong measurability of the selected doubled-Mu Hilbert maximizer/minimizer. The proof selects the first dense generator whose block energy is within 1 / (m + 1) of Mu, and then passes to the Hilbert energy-gap limit.

theorem HCPolySupport.measurable_energyBilin_fixed_canonicalAEEMuHilbertMinimizer_aeeQuantitativeSlice_cubeSet {d : ℕ} (Q : TriadicCube d) {k : ℕ} (P : BlockVec d) (Y : BlockState d) (hY : MemBlockL2 (cubeSet Q) Y.eval) : Measurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) => ((canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization.energyBilin (toHilbertBlockL2OfBlockField hY)) ((canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization.minimizerMap P)

Canonical AEE cube-slice measurability of a fixed block-L² test paired through the Hilbert energy form with the selected canonical doubled-Mu minimizer. This is the source primitive for scalar-response operator-image averages: the proof uses the same dense-generator selection as the minimizer measurability theorem, then passes the fixed continuous bilinear functional to the limit.

theorem HCPolySupport.measurable_Mu_comp_aeeQuantitativeSlice_canonical_cubeSet {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (Q : TriadicCube d) {k : ℕ} (A : Ω → CoeffField d) (hA : IsPointwiseLocalSigmaMeasurableOn A (cubeSet Q)) (hSlice : ∀ (ω : Ω), AEEQuantitativeEllipticSlice (cubeSet Q) k (A ω)) (P : BlockVec d) : Measurable fun (ω : Ω) => Mu (cubeSet Q) P (A ω)

Canonical composed AEE cube-slice measurability of Mu.

theorem HCPolySupport.measurable_Mu_comp_countable_aeeQuantitativeSlice_canonical_cubeSet_cover {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (Q : TriadicCube d) (A : Ω → CoeffField d) (hA : IsPointwiseLocalSigmaMeasurableOn A (cubeSet Q)) (t : ℕ → Set Ω) (ht : ∀ (k : ℕ), MeasurableSet (t k)) (hcover : ⋃ (k : ℕ), t k = Set.univ) (hSlice : ∀ (k : ℕ), ∀ ω ∈ t k, AEEQuantitativeEllipticSlice (cubeSet Q) k (A ω)) (P : BlockVec d) : Measurable fun (ω : Ω) => Mu (cubeSet Q) P (A ω)

Canonical countable-cover AEE cube-slice measurability of Mu.

theorem HCPolySupport.aemeasurable_Mu_comp_countable_aeeQuantitativeSlice_canonical_cubeSet_cover {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {d : ℕ} (Q : TriadicCube d) (A : Ω → CoeffField d) (hA : IsPointwiseLocalSigmaMeasurableOn A (cubeSet Q)) (t : ℕ → Set Ω) (ht : ∀ (k : ℕ), MeasurableSet (t k)) (hcover_ae : ∀ᵐ (ω : Ω) ∂μ, ω ∈ ⋃ (k : ℕ), t k) (hSlice : ∀ (k : ℕ), ∀ ω ∈ t k, AEEQuantitativeEllipticSlice (cubeSet Q) k (A ω)) (P : BlockVec d) : AEMeasurable (fun (ω : Ω) => Mu (cubeSet Q) P (A ω)) μ

Canonical a.e. countable-cover AEE cube-slice measurability of Mu.

theorem HCPolySupport.measurable_Mu_comp_aeeQuantitativeSlice_canonical_cubeSet_sets {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} (Q : TriadicCube d) (A : Ω → CoeffField d) (hA : IsPointwiseLocalSigmaMeasurableOn A (cubeSet Q)) (hSliceMeas : ∀ (k : ℕ), MeasurableSet {ω : Ω | AEEQuantitativeEllipticSlice (cubeSet Q) k (A ω)}) (hcover : ∀ (ω : Ω), ∃ (k : ℕ), AEEQuantitativeEllipticSlice (cubeSet Q) k (A ω)) (P : BlockVec d) : Measurable fun (ω : Ω) => Mu (cubeSet Q) P (A ω)

Canonical set-cover AEE cube-slice measurability of Mu.

theorem HCPolySupport.aemeasurable_Mu_comp_aeeQuantitativeSlice_canonical_cubeSet_sets {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {d : ℕ} (Q : TriadicCube d) (A : Ω → CoeffField d) (hA : IsPointwiseLocalSigmaMeasurableOn A (cubeSet Q)) (hSliceMeas : ∀ (k : ℕ), MeasurableSet {ω : Ω | AEEQuantitativeEllipticSlice (cubeSet Q) k (A ω)}) (hcover_ae : ∀ᵐ (ω : Ω) ∂μ, ∃ (k : ℕ), AEEQuantitativeEllipticSlice (cubeSet Q) k (A ω)) (P : BlockVec d) : AEMeasurable (fun (ω : Ω) => Mu (cubeSet Q) P (A ω)) μ

Canonical a.e. set-cover AEE cube-slice measurability of Mu.

theorem HCPolySupport.hasMeasurableMuFamily_of_measurable_aeeQuantitativeSlice_sets_canonical_cubeSet {d : ℕ} (Q : TriadicCube d) (hLocal : IsPointwiseLocalSigmaMeasurableOn (fun (a : CoeffField d) => a) (cubeSet Q)) (hSliceMeas : ∀ (k : ℕ), MeasurableSet {a : CoeffField d | AEEQuantitativeEllipticSlice (cubeSet Q) k a}) (hcover : ∀ (a : CoeffField d), ∃ (k : ℕ), AEEQuantitativeEllipticSlice (cubeSet Q) k a) : HasMeasurableMuFamily (cubeSet Q)

Canonical cube-set HasMeasurableMuFamily from an AEE quantitative-slice cover.

theorem HCPolySupport.aemeasurable_Mu_family_of_aeeQuantitativeSlice_sets_canonical_cubeSet {d : ℕ} (Q : TriadicCube d) (μ : MeasureTheory.Measure (CoeffField d)) (hLocal : IsPointwiseLocalSigmaMeasurableOn (fun (a : CoeffField d) => a) (cubeSet Q)) (hSliceMeas : ∀ (k : ℕ), MeasurableSet {a : CoeffField d | AEEQuantitativeEllipticSlice (cubeSet Q) k a}) (hcover_ae : ∀ᵐ (a : CoeffField d) ∂μ, ∃ (k : ℕ), AEEQuantitativeEllipticSlice (cubeSet Q) k a) (P : BlockVec d) : AEMeasurable (fun (a : CoeffField d) => Mu (cubeSet Q) P a) μ

Canonical law-facing a.e. AEE cube-slice Mu family bridge.

theorem HCPolySupport.measurable_Mu_comp_aeeQuantitativeSlice {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} {U : Set (Vec d)} {k : ℕ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hToL2 : Measurable AEEQuantitativeEllipticSlice.toHilbertMatrixL2) (A : Ω → CoeffField d) (hA : IsPointwiseLocalSigmaMeasurableOn A U) (hSlice : ∀ (ω : Ω), AEEQuantitativeEllipticSlice U k (A ω)) (R : MuCorrectionSpaceRecoveryData U) [TopologicalSpace.SeparableSpace ↥R.correctionSpace] (system : (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a) (mu_eq_muCandidate : ∀ (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) (P : BlockVec d), Mu U P ↑a = ((system a).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) : Measurable fun (ω : Ω) => Mu U P (A ω)

theorem HCPolySupport.measurable_Mu_comp_countable_aeeQuantitativeSlice_cover {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hToL2 : ∀ (k : ℕ), Measurable AEEQuantitativeEllipticSlice.toHilbertMatrixL2) (A : Ω → CoeffField d) (hA : IsPointwiseLocalSigmaMeasurableOn A U) (t : ℕ → Set Ω) (ht : ∀ (k : ℕ), MeasurableSet (t k)) (hcover : ⋃ (k : ℕ), t k = Set.univ) (hSlice : ∀ (k : ℕ), ∀ ω ∈ t k, AEEQuantitativeEllipticSlice U k (A ω)) (R : MuCorrectionSpaceRecoveryData U) [TopologicalSpace.SeparableSpace ↥R.correctionSpace] (system : (k : ℕ) → (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a) (mu_eq_muCandidate : ∀ (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) (P : BlockVec d), Mu U P ↑a = ((system k a).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) : Measurable fun (ω : Ω) => Mu U P (A ω)

theorem HCPolySupport.aemeasurable_Mu_comp_countable_aeeQuantitativeSlice_cover {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hToL2 : ∀ (k : ℕ), Measurable AEEQuantitativeEllipticSlice.toHilbertMatrixL2) (A : Ω → CoeffField d) (hA : IsPointwiseLocalSigmaMeasurableOn A U) (t : ℕ → Set Ω) (ht : ∀ (k : ℕ), MeasurableSet (t k)) (hcover_ae : ∀ᵐ (ω : Ω) ∂μ, ω ∈ ⋃ (k : ℕ), t k) (hSlice : ∀ (k : ℕ), ∀ ω ∈ t k, AEEQuantitativeEllipticSlice U k (A ω)) (R : MuCorrectionSpaceRecoveryData U) [TopologicalSpace.SeparableSpace ↥R.correctionSpace] (system : (k : ℕ) → (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a) (mu_eq_muCandidate : ∀ (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) (P : BlockVec d), Mu U P ↑a = ((system k a).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) : AEMeasurable (fun (ω : Ω) => Mu U P (A ω)) μ

theorem HCPolySupport.measurable_Mu_comp_aeeQuantitativeSlice_sets {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hToL2 : ∀ (k : ℕ), Measurable AEEQuantitativeEllipticSlice.toHilbertMatrixL2) (A : Ω → CoeffField d) (hA : IsPointwiseLocalSigmaMeasurableOn A U) (hSliceMeas : ∀ (k : ℕ), MeasurableSet {ω : Ω | AEEQuantitativeEllipticSlice U k (A ω)}) (hcover : ∀ (ω : Ω), ∃ (k : ℕ), AEEQuantitativeEllipticSlice U k (A ω)) (R : MuCorrectionSpaceRecoveryData U) [TopologicalSpace.SeparableSpace ↥R.correctionSpace] (system : (k : ℕ) → (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a) (mu_eq_muCandidate : ∀ (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) (P : BlockVec d), Mu U P ↑a = ((system k a).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) : Measurable fun (ω : Ω) => Mu U P (A ω)

theorem HCPolySupport.aemeasurable_Mu_comp_aeeQuantitativeSlice_sets {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hToL2 : ∀ (k : ℕ), Measurable AEEQuantitativeEllipticSlice.toHilbertMatrixL2) (A : Ω → CoeffField d) (hA : IsPointwiseLocalSigmaMeasurableOn A U) (hSliceMeas : ∀ (k : ℕ), MeasurableSet {ω : Ω | AEEQuantitativeEllipticSlice U k (A ω)}) (hcover_ae : ∀ᵐ (ω : Ω) ∂μ, ∃ (k : ℕ), AEEQuantitativeEllipticSlice U k (A ω)) (R : MuCorrectionSpaceRecoveryData U) [TopologicalSpace.SeparableSpace ↥R.correctionSpace] (system : (k : ℕ) → (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a) (mu_eq_muCandidate : ∀ (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) (P : BlockVec d), Mu U P ↑a = ((system k a).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) : AEMeasurable (fun (ω : Ω) => Mu U P (A ω)) μ

theorem HCPolySupport.aemeasurable_Mu_comp_aeeQuantitativeSlice_sets_of_isOpen_volume_ne_top {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hUopen : IsOpen U) (hUfinite : MeasureTheory.volume U ≠ ⊤) (A : Ω → CoeffField d) (hA : IsPointwiseLocalSigmaMeasurableOn A U) (hSliceMeas : ∀ (k : ℕ), MeasurableSet {ω : Ω | AEEQuantitativeEllipticSlice U k (A ω)}) (hcover_ae : ∀ᵐ (ω : Ω) ∂μ, ∃ (k : ℕ), AEEQuantitativeEllipticSlice U k (A ω)) (R : MuCorrectionSpaceRecoveryData U) [TopologicalSpace.SeparableSpace ↥R.correctionSpace] (system : (k : ℕ) → (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a) (mu_eq_muCandidate : ∀ (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) (P : BlockVec d), Mu U P ↑a = ((system k a).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) : AEMeasurable (fun (ω : Ω) => Mu U P (A ω)) μ

theorem HCPolySupport.hasMeasurableMuFamily_of_measurable_aeeQuantitativeSlice_sets {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hToL2 : ∀ (k : ℕ), Measurable AEEQuantitativeEllipticSlice.toHilbertMatrixL2) (hLocal : IsPointwiseLocalSigmaMeasurableOn (fun (a : CoeffField d) => a) U) (hSliceMeas : ∀ (k : ℕ), MeasurableSet {a : CoeffField d | AEEQuantitativeEllipticSlice U k a}) (hcover : ∀ (a : CoeffField d), ∃ (k : ℕ), AEEQuantitativeEllipticSlice U k a) (R : MuCorrectionSpaceRecoveryData U) [TopologicalSpace.SeparableSpace ↥R.correctionSpace] (system : (k : ℕ) → (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a) (mu_eq_muCandidate : ∀ (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) (P : BlockVec d), Mu U P ↑a = ((system k a).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) : HasMeasurableMuFamily U

Build the ambient HasMeasurableMuFamily U hypothesis from a measurable AEE quantitative-slice cover.

The explicit hLocal hypothesis records that the sampled coefficient field is measurable into the local coefficient-field sigma algebra on U. For the identity map on ambient coefficient fields this is now supplied by the public coefficient-field measurable-space API.

theorem HCPolySupport.hasMeasurableMuFamily_of_measurable_aeeQuantitativeSlice_sets_of_isOpen_volume_ne_top {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hUopen : IsOpen U) (hUfinite : MeasureTheory.volume U ≠ ⊤) (hLocal : IsPointwiseLocalSigmaMeasurableOn (fun (a : CoeffField d) => a) U) (hSliceMeas : ∀ (k : ℕ), MeasurableSet {a : CoeffField d | AEEQuantitativeEllipticSlice U k a}) (hcover : ∀ (a : CoeffField d), ∃ (k : ℕ), AEEQuantitativeEllipticSlice U k a) (R : MuCorrectionSpaceRecoveryData U) [TopologicalSpace.SeparableSpace ↥R.correctionSpace] (system : (k : ℕ) → (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a) (mu_eq_muCandidate : ∀ (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) (P : BlockVec d), Mu U P ↑a = ((system k a).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) : HasMeasurableMuFamily U

Open finite-volume version of hasMeasurableMuFamily_of_measurable_aeeQuantitativeSlice_sets, with the smooth-probe Hilbert L² measurability supplied internally.

theorem HCPolySupport.aemeasurable_Mu_family_of_aeeQuantitativeSlice_sets {d : ℕ} {U : Set (Vec d)} (μ : MeasureTheory.Measure (CoeffField d)) [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hToL2 : ∀ (k : ℕ), Measurable AEEQuantitativeEllipticSlice.toHilbertMatrixL2) (hLocal : IsPointwiseLocalSigmaMeasurableOn (fun (a : CoeffField d) => a) U) (hSliceMeas : ∀ (k : ℕ), MeasurableSet {a : CoeffField d | AEEQuantitativeEllipticSlice U k a}) (hcover_ae : ∀ᵐ (a : CoeffField d) ∂μ, ∃ (k : ℕ), AEEQuantitativeEllipticSlice U k a) (R : MuCorrectionSpaceRecoveryData U) [TopologicalSpace.SeparableSpace ↥R.correctionSpace] (system : (k : ℕ) → (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a) (mu_eq_muCandidate : ∀ (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) (P : BlockVec d), Mu U P ↑a = ((system k a).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) : AEMeasurable (fun (a : CoeffField d) => Mu U P a) μ

Law-facing a.e. version of the AEE-slice Mu family bridge. This is the form naturally produced by a random law whose fields are only known to be locally uniformly elliptic almost surely.

theorem HCPolySupport.aemeasurable_Mu_family_of_aeeQuantitativeSlice_sets_of_isOpen_volume_ne_top {d : ℕ} {U : Set (Vec d)} (μ : MeasureTheory.Measure (CoeffField d)) [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hUopen : IsOpen U) (hUfinite : MeasureTheory.volume U ≠ ⊤) (hLocal : IsPointwiseLocalSigmaMeasurableOn (fun (a : CoeffField d) => a) U) (hSliceMeas : ∀ (k : ℕ), MeasurableSet {a : CoeffField d | AEEQuantitativeEllipticSlice U k a}) (hcover_ae : ∀ᵐ (a : CoeffField d) ∂μ, ∃ (k : ℕ), AEEQuantitativeEllipticSlice U k a) (R : MuCorrectionSpaceRecoveryData U) [TopologicalSpace.SeparableSpace ↥R.correctionSpace] (system : (k : ℕ) → (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a) (mu_eq_muCandidate : ∀ (k : ℕ) (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) (P : BlockVec d), Mu U P ↑a = ((system k a).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P) (P : BlockVec d) : AEMeasurable (fun (a : CoeffField d) => Mu U P a) μ

Open finite-volume version of the law-facing a.e. AEE-slice Mu family bridge.