Coarse-graining support: Support.Book.Ch04.Internal.AEESliceAssembly.BlockEnergyAverage #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
AEE quantitative slice assembly #
Audit tag (Ch4 rebuild contract CH04_REBUILD_SURFACE_2026-05-16.md) #
Internal claim: the probability-facing replacement of the pointwise
quantitative-slice handoff. Re-routes the block-energy-average
measurability of Internal/FixedCompetitorEnergyMeasurability through the
a.e.-elliptic slice predicate AEEQuantitativeEllipticSlice, so the
local-test σ-algebra lane only needs a.e. quantitative ellipticity
information rather than a pointwise total cover.
Consumed by: AEESliceAssembly/MuFamily.lean, then
Theorems/Mu.lean :: aemeasurable_Mu_cubeSet and the AEE-slice
specialization
aemeasurable_Mu_cubeSet_of_measurable_aeeQuantitativeSlice.
Downstream developments should consume this through high-level
measurability bridges (e.g. HasMeasurableMuFamily) rather than threading
AEE-slice predicates through deterministic estimates.
If the single-claim summary above grows into three or more distinct claims, split or refactor per the rebuild contract.
theorem
HCPolySupport.AEEQuantitativeEllipticSlice.ae_hilbertMatrixL2_mem_ellipticMatrixSet
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a })
:
∀ᵐ (x : Vec d) ∂volumeMeasureOn U, ↑↑(toHilbertMatrixL2 a) x ∈ quantitativeEllipticHilbertMatSet d k
theorem
HCPolySupport.AEEQuantitativeEllipticSlice.ae_fullBlockCoeffEntry_toHilbertMatrixL2_eq
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a })
(α β : BlockCoord d)
:
(fun (x : Vec d) => toFullBlockMat (blockCoeffField (↑a) x) α β) =ᵐ[volumeMeasureOn U] fun (x : Vec d) =>
toFullBlockMat (blockMatrixOfCoeff (↑↑(toHilbertMatrixL2 a) x).toMat) α β
theorem
HCPolySupport.AEEQuantitativeEllipticSlice.weightedFullBlockCoeffEntryIntegral_eq_hilbertMatrixL2
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a })
(w : Vec d → ℝ)
(α β : BlockCoord d)
:
∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (↑a) x) α β = ∫ (x : Vec d), w x * toFullBlockMat (blockMatrixOfCoeff (↑↑(toHilbertMatrixL2 a) x).toMat) α β ∂volumeMeasureOn U
theorem
HCPolySupport.AEEQuantitativeEllipticSlice.measurable_l2WeightedBlockEntryIntegral_of_lipschitz
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hToL2 : Measurable toHilbertMatrixL2)
{w : Vec d → ℝ}
(hw : MemScalarL2 U w)
(α β : BlockCoord d)
{K : NNReal}
{Q : HilbertMat d → ℝ}
(hQ : LipschitzWith K Q)
(hQ_eq : ∀ A ∈ quantitativeEllipticHilbertMatSet d k, Q A = toFullBlockMat (blockMatrixOfCoeff A.toMat) α β)
:
Measurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (↑a) x) α β
theorem
HCPolySupport.AEEQuantitativeEllipticSlice.measurable_l2WeightedFullBlockCoeffEntryIntegral_of_lipschitzOn
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hToL2 : Measurable toHilbertMatrixL2)
{w : Vec d → ℝ}
(hw : MemScalarL2 U w)
(α β : BlockCoord d)
{K : NNReal}
(hLip :
LipschitzOnWith K (fun (A : HilbertMat d) => toFullBlockMat (blockMatrixOfCoeff A.toMat) α β)
(quantitativeEllipticHilbertMatSet d k))
:
Measurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (↑a) x) α β
theorem
HCPolySupport.AEEQuantitativeEllipticSlice.measurable_l2WeightedFullBlockCoeffEntryIntegral
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hToL2 : Measurable toHilbertMatrixL2)
{w : Vec d → ℝ}
(hw : MemScalarL2 U w)
(α β : BlockCoord d)
:
Measurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (↑a) x) α β
theorem
HCPolySupport.AEEQuantitativeEllipticSlice.integrable_weightedFullBlockCoeffEntry_of_integrable
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{k : ℕ}
{w : Vec d → ℝ}
(hSlice : AEEQuantitativeEllipticSlice U k a)
(hw : MeasureTheory.Integrable w (volumeMeasureOn U))
(α β : BlockCoord d)
:
MeasureTheory.Integrable (fun (x : Vec d) => w x * toFullBlockMat (blockCoeffField a x) α β) (volumeMeasureOn U)
theorem
HCPolySupport.AEEQuantitativeEllipticSlice.measurable_integrableWeightedBlockEntryIntegral
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hToL2 : Measurable toHilbertMatrixL2)
{w : Vec d → ℝ}
(hw_meas : Measurable w)
(hw_int : MeasureTheory.Integrable w (volumeMeasureOn U))
(α β : BlockCoord d)
:
Measurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (↑a) x) α β
theorem
HCPolySupport.AEEQuantitativeEllipticSlice.measurable_integrableWeightedFullBlockCoeffEntryIntegral
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hToL2 : Measurable toHilbertMatrixL2)
{w : Vec d → ℝ}
(hw : MeasureTheory.Integrable w (volumeMeasureOn U))
(α β : BlockCoord d)
:
Measurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (↑a) x) α β
theorem
HCPolySupport.AEEQuantitativeEllipticSlice.integrableOn_weightedFullBlockCoeffEntry_of_memBlockL2
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{k : ℕ}
{X : BlockState d}
(hSlice : AEEQuantitativeEllipticSlice U k a)
(hX : MemBlockL2 U X.eval)
(α β : BlockCoord d)
:
MeasureTheory.IntegrableOn
(fun (x : Vec d) => blockEnergyEntryWeight X α β x * toFullBlockMat (blockCoeffField a x) α β) U MeasureTheory.volume
theorem
HCPolySupport.AEEQuantitativeEllipticSlice.integrableOn_pairingWeightedFullBlockCoeffEntry_of_memBlockL2
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{k : ℕ}
{X Y : BlockState d}
(hSlice : AEEQuantitativeEllipticSlice U k a)
(hX : MemBlockL2 U X.eval)
(hY : MemBlockL2 U Y.eval)
(α β : BlockCoord d)
:
MeasureTheory.IntegrableOn
(fun (x : Vec d) => blockPairingEntryWeight X Y α β x * toFullBlockMat (blockCoeffField a x) α β) U
MeasureTheory.volume
theorem
HCPolySupport.measurable_blockEnergyAverage_aeeQuantitativeSlice
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hToL2 : Measurable AEEQuantitativeEllipticSlice.toHilbertMatrixL2)
(X : BlockState d)
(hX : MemBlockL2 U X.eval)
:
Measurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) => blockEnergyAverage U (↑a) X
theorem
HCPolySupport.measurable_blockPairingAverage_aeeQuantitativeSlice
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hToL2 : Measurable AEEQuantitativeEllipticSlice.toHilbertMatrixL2)
(X Y : BlockState d)
(hX : MemBlockL2 U X.eval)
(hY : MemBlockL2 U Y.eval)
:
Measurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice U k a }) => blockPairingAverage U (↑a) X Y
theorem
HCPolySupport.measurable_energyBilin_canonicalAEEMuGenerator_aeeQuantitativeSlice_cubeSet
{d : ℕ}
(Q : TriadicCube d)
(k : ℕ)
(Y Z : ↥(canonicalMuBlockCorrectionGeneratorSubmodule (cubeSet Q)))
:
Measurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) =>
((canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization.energyBilin
↑(canonicalMuCorrectionGeneratorEmbedding (cubeSet Q) Y))
↑(canonicalMuCorrectionGeneratorEmbedding (cubeSet Q) Z)
Canonical AEE cube-slice measurability of the Hilbert bilinear form on two dense-generator correction probes.
theorem
HCPolySupport.measurable_energyBilin_const_canonicalAEEMuGenerator_aeeQuantitativeSlice_cubeSet
{d : ℕ}
(Q : TriadicCube d)
(k : ℕ)
(P : BlockVec d)
(Y : ↥(canonicalMuBlockCorrectionGeneratorSubmodule (cubeSet Q)))
:
Measurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) =>
((canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization.energyBilin
((canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization.constantField P))
↑(canonicalMuCorrectionGeneratorEmbedding (cubeSet Q) Y)
Canonical AEE cube-slice measurability of the Hilbert bilinear form on a constant affine shift and one dense-generator correction probe.
theorem
HCPolySupport.measurable_energyBilin_fixed_canonicalMuGeneratorAffineField_aeeQuantitativeSlice_cubeSet
{d : ℕ}
(Q : TriadicCube d)
(k : ℕ)
(P : BlockVec d)
(Y : BlockState d)
(hY : MemBlockL2 (cubeSet Q) Y.eval)
(Z : ↥(canonicalMuBlockCorrectionGeneratorSubmodule (cubeSet Q)))
:
Measurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) =>
((canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization.energyBilin (toHilbertBlockL2OfBlockField hY))
(blockVecToHilbertBlockL2Const P + ↑(canonicalMuCorrectionGeneratorEmbedding (cubeSet Q) Z))
Canonical AEE cube-slice measurability of the Hilbert bilinear form on a
fixed block-L² test and one affine dense-generator probe. This is the
internal scalar-response source for measuring operator-image averages of the
selected doubled-Mu minimizer against deterministic tests.
theorem
HCPolySupport.measurable_galerkinAffineMinimizer_canonicalAEEMuGenerator_aeeQuantitativeSlice_cubeSet
{d : ℕ}
(Q : TriadicCube d)
(k : ℕ)
(P : BlockVec d)
{n : ℕ}
(e : Fin n → ↥(canonicalMuBlockCorrectionGeneratorSubmodule (cubeSet Q)))
:
Measurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) =>
galerkinAffineMinimizer (canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization.energyBilin
((canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization.constantField P) fun (i : Fin n) =>
↑(canonicalMuCorrectionGeneratorEmbedding (cubeSet Q) (e i))
Canonical AEE cube-slice measurability of every finite Galerkin affine minimizer built from dense-generator correction probes.
theorem
HCPolySupport.stronglyMeasurable_canonicalAEEMuHilbertMinimizer_aeeQuantitativeSlice_cubeSet_of_galerkin_energy
{d : ℕ}
(Q : TriadicCube d)
(k : ℕ)
(P : BlockVec d)
(e : (m : ℕ) → Fin m → ↥(canonicalMuBlockCorrectionGeneratorSubmodule (cubeSet Q)))
(v : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a } → ℕ → ↥(HilbertBlockL2 (cubeSet Q)))
(hv_mem :
∀ (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) (m : ℕ),
have H := (canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization;
v a m - H.constantField P ∈ (canonicalAEEMuCorrectionSpaceData Q).correctionSpace)
(hEnergy :
∀ (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) (m : ℕ),
have H := (canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization;
quadraticEnergy H.energyBilin
(galerkinAffineMinimizer H.energyBilin (H.constantField P) fun (i : Fin m) =>
↑(canonicalMuCorrectionGeneratorEmbedding (cubeSet Q) (e m i))) ≤ quadraticEnergy H.energyBilin (v a m))
(hv_tendsto :
∀ (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }),
have H := (canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization;
Filter.Tendsto (fun (m : ℕ) => v a m) Filter.atTop
(nhds
((affineMinimizerMap (canonicalAEEMuCorrectionSpaceData Q).correctionSpace H.energyBilin ⋯)
(H.constantField P))))
:
MeasureTheory.StronglyMeasurable fun (a : { a : CoeffField d // AEEQuantitativeEllipticSlice (cubeSet Q) k a }) =>
have H := (canonicalAEEMuOperatorSystemData Q k a).toMuHilbertRealization;
(affineMinimizerMap (canonicalAEEMuCorrectionSpaceData Q).correctionSpace H.energyBilin ⋯) (H.constantField P)
Slice-local strong measurability of the selected canonical doubled-Mu
Hilbert minimizer, once the canonical finite Galerkin approximants satisfy the
deterministic energy-comparison convergence hypotheses.
theorem
HCPolySupport.measurable_subtype_mk_aeeQuantitativeSlice_of_isLocalSigmaMeasurableOn
{Ω : Type u_1}
[MeasurableSpace Ω]
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
(A : Ω → CoeffField d)
(hA : IsPointwiseLocalSigmaMeasurableOn A U)
(hSlice : ∀ (ω : Ω), AEEQuantitativeEllipticSlice U k (A ω))
:
Measurable fun (ω : Ω) => ⟨A ω, ⋯⟩
theorem
HCPolySupport.measurable_blockEnergyAverage_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 ω))
(X : BlockState d)
(hX : MemBlockL2 U X.eval)
:
Measurable fun (ω : Ω) => blockEnergyAverage U (A ω) X
theorem
HCPolySupport.measurable_blockPairingAverage_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 ω))
(X Y : BlockState d)
(hX : MemBlockL2 U X.eval)
(hY : MemBlockL2 U Y.eval)
:
Measurable fun (ω : Ω) => blockPairingAverage U (A ω) X Y
theorem
HCPolySupport.measurable_blockEnergyAverage_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 ω))
(X : BlockState d)
(hX : MemBlockL2 U X.eval)
:
Measurable fun (ω : Ω) => blockEnergyAverage U (A ω) X
theorem
HCPolySupport.aemeasurable_blockEnergyAverage_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 ω))
(X : BlockState d)
(hX : MemBlockL2 U X.eval)
:
AEMeasurable (fun (ω : Ω) => blockEnergyAverage U (A ω) X) μ
theorem
HCPolySupport.measurable_blockEnergyAverage_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 ω))
(X : BlockState d)
(hX : MemBlockL2 U X.eval)
:
Measurable fun (ω : Ω) => blockEnergyAverage U (A ω) X
theorem
HCPolySupport.aemeasurable_blockEnergyAverage_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 ω))
(X : BlockState d)
(hX : MemBlockL2 U X.eval)
:
AEMeasurable (fun (ω : Ω) => blockEnergyAverage U (A ω) X) μ
theorem
HCPolySupport.aemeasurable_blockEnergyAverage_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 ω))
(X : BlockState d)
(hX : MemBlockL2 U X.eval)
:
AEMeasurable (fun (ω : Ω) => blockEnergyAverage U (A ω) X) μ