Coarse-graining support: #
Support.Book.Ch04.Internal.FixedCompetitorEnergyMeasurability.MuObservable
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 candidate viewed as a
functional of the coefficient field, composed through the measurable
block-energy-average machinery of BlockEnergyAverage.lean. This is the
top of the FixedCompetitorEnergyMeasurability/ chain — every preceding
file in this directory feeds into the proofs here.
Consumed by: the umbrella module
FixedCompetitorEnergyMeasurability.lean, then
Internal/AEESliceAssembly/{BlockEnergyAverage, MuFamily}.lean, then
Theorems/Mu.lean :: aemeasurable_Mu_cubeSet (and the AEE-slice variant
aemeasurable_Mu_cubeSet_of_measurable_aeeQuantitativeSlice).
If the single-claim summary above grows into three or more distinct claims, split or refactor per the rebuild contract.
theorem
HCPolySupport.measurable_Mu_comp_of_measurable_blockEnergyAverage_affineField_denseSeq
{Ω : Type u_1}
[MeasurableSpace Ω]
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(A : Ω → CoeffField d)
(R : MuCorrectionSpaceRecoveryData U)
[TopologicalSpace.SeparableSpace ↥R.correctionSpace]
(system : (ω : Ω) → MuOperatorSystemData U (A ω))
(mu_eq_muCandidate :
∀ (ω : Ω) (P : BlockVec d),
Mu U P (A ω) = ((system ω).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P)
(P : BlockVec d)
(hMeas :
∀ (n : ℕ),
Measurable fun (ω : Ω) =>
blockEnergyAverage U (A ω) (R.affineField P (TopologicalSpace.denseSeq (↥R.correctionSpace) n)))
:
Measurable fun (ω : Ω) => Mu U P (A ω)
theorem
HCPolySupport.measurable_Mu_of_measurable_blockEnergyAverage_affineField_denseSeq
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(R : MuCorrectionSpaceRecoveryData U)
[TopologicalSpace.SeparableSpace ↥R.correctionSpace]
(system : (a : CoeffField d) → MuOperatorSystemData U a)
(mu_eq_muCandidate :
∀ (a : CoeffField d) (P : BlockVec d),
Mu U P a = ((system a).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P)
(P : BlockVec d)
(hMeas :
∀ (n : ℕ),
Measurable fun (a : CoeffField d) =>
blockEnergyAverage U a (R.affineField P (TopologicalSpace.denseSeq (↥R.correctionSpace) n)))
:
Measurable fun (a : CoeffField d) => Mu U P a
theorem
HCPolySupport.measurable_Mu_of_measurable_weightedFullBlockCoeffEntryIntegrals_denseSeq
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(R : MuCorrectionSpaceRecoveryData U)
[TopologicalSpace.SeparableSpace ↥R.correctionSpace]
(system : (a : CoeffField d) → MuOperatorSystemData U a)
(mu_eq_muCandidate :
∀ (a : CoeffField d) (P : BlockVec d),
Mu U P a = ((system a).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P)
(P : BlockVec d)
(hInt :
∀ (a : CoeffField d) (n : ℕ) (α β : BlockCoord d),
MeasureTheory.IntegrableOn
(fun (x : Vec d) =>
blockEnergyEntryWeight (R.affineField P (TopologicalSpace.denseSeq (↥R.correctionSpace) n)) α β x * toFullBlockMat (blockCoeffField a x) α β)
U MeasureTheory.volume)
(hMeas :
∀ (n : ℕ) (α β : BlockCoord d),
Measurable fun (a : CoeffField d) =>
∫ (x : Vec d) in U, blockEnergyEntryWeight (R.affineField P (TopologicalSpace.denseSeq (↥R.correctionSpace) n)) α β x * toFullBlockMat (blockCoeffField a x) α β)
:
Measurable fun (a : CoeffField d) => Mu U P a
theorem
HCPolySupport.measurable_Mu_comp_of_measurable_weightedFullBlockCoeffEntryIntegrals_denseSeq
{Ω : Type u_1}
[MeasurableSpace Ω]
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(A : Ω → CoeffField d)
(R : MuCorrectionSpaceRecoveryData U)
[TopologicalSpace.SeparableSpace ↥R.correctionSpace]
(system : (ω : Ω) → MuOperatorSystemData U (A ω))
(mu_eq_muCandidate :
∀ (ω : Ω) (P : BlockVec d),
Mu U P (A ω) = ((system ω).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P)
(P : BlockVec d)
(hInt :
∀ (ω : Ω) (n : ℕ) (α β : BlockCoord d),
MeasureTheory.IntegrableOn
(fun (x : Vec d) =>
blockEnergyEntryWeight (R.affineField P (TopologicalSpace.denseSeq (↥R.correctionSpace) n)) α β x * toFullBlockMat (blockCoeffField (A ω) x) α β)
U MeasureTheory.volume)
(hMeas :
∀ (n : ℕ) (α β : BlockCoord d),
Measurable fun (ω : Ω) =>
∫ (x : Vec d) in U, blockEnergyEntryWeight (R.affineField P (TopologicalSpace.denseSeq (↥R.correctionSpace) n)) α β x * toFullBlockMat (blockCoeffField (A ω) x) α β)
:
Measurable fun (ω : Ω) => Mu U P (A ω)
theorem
HCPolySupport.measurable_Mu_quantitativeSlice_of_measurable_weightedFullBlockCoeffEntryIntegrals_denseSeq
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(R : MuCorrectionSpaceRecoveryData U)
[TopologicalSpace.SeparableSpace ↥R.correctionSpace]
(system : (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a)
(mu_eq_muCandidate :
∀ (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) (P : BlockVec d),
Mu U P ↑a = ((system a).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P)
(P : BlockVec d)
(hMeas :
∀ (n : ℕ) (α β : BlockCoord d),
Measurable fun (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, blockEnergyEntryWeight (R.affineField P (TopologicalSpace.denseSeq (↥R.correctionSpace) n)) α β x * toFullBlockMat (blockCoeffField (↑a) x) α β)
:
Measurable fun (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) => Mu U P ↑a
theorem
HCPolySupport.measurable_Mu_quantitativeSlice
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hToL2 : Measurable QuantitativeEllipticSlice.toHilbertMatrixL2)
(R : MuCorrectionSpaceRecoveryData U)
[TopologicalSpace.SeparableSpace ↥R.correctionSpace]
(system : (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a)
(mu_eq_muCandidate :
∀ (a : { a : CoeffField d // QuantitativeEllipticSlice 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 // QuantitativeEllipticSlice U k a }) => Mu U P ↑a
Note-facing quantitative-slice measurability of Mu: once the slice has
the measurable L² coefficient realization, fixed competitors are measurable
by the L¹ entry theorem and Mu follows from the dense iInf formula.
theorem
HCPolySupport.measurable_blockEnergyAverage_quantitativeSlice_of_isOpen_volume_ne_top
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hUopen : IsOpen U)
(hUfinite : MeasureTheory.volume U ≠ ⊤)
(X : BlockState d)
(hX : MemBlockL2 U X.eval)
:
Measurable fun (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) => blockEnergyAverage U (↑a) X
Open finite-measure wrapper for fixed-competitor energy measurability on a quantitative elliptic slice.
theorem
HCPolySupport.measurable_Mu_quantitativeSlice_of_isOpen_volume_ne_top
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hUopen : IsOpen U)
(hUfinite : MeasureTheory.volume U ≠ ⊤)
(R : MuCorrectionSpaceRecoveryData U)
[TopologicalSpace.SeparableSpace ↥R.correctionSpace]
(system : (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a)
(mu_eq_muCandidate :
∀ (a : { a : CoeffField d // QuantitativeEllipticSlice 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 // QuantitativeEllipticSlice U k a }) => Mu U P ↑a
Open finite-measure wrapper for note-facing quantitative-slice
measurability of Mu.
theorem
HCPolySupport.measurable_Mu_comp_quantitativeSlice
{Ω : Type u_1}
[MeasurableSpace Ω]
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hToL2 : Measurable QuantitativeEllipticSlice.toHilbertMatrixL2)
(A : Ω → CoeffField d)
(hA : IsPointwiseLocalSigmaMeasurableOn A U)
(hSlice : ∀ (ω : Ω), QuantitativeEllipticSlice U k (A ω))
(R : MuCorrectionSpaceRecoveryData U)
[TopologicalSpace.SeparableSpace ↥R.correctionSpace]
(system : (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a)
(mu_eq_muCandidate :
∀ (a : { a : CoeffField d // QuantitativeEllipticSlice 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 ω)
Composition form of quantitative-slice Mu measurability for
sample-space-valued coefficient fields landing in one slice.
theorem
HCPolySupport.measurable_Mu_comp_quantitativeSlice_of_isOpen_volume_ne_top
{Ω : Type u_1}
[MeasurableSpace Ω]
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hUopen : IsOpen U)
(hUfinite : MeasureTheory.volume U ≠ ⊤)
(A : Ω → CoeffField d)
(hA : IsPointwiseLocalSigmaMeasurableOn A U)
(hSlice : ∀ (ω : Ω), QuantitativeEllipticSlice U k (A ω))
(R : MuCorrectionSpaceRecoveryData U)
[TopologicalSpace.SeparableSpace ↥R.correctionSpace]
(system : (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a)
(mu_eq_muCandidate :
∀ (a : { a : CoeffField d // QuantitativeEllipticSlice 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 ω)
Open finite-measure wrapper for the fixed-slice composition theorem for
Mu.
theorem
HCPolySupport.measurable_Mu_comp_countable_quantitativeSlice_cover
{Ω : Type u_1}
[MeasurableSpace Ω]
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hToL2 : ∀ (k : ℕ), Measurable QuantitativeEllipticSlice.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, QuantitativeEllipticSlice U k (A ω))
(R : MuCorrectionSpaceRecoveryData U)
[TopologicalSpace.SeparableSpace ↥R.correctionSpace]
(system : (k : ℕ) → (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a)
(mu_eq_muCandidate :
∀ (k : ℕ) (a : { a : CoeffField d // QuantitativeEllipticSlice 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 ω)
Countable-slice assembly for Mu. On each measurable piece t k, the
sample-space coefficient field is only required to land in the corresponding
quantitative ellipticity slice; the countable cover is glued by
Set.liftCover.
theorem
HCPolySupport.aemeasurable_Mu_comp_countable_quantitativeSlice_cover
{Ω : Type u_1}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hToL2 : ∀ (k : ℕ), Measurable QuantitativeEllipticSlice.toHilbertMatrixL2)
(A : Ω → CoeffField d)
(hA : IsPointwiseLocalSigmaMeasurableOn A U)
(t : ℕ → Set Ω)
(ht : ∀ (k : ℕ), MeasurableSet (t k))
(hcover_ae : ∀ᵐ (ω : Ω) ∂μ, ω ∈ ⋃ (k : ℕ), t k)
(hSlice : ∀ (k : ℕ), ∀ ω ∈ t k, QuantitativeEllipticSlice U k (A ω))
(R : MuCorrectionSpaceRecoveryData U)
[TopologicalSpace.SeparableSpace ↥R.correctionSpace]
(system : (k : ℕ) → (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a)
(mu_eq_muCandidate :
∀ (k : ℕ) (a : { a : CoeffField d // QuantitativeEllipticSlice 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 ω)) μ
Almost-everywhere countable-slice assembly for Mu. The theorem adds a
measurable null fallback piece to an AE countable cover and then glues the
slice-wise measurable realizations.
theorem
HCPolySupport.measurable_Mu_comp_quantitativeSlice_sets
{Ω : Type u_1}
[MeasurableSpace Ω]
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hToL2 : ∀ (k : ℕ), Measurable QuantitativeEllipticSlice.toHilbertMatrixL2)
(A : Ω → CoeffField d)
(hA : IsPointwiseLocalSigmaMeasurableOn A U)
(hSliceMeas : ∀ (k : ℕ), MeasurableSet {ω : Ω | QuantitativeEllipticSlice U k (A ω)})
(hcover : ∀ (ω : Ω), ∃ (k : ℕ), QuantitativeEllipticSlice U k (A ω))
(R : MuCorrectionSpaceRecoveryData U)
[TopologicalSpace.SeparableSpace ↥R.correctionSpace]
(system : (k : ℕ) → (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a)
(mu_eq_muCandidate :
∀ (k : ℕ) (a : { a : CoeffField d // QuantitativeEllipticSlice 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 ω)
If the raw quantitative-slice membership sets are measurable and cover the
sample space, then the countable-slice Mu assembly theorem applies directly
to those sets.
theorem
HCPolySupport.aemeasurable_Mu_comp_quantitativeSlice_sets
{Ω : Type u_1}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hToL2 : ∀ (k : ℕ), Measurable QuantitativeEllipticSlice.toHilbertMatrixL2)
(A : Ω → CoeffField d)
(hA : IsPointwiseLocalSigmaMeasurableOn A U)
(hSliceMeas : ∀ (k : ℕ), MeasurableSet {ω : Ω | QuantitativeEllipticSlice U k (A ω)})
(hcover_ae : ∀ᵐ (ω : Ω) ∂μ, ∃ (k : ℕ), QuantitativeEllipticSlice U k (A ω))
(R : MuCorrectionSpaceRecoveryData U)
[TopologicalSpace.SeparableSpace ↥R.correctionSpace]
(system : (k : ℕ) → (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a)
(mu_eq_muCandidate :
∀ (k : ℕ) (a : { a : CoeffField d // QuantitativeEllipticSlice 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 ω)) μ
AE version of measurable_Mu_comp_quantitativeSlice_sets. This is the
selection/assembly handoff from almost-sure slice existence, conditional on
measurability of the raw slice-membership sets.
theorem
HCPolySupport.aemeasurable_Mu_comp_quantitativeSlice_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 {ω : Ω | QuantitativeEllipticSlice U k (A ω)})
(hcover_ae : ∀ᵐ (ω : Ω) ∂μ, ∃ (k : ℕ), QuantitativeEllipticSlice U k (A ω))
(R : MuCorrectionSpaceRecoveryData U)
[TopologicalSpace.SeparableSpace ↥R.correctionSpace]
(system : (k : ℕ) → (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) → MuOperatorSystemData U ↑a)
(mu_eq_muCandidate :
∀ (k : ℕ) (a : { a : CoeffField d // QuantitativeEllipticSlice 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 ω)) μ
Open finite-measure wrapper for the AE Mu slice-set assembly theorem.
theorem
HCPolySupport.aemeasurable_Mu_comp_openCubeSet_originCube_of_ae_locallyUniformlyElliptic
{Ω : Type u_1}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
{d : ℕ}
(n : ℤ)
(A : Ω → CoeffField d)
(hA : IsPointwiseLocalSigmaMeasurableOn A (openCubeSet (originCube d n)))
(hloc : ∀ᵐ (ω : Ω) ∂μ, IsLocallyUniformlyElliptic (A ω))
(hSliceMeas : ∀ (k : ℕ), MeasurableSet {ω : Ω | QuantitativeEllipticSlice (openCubeSet (originCube d n)) k (A ω)})
(R : MuCorrectionSpaceRecoveryData (openCubeSet (originCube d n)))
[TopologicalSpace.SeparableSpace ↥R.correctionSpace]
(system :
(k : ℕ) →
(a : { a : CoeffField d // QuantitativeEllipticSlice (openCubeSet (originCube d n)) k a }) →
MuOperatorSystemData (openCubeSet (originCube d n)) ↑a)
(mu_eq_muCandidate :
∀ (k : ℕ) (a : { a : CoeffField d // QuantitativeEllipticSlice (openCubeSet (originCube d n)) k a }) (P : BlockVec d),
Mu (openCubeSet (originCube d n)) P ↑a = ((system k a).toMuOperatorRealization.toMuHilbertRealization R.toMuCorrectionSpaceData).muCandidate P)
(P : BlockVec d)
:
AEMeasurable (fun (ω : Ω) => Mu (openCubeSet (originCube d n)) P (A ω)) μ
Origin-open-cube handoff from almost-sure local uniform ellipticity to
Mu AEMeasurable, conditional on measurability of the raw quantitative-slice
membership sets.