Coarse-graining support: #
Support.Book.Ch04.Internal.FixedCompetitorEnergyMeasurability.Measurability
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Fixed-competitor energy measurability, first atoms #
Audit tag (Ch4 rebuild contract CH04_REBUILD_SURFACE_2026-05-16.md) #
Internal claim: the PointwiseLocalSigma-measurable scalar atoms (single-vector
dot products, single-coordinate matrix-vector products, etc.) used as the
local-σ-measurable building blocks for fixed-competitor energy observables.
First layer of the internal HasMeasurableMuFamily cleanup.
Consumed by (within Internal/FixedCompetitorEnergyMeasurability/):
LipschitzBounds.lean, which lifts these atoms to Borel-measurable
fixed-coefficient maps; ultimately reaches the public
Theorems/Mu.lean :: aemeasurable_Mu_cubeSet via the chain
Measurability → LipschitzBounds → Integrals → BlockEnergyAverage → MuObservable → AEESliceAssembly/MuFamily.
If the single-claim summary above grows into three or more distinct claims, split or refactor per the rebuild contract.
theorem
HCPolySupport.localTestObservable_single_single_eq_integral_entry
{d : ℕ}
(i j : Fin d)
(φ : Vec d → ℝ)
:
localTestObservable (Pi.single j 1) (Pi.single i 1) φ = fun (a : CoeffField d) => ∫ (x : Vec d), a x i j * φ x
theorem
HCPolySupport.measurable_entryTestObservable_localSigma
{d : ℕ}
{U : Set (Vec d)}
(i j : Fin d)
{φ : Vec d → ℝ}
(hφ_cont : ContDiff ℝ (↑⊤) φ)
(hφ_compact : HasCompactSupport φ)
(hφ_support : tsupport φ ⊆ U)
:
Measurable fun (a : CoeffField d) => ∫ (x : Vec d), a x i j * φ x
theorem
HCPolySupport.measurable_entryTestObservable_setIntegral_localSigma
{d : ℕ}
{U : Set (Vec d)}
(i j : Fin d)
{φ : Vec d → ℝ}
(hφ_cont : ContDiff ℝ (↑⊤) φ)
(hφ_compact : HasCompactSupport φ)
(hφ_support : tsupport φ ⊆ U)
:
Measurable fun (a : CoeffField d) => ∫ (x : Vec d) in U, a x i j * φ x
theorem
HCPolySupport.measurable_inner_toScalarL2_matrixL2Entry_toMatrixL2_localMeasurableSpace
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(i j : Fin d)
{φ : Vec d → ℝ}
(hφL2 : MemScalarL2 U φ)
(hφ_cont : ContDiff ℝ (↑⊤) φ)
(hφ_compact : HasCompactSupport φ)
(hφ_support : tsupport φ ⊆ U)
:
Measurable fun (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) =>
inner ℝ (toScalarL2 hφL2) ((QuantitativeEllipticSlice.matrixL2Entry i j) (QuantitativeEllipticSlice.toMatrixL2 a))
theorem
HCPolySupport.measurable_inner_toScalarL2_hilbertMatrixL2Entry_toHilbertMatrixL2_localMeasurableSpace
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(i j : Fin d)
{φ : Vec d → ℝ}
(hφL2 : MemScalarL2 U φ)
(hφ_cont : ContDiff ℝ (↑⊤) φ)
(hφ_compact : HasCompactSupport φ)
(hφ_support : tsupport φ ⊆ U)
:
Measurable fun (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) =>
inner ℝ (toScalarL2 hφL2)
((QuantitativeEllipticSlice.hilbertMatrixL2Entry i j) (QuantitativeEllipticSlice.toHilbertMatrixL2 a))
theorem
HCPolySupport.measurable_inner_hilbertMatrixSmoothProbe_toHilbertMatrixL2_localMeasurableSpace
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{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 (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) =>
inner ℝ (MeasureTheory.MemLp.toLp g hgL2) (QuantitativeEllipticSlice.toHilbertMatrixL2 a)
theorem
HCPolySupport.measurable_toHilbertMatrixL2_of_dense_smoothProbeSequence
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(u : ℕ → ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U)))
(hu : DenseRange u)
(hSmooth :
∀ (n : ℕ),
∃ (g : Vec d → HilbertMat d) (hgL2 : MeasureTheory.MemLp g 2 (volumeMeasureOn U)),
u n = MeasureTheory.MemLp.toLp g hgL2 ∧ ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g ∧ tsupport g ⊆ U)
:
theorem
HCPolySupport.dense_smoothCompactHilbertMatrixL2
{d : ℕ}
{U : Set (Vec d)}
:
Dense
{f : ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U)) | ∃ (g : Vec d → HilbertMat d) (hgL2 : MeasureTheory.MemLp g 2 (volumeMeasureOn U)),
f = MeasureTheory.MemLp.toLp g hgL2 ∧ ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g}
Mathlib's global smooth compact-support density, converted to the exact toLp
representative shape used by the probability bookkeeping.
The later local argument still has to push these probes inside U; this lemma isolates the
ambient density input from that boundary-cutoff step.
theorem
HCPolySupport.exists_contDiff_hilbertMatrixL2_tsupport_subset_eLpNorm_sub_le
{d : ℕ}
{U : Set (Vec d)}
(hUopen : IsOpen U)
(hUfinite : MeasureTheory.volume U ≠ ⊤)
{g : Vec d → HilbertMat d}
(hgL2 : MeasureTheory.MemLp g 2 (volumeMeasureOn U))
(hg_cont : ContDiff ℝ (↑⊤) g)
{ε : ℝ}
(hε : 0 < ε)
:
∃ (φ : Vec d → HilbertMat d) (_ : MeasureTheory.MemLp φ 2 (volumeMeasureOn U)),
MeasureTheory.eLpNorm (g - φ) 2 (volumeMeasureOn U) ≤ ENNReal.ofReal ε ∧ ContDiff ℝ (↑⊤) φ ∧ HasCompactSupport φ ∧ tsupport φ ⊆ U
Localize a smooth L² matrix field to an open finite-measure set without
changing it much in L². This is the analytic cutoff step that turns
Mathlib's ambient compactly supported smooth density into the note-facing
tsupport ⊆ U probe class.
theorem
HCPolySupport.dense_smoothCompactSupportHilbertMatrixL2_tsupport_subset
{d : ℕ}
{U : Set (Vec d)}
(hUopen : IsOpen U)
(hUfinite : MeasureTheory.volume U ≠ ⊤)
:
Dense
{f : ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U)) | ∃ (g : Vec d → HilbertMat d) (hgL2 : MeasureTheory.MemLp g 2 (volumeMeasureOn U)),
f = MeasureTheory.MemLp.toLp g hgL2 ∧ ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g ∧ tsupport g ⊆ U}
Smooth compactly supported HilbertMat probes with support contained in an
open finite-measure set are dense in L²(U; HilbertMat d).
theorem
HCPolySupport.exists_dense_smoothProbeSequence_of_dense_smoothProbeSet
{d : ℕ}
{U : Set (Vec d)}
(hDense :
Dense
{f : ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U)) | ∃ (g : Vec d → HilbertMat d) (hgL2 : MeasureTheory.MemLp g 2 (volumeMeasureOn U)),
f = MeasureTheory.MemLp.toLp g hgL2 ∧ ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g ∧ tsupport g ⊆ U})
:
∃ (u : ℕ → ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U))),
DenseRange u ∧ ∀ (n : ℕ),
∃ (g : Vec d → HilbertMat d) (hgL2 : MeasureTheory.MemLp g 2 (volumeMeasureOn U)),
u n = MeasureTheory.MemLp.toLp g hgL2 ∧ ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g ∧ tsupport g ⊆ U
theorem
HCPolySupport.measurable_toHilbertMatrixL2_of_dense_smoothProbeSet
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hDense :
Dense
{f : ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U)) | ∃ (g : Vec d → HilbertMat d) (hgL2 : MeasureTheory.MemLp g 2 (volumeMeasureOn U)),
f = MeasureTheory.MemLp.toLp g hgL2 ∧ ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g ∧ tsupport g ⊆ U})
:
theorem
HCPolySupport.measurable_toHilbertMatrixL2_of_isOpen_volume_ne_top
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hUopen : IsOpen U)
(hUfinite : MeasureTheory.volume U ≠ ⊤)
:
On an open finite-measure domain, the quantitative-slice coefficient field
as an L² Hilbert-matrix object is measurable for the local sigma algebra.
theorem
HCPolySupport.measurable_inner_toScalarL2_hilbertMatrixL2Entry_toHilbertMatrixL2_essentialLocalMeasurableSpace
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(i j : Fin d)
{φ : Vec d → ℝ}
(hφL2 : MemScalarL2 U φ)
(hφ_cont : ContDiff ℝ (↑⊤) φ)
(hφ_compact : HasCompactSupport φ)
(hφ_support : tsupport φ ⊆ U)
:
Measurable fun (a : { a : CoeffField d // EssentialQuantitativeEllipticSlice U k a }) =>
inner ℝ (toScalarL2 hφL2)
((QuantitativeEllipticSlice.hilbertMatrixL2Entry i j) (EssentialQuantitativeEllipticSlice.toHilbertMatrixL2 a))
theorem
HCPolySupport.measurable_inner_hilbertMatrixSmoothProbe_toHilbertMatrixL2_essentialLocalMeasurableSpace
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{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 (a : { a : CoeffField d // EssentialQuantitativeEllipticSlice U k a }) =>
inner ℝ (MeasureTheory.MemLp.toLp g hgL2) (EssentialQuantitativeEllipticSlice.toHilbertMatrixL2 a)
theorem
HCPolySupport.measurable_toHilbertMatrixL2_essential_of_dense_smoothProbeSequence
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(u : ℕ → ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U)))
(hu : DenseRange u)
(hSmooth :
∀ (n : ℕ),
∃ (g : Vec d → HilbertMat d) (hgL2 : MeasureTheory.MemLp g 2 (volumeMeasureOn U)),
u n = MeasureTheory.MemLp.toLp g hgL2 ∧ ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g ∧ tsupport g ⊆ U)
:
theorem
HCPolySupport.measurable_toHilbertMatrixL2_essential_of_dense_smoothProbeSet
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hDense :
Dense
{f : ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U)) | ∃ (g : Vec d → HilbertMat d) (hgL2 : MeasureTheory.MemLp g 2 (volumeMeasureOn U)),
f = MeasureTheory.MemLp.toLp g hgL2 ∧ ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g ∧ tsupport g ⊆ U})
:
theorem
HCPolySupport.measurable_toHilbertMatrixL2_essential_of_isOpen_volume_ne_top
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hUopen : IsOpen U)
(hUfinite : MeasureTheory.volume U ≠ ⊤)
:
On an open finite-measure domain, the essential quantitative-slice
coefficient field as an L² Hilbert-matrix object is measurable for the local
sigma algebra.
theorem
HCPolySupport.dense_smoothCompactSupportHilbertMatrixL2_tsupport_subset_cubeSet
{d : ℕ}
(Q : TriadicCube d)
:
Dense
{f : ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn (cubeSet Q))) | ∃ (g : Vec d → HilbertMat d) (hgL2 : MeasureTheory.MemLp g 2 (volumeMeasureOn (cubeSet Q))),
f = MeasureTheory.MemLp.toLp g hgL2 ∧ ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g ∧ tsupport g ⊆ cubeSet Q}
Smooth probes supported in the open core of a triadic cube are dense for the half-open cube, because the two restricted volume measures agree.
theorem
HCPolySupport.measurable_toHilbertMatrixL2_essentialQuantitativeEllipticSlice_cubeSet
{d : ℕ}
(Q : TriadicCube d)
(k : ℕ)
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet Q))]
:
On a half-open triadic cube, the essential quantitative-slice coefficient
field as an L² Hilbert-matrix object is measurable for the local sigma
algebra.
theorem
HCPolySupport.measurable_inner_toScalarL2_hilbertMatrixL2Entry_toHilbertMatrixL2_aeeLocalMeasurableSpace
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(i j : Fin d)
{φ : Vec d → ℝ}
(hφL2 : MemScalarL2 U φ)
(hφ_cont : ContDiff ℝ (↑⊤) φ)
(hφ_compact : HasCompactSupport φ)
(hφ_support : tsupport φ ⊆ U)
:
Measurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) =>
inner ℝ (toScalarL2 hφL2)
((QuantitativeEllipticSlice.hilbertMatrixL2Entry i j) (AEEQuantitativeEllipticSlice.toHilbertMatrixL2 a))
Smooth-probe coordinate pairings of the AEE L² coefficient realization
are local-test measurable.
theorem
HCPolySupport.measurable_inner_hilbertMatrixSmoothProbe_toHilbertMatrixL2_aeeLocalMeasurableSpace
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{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 (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) =>
inner ℝ (MeasureTheory.MemLp.toLp g hgL2) (AEEQuantitativeEllipticSlice.toHilbertMatrixL2 a)
theorem
HCPolySupport.measurable_toHilbertMatrixL2_aee_of_dense_smoothProbeSequence
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(u : ℕ → ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U)))
(hu : DenseRange u)
(hSmooth :
∀ (n : ℕ),
∃ (g : Vec d → HilbertMat d) (hgL2 : MeasureTheory.MemLp g 2 (volumeMeasureOn U)),
u n = MeasureTheory.MemLp.toLp g hgL2 ∧ ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g ∧ tsupport g ⊆ U)
:
theorem
HCPolySupport.measurable_toHilbertMatrixL2_aee_of_dense_smoothProbeSet
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hDense :
Dense
{f : ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U)) | ∃ (g : Vec d → HilbertMat d) (hgL2 : MeasureTheory.MemLp g 2 (volumeMeasureOn U)),
f = MeasureTheory.MemLp.toLp g hgL2 ∧ ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g ∧ tsupport g ⊆ U})
:
theorem
HCPolySupport.measurable_toHilbertMatrixL2_aee_of_isOpen_volume_ne_top
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hUopen : IsOpen U)
(hUfinite : MeasureTheory.volume U ≠ ⊤)
:
On an open finite-measure domain, the AEE quantitative-slice coefficient
field as an L² Hilbert-matrix object is measurable for the local sigma
algebra.
theorem
HCPolySupport.measurable_toHilbertMatrixL2_aeeQuantitativeEllipticSlice_cubeSet
{d : ℕ}
(Q : TriadicCube d)
(k : ℕ)
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet Q))]
:
On a half-open triadic cube, the AEE quantitative-slice coefficient field
as an L² Hilbert-matrix object is measurable for the local sigma algebra.