Coarse-graining support: Support.Book.Ch04.Internal.FixedCompetitorEnergyMeasurability.Integrals #
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: integrability and a.e. membership of toHilbertMatrixL2
in the quantitative-elliptic Hilbert-matrix set, plus the Bochner-integral
algebra needed to take the Lipschitz scalar atoms from LipschitzBounds.lean
and turn them into measurable energy-functional integrals on quantitative
slices.
Consumed by (within Internal/FixedCompetitorEnergyMeasurability/):
BlockEnergyAverage.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.QuantitativeEllipticSlice.ae_hilbertMatrixL2_mem_ellipticMatrixSet
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(a : { a : CoeffField d // QuantitativeEllipticSlice U k a })
:
∀ᵐ (x : Vec d) ∂volumeMeasureOn U, ↑↑(toHilbertMatrixL2 a) x ∈ quantitativeEllipticHilbertMatSet d k
theorem
HCPolySupport.IsPointwiseLocalSigmaMeasurableOn.measurable_entryTestObservable
{Ω : Type u_1}
[MeasurableSpace Ω]
{d : ℕ}
{A : Ω → CoeffField d}
{U : Set (Vec d)}
(hA : IsPointwiseLocalSigmaMeasurableOn A U)
(i j : Fin d)
{φ : Vec d → ℝ}
(hφ_cont : ContDiff ℝ (↑⊤) φ)
(hφ_compact : HasCompactSupport φ)
(hφ_support : tsupport φ ⊆ U)
:
Measurable fun (ω : Ω) => ∫ (x : Vec d), A ω x i j * φ x
theorem
HCPolySupport.measurable_blockEnergyDensity_eval
{d : ℕ}
(X : BlockState d)
(x : Vec d)
:
Measurable fun (a : CoeffField d) => blockEnergyDensity a X x
theorem
HCPolySupport.blockEnergyDensity_eq_sum_fullBlockMat_entries
{d : ℕ}
(a : CoeffField d)
(X : BlockState d)
(x : Vec d)
:
blockEnergyDensity a X x = 1 / 2 * ∑ α : BlockCoord d,
∑ β : BlockCoord d,
toFullBlockVec (X.eval x) α * toFullBlockVec (X.eval x) β * toFullBlockMat (blockCoeffField a x) α β
theorem
HCPolySupport.memScalarL2_fullBlockCoord_of_memBlockL2
{d : ℕ}
{U : Set (Vec d)}
{F : Vec d → BlockVec d}
(hF : MemBlockL2 U F)
(α : BlockCoord d)
:
MemScalarL2 U fun (x : Vec d) => toFullBlockVec (F x) α
theorem
HCPolySupport.integrableOn_fullBlockCoord_mul_of_memBlockL2
{d : ℕ}
{U : Set (Vec d)}
{F : Vec d → BlockVec d}
(hF : MemBlockL2 U F)
(α β : BlockCoord d)
:
MeasureTheory.IntegrableOn (fun (x : Vec d) => toFullBlockVec (F x) α * toFullBlockVec (F x) β) U MeasureTheory.volume
theorem
HCPolySupport.abs_toFullBlockMat_blockMatrixOfCoeff_entry_le_of_isEllipticMatrix
{d : ℕ}
{A : Mat d}
{lam Lam : ℝ}
(hA : IsEllipticMatrix lam Lam A)
(α β : BlockCoord d)
:
theorem
HCPolySupport.abs_fullBlockCoeffEntry_hilbertMat_le_of_mem_quantitativeEllipticHilbertMatSet
{d k : ℕ}
{A : HilbertMat d}
(hA : A ∈ quantitativeEllipticHilbertMatSet d k)
(α β : BlockCoord d)
:
|toFullBlockMat (blockMatrixOfCoeff A.toMat) α β| ≤ √(blockMatrixOfCoeffNormSqBound (↑k + 1)⁻¹ (↑k + 1))
theorem
HCPolySupport.QuantitativeEllipticSlice.ae_fullBlockCoeffEntry_toHilbertMatrixL2_eq
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(a : { a : CoeffField d // QuantitativeEllipticSlice 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.QuantitativeEllipticSlice.ae_abs_fullBlockCoeffEntry_toHilbertMatrixL2_le
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(a : { a : CoeffField d // QuantitativeEllipticSlice U k a })
(α β : BlockCoord d)
:
∀ᵐ (x : Vec d) ∂volumeMeasureOn U, |toFullBlockMat (blockMatrixOfCoeff (↑↑(toHilbertMatrixL2 a) x).toMat) α β| ≤ √(blockMatrixOfCoeffNormSqBound (↑k + 1)⁻¹ (↑k + 1))
theorem
HCPolySupport.QuantitativeEllipticSlice.weightedFullBlockCoeffEntryIntegral_eq_hilbertMatrixL2
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(a : { a : CoeffField d // QuantitativeEllipticSlice 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.measurable_l2WeightedHilbertMatrixLipschitzIntegral
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{d : ℕ}
{U : Set (Vec d)}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
{F : Ω → ↥(MeasureTheory.Lp (HilbertMat d) 2 (volumeMeasureOn U))}
(hF : Measurable F)
{w : Vec d → ℝ}
(hw : MemScalarL2 U w)
{K : NNReal}
{Q : HilbertMat d → ℝ}
(hQ : LipschitzWith K Q)
:
Measurable fun (ω : Ω) => ∫ (x : Vec d), w x * Q (↑↑(F ω) x) ∂volumeMeasureOn U
If a scalar observable of a Hilbert-matrix value has a global Lipschitz
extension, then its L²-weighted integral is measurable as a function of the
L² Hilbert-matrix field. This is the Nemytskii/pairing bridge used before
the final L¹ weight approximation.
theorem
HCPolySupport.QuantitativeEllipticSlice.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 // QuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (↑a) x) α β
Slice-level version of the Lipschitz-extension bridge for a full-block coefficient entry. The agreement hypothesis keeps the theorem independent of the later finite-dimensional extension construction.
theorem
HCPolySupport.QuantitativeEllipticSlice.measurable_weightedBlockEntryIntegral_of_openFiniteLipschitz
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hUopen : IsOpen U)
(hUfinite : MeasureTheory.volume U ≠ ⊤)
{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 // QuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (↑a) x) α β
Open finite-measure wrapper for the L²-weighted full-block entry bridge.
The only remaining external input is the finite-dimensional Lipschitz extension
of the entry observable.
theorem
HCPolySupport.QuantitativeEllipticSlice.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 // QuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (↑a) x) α β
If the finite-dimensional full-block entry is Lipschitz on the
quantitative elliptic value set, then the L²-weighted entry integral is
measurable on the slice. The global Lipschitz extension is supplied by
LipschitzOnWith.extend_real.
theorem
HCPolySupport.QuantitativeEllipticSlice.measurable_weightedBlockEntryIntegral_of_openFiniteLipschitzOn
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hUopen : IsOpen U)
(hUfinite : MeasureTheory.volume U ≠ ⊤)
{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 // QuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (↑a) x) α β
Open finite-measure wrapper for the Lipschitz-on-value-set version.
theorem
HCPolySupport.QuantitativeEllipticSlice.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 // QuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (↑a) x) α β
Slice-level L²-weighted full-block entry measurability with the
finite-dimensional quantitative Lipschitz estimate supplied internally.
theorem
HCPolySupport.QuantitativeEllipticSlice.measurable_l2WeightedFullBlockCoeffEntryIntegral_of_isOpen_volume_ne_top
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hUopen : IsOpen U)
(hUfinite : MeasureTheory.volume U ≠ ⊤)
{w : Vec d → ℝ}
(hw : MemScalarL2 U w)
(α β : BlockCoord d)
:
Measurable fun (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (↑a) x) α β
Open finite-measure wrapper for the fully internal L²-weighted
full-block entry measurability theorem.
theorem
HCPolySupport.abs_toFullBlockMat_blockCoeffField_entry_le_of_isEllipticFieldOn
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U a)
{x : Vec d}
(hx : x ∈ U)
(α β : BlockCoord d)
:
theorem
HCPolySupport.QuantitativeEllipticSlice.integrable_weightedFullBlockCoeffEntry_of_integrable
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{k : ℕ}
{w : Vec d → ℝ}
(hSlice : QuantitativeEllipticSlice 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.QuantitativeEllipticSlice.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 // QuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (↑a) x) α β
L¹ deterministic weights are enough for slice-level full-block entry
measurability, provided the weight is represented by an honest measurable
function. The proof approximates the weight by simple functions, uses the
already-proved L² theorem for each approximant, and passes to the limit by
the uniform quantitative ellipticity bound on the slice.
theorem
HCPolySupport.QuantitativeEllipticSlice.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 // QuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (↑a) x) α β
L¹ deterministic weights are enough for slice-level full-block entry
measurability. This wrapper removes the need for callers to choose a
measurable representative of an integrable weight.
theorem
HCPolySupport.QuantitativeEllipticSlice.measurable_integrableWeightedBlockEntryIntegral_of_openFinite
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hUopen : IsOpen U)
(hUfinite : MeasureTheory.volume U ≠ ⊤)
{w : Vec d → ℝ}
(hw : MeasureTheory.Integrable w (volumeMeasureOn U))
(α β : BlockCoord d)
:
Measurable fun (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, w x * toFullBlockMat (blockCoeffField (↑a) x) α β
Open finite-measure wrapper for the L¹-weighted full-block entry
measurability theorem.
theorem
HCPolySupport.QuantitativeEllipticSlice.blockEnergyDensity_integrableOn_of_memBlockL2
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{k : ℕ}
{X : BlockState d}
(hSlice : QuantitativeEllipticSlice U k a)
(hX : MemBlockL2 U X.eval)
:
noncomputable def
HCPolySupport.blockEnergyEntryWeight
{d : ℕ}
(X : BlockState d)
(α β : BlockCoord d)
(x : Vec d)
:
Half the product of the α and β coordinates of the block state, the weight of a
coefficient entry in its energy density.
Equations
- HCPolySupport.blockEnergyEntryWeight X α β x = 1 / 2 * (HCPolySupport.toFullBlockVec (X.eval x) α * HCPolySupport.toFullBlockVec (X.eval x) β)
Instances For
noncomputable def
HCPolySupport.blockPairingEntryWeight
{d : ℕ}
(X Y : BlockState d)
(α β : BlockCoord d)
(x : Vec d)
:
The product of coordinate α of X and coordinate β of Y, the weight of a coefficient
entry in their block pairing.
Equations
- HCPolySupport.blockPairingEntryWeight X Y α β x = HCPolySupport.toFullBlockVec (X.eval x) α * HCPolySupport.toFullBlockVec (Y.eval x) β
Instances For
theorem
HCPolySupport.integrable_blockEnergyEntryWeight_of_memBlockL2
{d : ℕ}
{U : Set (Vec d)}
{X : BlockState d}
(hX : MemBlockL2 U X.eval)
(α β : BlockCoord d)
:
theorem
HCPolySupport.integrable_blockPairingEntryWeight_of_memBlockL2
{d : ℕ}
{U : Set (Vec d)}
{X Y : BlockState d}
(hX : MemBlockL2 U X.eval)
(hY : MemBlockL2 U Y.eval)
(α β : BlockCoord d)
:
MeasureTheory.Integrable (blockPairingEntryWeight X Y α β) (volumeMeasureOn U)
theorem
HCPolySupport.QuantitativeEllipticSlice.integrableOn_weightedFullBlockCoeffEntry_of_memBlockL2
{d : ℕ}
{U : Set (Vec d)}
{a : CoeffField d}
{k : ℕ}
{X : BlockState d}
(hSlice : QuantitativeEllipticSlice 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.blockEnergyDensity_eq_sum_entryWeights
{d : ℕ}
(a : CoeffField d)
(X : BlockState d)
(x : Vec d)
:
blockEnergyDensity a X x = ∑ α : BlockCoord d, ∑ β : BlockCoord d, blockEnergyEntryWeight X α β x * toFullBlockMat (blockCoeffField a x) α β
theorem
HCPolySupport.blockPairingIntegrand_eq_sum_entryWeights
{d : ℕ}
(a : CoeffField d)
(X Y : BlockState d)
(x : Vec d)
:
blockPairingIntegrand a X Y x = ∑ α : BlockCoord d, ∑ β : BlockCoord d, blockPairingEntryWeight X Y α β x * toFullBlockMat (blockCoeffField a x) α β
theorem
HCPolySupport.blockEnergyAverage_eq_sum_weightedFullBlockCoeffEntryIntegrals
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
(X : BlockState d)
(hInt :
∀ (α β : BlockCoord d),
MeasureTheory.IntegrableOn
(fun (x : Vec d) => blockEnergyEntryWeight X α β x * toFullBlockMat (blockCoeffField a x) α β) U
MeasureTheory.volume)
:
blockEnergyAverage U a X = (MeasureTheory.volume U).toReal⁻¹ * ∑ α : BlockCoord d,
∑ β : BlockCoord d, ∫ (x : Vec d) in U, blockEnergyEntryWeight X α β x * toFullBlockMat (blockCoeffField a x) α β
theorem
HCPolySupport.blockPairingAverage_eq_sum_weightedFullBlockCoeffEntryIntegrals
{d : ℕ}
(U : Set (Vec d))
(a : CoeffField d)
(X Y : BlockState d)
(hInt :
∀ (α β : BlockCoord d),
MeasureTheory.IntegrableOn
(fun (x : Vec d) => blockPairingEntryWeight X Y α β x * toFullBlockMat (blockCoeffField a x) α β) U
MeasureTheory.volume)
:
blockPairingAverage U a X Y = (MeasureTheory.volume U).toReal⁻¹ * ∑ α : BlockCoord d,
∑ β : BlockCoord d,
∫ (x : Vec d) in U, blockPairingEntryWeight X Y α β x * toFullBlockMat (blockCoeffField a x) α β
theorem
HCPolySupport.measurable_blockEnergyAverage_of_measurable_weightedFullBlockCoeffEntryIntegrals
{d : ℕ}
{U : Set (Vec d)}
(X : BlockState d)
(hInt :
∀ (a : CoeffField d) (α β : BlockCoord d),
MeasureTheory.IntegrableOn
(fun (x : Vec d) => blockEnergyEntryWeight X α β x * toFullBlockMat (blockCoeffField a x) α β) U
MeasureTheory.volume)
(hMeas :
∀ (α β : BlockCoord d),
Measurable fun (a : CoeffField d) =>
∫ (x : Vec d) in U, blockEnergyEntryWeight X α β x * toFullBlockMat (blockCoeffField a x) α β)
:
Measurable fun (a : CoeffField d) => blockEnergyAverage U a X
theorem
HCPolySupport.measurable_blockPairingAverage_of_measurable_weightedFullBlockCoeffEntryIntegrals
{d : ℕ}
{U : Set (Vec d)}
(X Y : BlockState d)
(hInt :
∀ (a : CoeffField d) (α β : BlockCoord d),
MeasureTheory.IntegrableOn
(fun (x : Vec d) => blockPairingEntryWeight X Y α β x * toFullBlockMat (blockCoeffField a x) α β) U
MeasureTheory.volume)
(hMeas :
∀ (α β : BlockCoord d),
Measurable fun (a : CoeffField d) =>
∫ (x : Vec d) in U, blockPairingEntryWeight X Y α β x * toFullBlockMat (blockCoeffField a x) α β)
:
Measurable fun (a : CoeffField d) => blockPairingAverage U a X Y
theorem
HCPolySupport.measurable_blockEnergyAverage_comp_of_measurable_weightedFullBlockCoeffEntryIntegrals
{Ω : Type u_1}
[MeasurableSpace Ω]
{d : ℕ}
{U : Set (Vec d)}
(A : Ω → CoeffField d)
(X : BlockState d)
(hInt :
∀ (ω : Ω) (α β : BlockCoord d),
MeasureTheory.IntegrableOn
(fun (x : Vec d) => blockEnergyEntryWeight X α β x * toFullBlockMat (blockCoeffField (A ω) x) α β) U
MeasureTheory.volume)
(hMeas :
∀ (α β : BlockCoord d),
Measurable fun (ω : Ω) =>
∫ (x : Vec d) in U, blockEnergyEntryWeight X α β x * toFullBlockMat (blockCoeffField (A ω) x) α β)
:
Measurable fun (ω : Ω) => blockEnergyAverage U (A ω) X
theorem
HCPolySupport.measurable_blockPairingAverage_comp_of_measurable_weightedFullBlockCoeffEntryIntegrals
{Ω : Type u_1}
[MeasurableSpace Ω]
{d : ℕ}
{U : Set (Vec d)}
(A : Ω → CoeffField d)
(X Y : BlockState d)
(hInt :
∀ (ω : Ω) (α β : BlockCoord d),
MeasureTheory.IntegrableOn
(fun (x : Vec d) => blockPairingEntryWeight X Y α β x * toFullBlockMat (blockCoeffField (A ω) x) α β) U
MeasureTheory.volume)
(hMeas :
∀ (α β : BlockCoord d),
Measurable fun (ω : Ω) =>
∫ (x : Vec d) in U, blockPairingEntryWeight X Y α β x * toFullBlockMat (blockCoeffField (A ω) x) α β)
:
Measurable fun (ω : Ω) => blockPairingAverage U (A ω) X Y
theorem
HCPolySupport.measurable_blockEnergyAverage_quantitativeSlice_of_measurable_weightedFullBlockCoeffEntryIntegrals
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
(X : BlockState d)
(hX : MemBlockL2 U X.eval)
(hMeas :
∀ (α β : BlockCoord d),
Measurable fun (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) =>
∫ (x : Vec d) in U, blockEnergyEntryWeight X α β x * toFullBlockMat (blockCoeffField (↑a) x) α β)
:
Measurable fun (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) => blockEnergyAverage U (↑a) X
theorem
HCPolySupport.measurable_blockEnergyAverage_quantitativeSlice
{d : ℕ}
{U : Set (Vec d)}
{k : ℕ}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)]
(hToL2 : Measurable QuantitativeEllipticSlice.toHilbertMatrixL2)
(X : BlockState d)
(hX : MemBlockL2 U X.eval)
:
Measurable fun (a : { a : CoeffField d // QuantitativeEllipticSlice U k a }) => blockEnergyAverage U (↑a) X
Fixed-competitor energy averages are measurable on a quantitative elliptic
slice once the slice has the note-facing measurable L² realization.