Coarse-graining support:

Support.Book.Ch04.Internal.FixedCompetitorEnergyMeasurability.BlockEnergyAverage

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: block-energy-average measurability under quantitative elliptic slices — combines Integrals.lean with the subtype-measurability of locally σ-measurable coefficient fields landing in a single slice to produce measurable block-energy-average observables of the form needed by the Mu-candidate construction.

Consumed by (within Internal/FixedCompetitorEnergyMeasurability/): MuObservable.lean. Upstream chain continues to Theorems/Mu.lean :: aemeasurable_Mu_cubeSet.

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

theorem HCPolySupport.measurable_subtype_mk_quantitativeSlice_of_isLocalSigmaMeasurableOn {Ω : Type u_1} [MeasurableSpace Ω] {d : ℕ} {U : Set (Vec d)} {k : ℕ} (A : Ω → CoeffField d) (hA : IsPointwiseLocalSigmaMeasurableOn A U) (hSlice : ∀ (ω : Ω), QuantitativeEllipticSlice U k (A ω)) : Measurable fun (ω : Ω) => ⟨A ω, ⋯⟩

A locally measurable sample-space coefficient field that lands in one quantitative slice is measurable as a map into that slice subtype.

theorem HCPolySupport.measurable_blockEnergyAverage_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 ω)) (X : BlockState d) (hX : MemBlockL2 U X.eval) : Measurable fun (ω : Ω) => blockEnergyAverage U (A ω) X

Composition form of fixed-competitor energy measurability on a single quantitative slice for sample-space-valued coefficient fields.

theorem HCPolySupport.measurable_blockEnergyAverage_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 ω)) (X : BlockState d) (hX : MemBlockL2 U X.eval) : Measurable fun (ω : Ω) => blockEnergyAverage U (A ω) X

Open finite-measure wrapper for the fixed-slice composition theorem for fixed-competitor energies.

theorem HCPolySupport.measurable_blockEnergyAverage_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 ω)) (X : BlockState d) (hX : MemBlockL2 U X.eval) : Measurable fun (ω : Ω) => blockEnergyAverage U (A ω) X

Countable-slice assembly for fixed-competitor energy averages. If a sample-space coefficient field lands on the k-th quantitative ellipticity slice on the measurable piece t k, and the pieces cover the whole sample space, then the energy observable is measurable.

theorem HCPolySupport.aemeasurable_blockEnergyAverage_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 ω)) (X : BlockState d) (hX : MemBlockL2 U X.eval) : AEMeasurable (fun (ω : Ω) => blockEnergyAverage U (A ω) X) μ

Almost-everywhere countable-slice assembly for fixed-competitor energy averages. This is the AE version used after local ellipticity supplies an almost-sure countable quantitative-slice cover.

theorem HCPolySupport.measurable_blockEnergyAverage_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 ω)) (X : BlockState d) (hX : MemBlockL2 U X.eval) : Measurable fun (ω : Ω) => blockEnergyAverage U (A ω) X

If the raw quantitative-slice membership sets are measurable and cover the sample space, then the countable-slice fixed-energy assembly theorem applies directly to those sets.

theorem HCPolySupport.aemeasurable_blockEnergyAverage_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 ω)) (X : BlockState d) (hX : MemBlockL2 U X.eval) : AEMeasurable (fun (ω : Ω) => blockEnergyAverage U (A ω) X) μ

AE version of measurable_blockEnergyAverage_comp_quantitativeSlice_sets. This is the immediate handoff from an almost-sure countable slice-existence statement, provided the raw slice-membership sets are measurable.

theorem HCPolySupport.aemeasurable_blockEnergyAverage_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 ω)) (X : BlockState d) (hX : MemBlockL2 U X.eval) : AEMeasurable (fun (ω : Ω) => blockEnergyAverage U (A ω) X) μ

Open finite-measure wrapper for the AE fixed-energy slice-set assembly theorem.

theorem HCPolySupport.aemeasurable_blockEnergyAverage_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 ω)}) (X : BlockState d) (hX : MemBlockL2 (openCubeSet (originCube d n)) X.eval) : AEMeasurable (fun (ω : Ω) => blockEnergyAverage (openCubeSet (originCube d n)) (A ω) X) μ

Origin-open-cube handoff from almost-sure local uniform ellipticity to fixed-energy AEMeasurable, conditional on measurability of the raw quantitative-slice membership sets.

theorem HCPolySupport.blockEnergyAverage_restrictCoeffField_eq {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (a : CoeffField d) (X : BlockState d) : blockEnergyAverage U (restrictCoeffField U a) X = blockEnergyAverage U a X

theorem HCPolySupport.blockEnergyAverage_eq_of_forall_mem_eq {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) {a₁ a₂ : CoeffField d} (X : BlockState d) (hEq : ∀ x ∈ U, a₁ x = a₂ x) : blockEnergyAverage U a₁ X = blockEnergyAverage U a₂ X

theorem HCPolySupport.isLocalObservable_blockEnergyAverage {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (X : BlockState d) : IsRestrictionLocalObservable U fun (a : CoeffField d) => blockEnergyAverage U a X

theorem HCPolySupport.measurable_blockEnergyAverage_restrictionSigma_of_measurable {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (X : BlockState d) (hX : Measurable fun (a : CoeffField d) => blockEnergyAverage U a X) : Measurable fun (a : CoeffField d) => blockEnergyAverage U a X

noncomputable def HCPolySupport.blockEnergyAverageLocalObservableOfMeasurable {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (X : BlockState d) (hX : Measurable fun (a : CoeffField d) => blockEnergyAverage U a X) : MeasurableRestrictionLocalObservable d U ℝ

The block energy average for a fixed state, bundled as a measurable observable local to U.

Equations

• One or more equations did not get rendered due to their size.