Coarse-graining support: Support.Book.Ch04.Internal.CoarseObservableMeasurability.Basic

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: the product measurable structure on Mat d and FullBlockMat d coincides with their Borel σ-algebras, giving the generic Bochner-integral API a measurable-target for full coarse matrices.

Consumed by:

• HCPolySupport/Book/Ch04/AnnealedObjects.lean
• HCPolySupport/Book/Ch04/Theorems/CoarseObservables.lean (aemeasurable_coarseFullBlockMatrix_cubeSet and entrywise wrappers)
• HCPolySupport/Book/Ch04/Internal/CoarseObservableMeasurability/Mu.lean

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

instance HCPolySupport.instBorelSpaceMat (d : ℕ) : BorelSpace (Mat d)

The product measurable structure on Mat d agrees with its Borel sigma-algebra. This lets the generic Bochner-integral API target full coarse matrices directly.

@[instance_reducible]

instance HCPolySupport.instMeasurableSpaceFullBlockMat (d : ℕ) : MeasurableSpace (FullBlockMat d)

Equations

• HCPolySupport.instMeasurableSpaceFullBlockMat d = id inferInstance

instance HCPolySupport.instBorelSpaceFullBlockMat (d : ℕ) : BorelSpace (FullBlockMat d)

The unfolded 2d × 2d block matrices carry the Borel sigma-algebra coming from their coordinatewise matrix topology.

@[instance_reducible]

instance HCPolySupport.instContinuousENormMatrix {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] : ContinuousENorm (Matrix m n ℝ)

Matrix.instTopologicalSpace (the ambient, always-active topology on Matrix m n R, coming from the coordinatewise Pi topology) and the elementwise-norm-derived topology from open scoped Matrix.Norms.Elementwise are only defeq once Matrix is unfolded to its underlying Pi type, which instance search will not do on its own. This head-class cache resolves the resulting ContinuousENorm synthesis gap for every Matrix m n ℝ-valued Measurable/Integrable statement in this file (and its Mat d/FullBlockMat d specializations).

Equations

• HCPolySupport.instContinuousENormMatrix = id inferInstance

def HCPolySupport.HasMeasurableMuFamily {d : ℕ} (U : Set (Vec d)) : Prop

Strong ambient measurability of the variational quantity Mu U P a for every deterministic block loading P.

Equations

• HCPolySupport.HasMeasurableMuFamily U = ∀ (P : HCPolySupport.BlockVec d), Measurable fun (a : HCPolySupport.CoeffField d) => HCPolySupport.Mu U P a

theorem HCPolySupport.hasMeasurableMuFamily_of_forall_mu_eq {d : ℕ} {U V : Set (Vec d)} (hMu : HasMeasurableMuFamily V) (hEq : ∀ (P : BlockVec d) (a : CoeffField d), Mu U P a = Mu V P a) : HasMeasurableMuFamily U

Transport HasMeasurableMuFamily across pointwise identities for the full Mu family.

theorem HCPolySupport.hasMeasurableMuFamily_iff_of_forall_mu_eq {d : ℕ} {U V : Set (Vec d)} (hEq : ∀ (P : BlockVec d) (a : CoeffField d), Mu U P a = Mu V P a) : HasMeasurableMuFamily U ↔ HasMeasurableMuFamily V

Two domains share the same measurable Mu family whenever their Mu values agree pointwise on every deterministic loading.

noncomputable def HCPolySupport.coarseSigmaStarInvEntryObservable {d : ℕ} (U : Set (Vec d)) (r c : Fin d) : CoeffField d → ℝ

The (r,c) entry of the coarse inverse-star matrix observable a ↦ \sigma_*^{-1}(U; a).

Equations

• HCPolySupport.coarseSigmaStarInvEntryObservable U r c a = (HCPolySupport.coarseBlockMatrix U a).lowerRight r c

noncomputable def HCPolySupport.coarseBEntryObservable {d : ℕ} (U : Set (Vec d)) (r c : Fin d) : CoeffField d → ℝ

The (r,c) entry of the coarse upper-left block observable a ↦ b(U; a).

Equations

• HCPolySupport.coarseBEntryObservable U r c a = (HCPolySupport.coarseBlockMatrix U a).upperLeft r c

noncomputable def HCPolySupport.coarseSigmaStarInvKappaMeanEntryObservable {d : ℕ} (U : Set (Vec d)) (r c : Fin d) : CoeffField d → ℝ

The (r,c) entry of the mean mixed observable a ↦ \sigma_*^{-1}(U; a)\kappa(U; a).

Equations

• HCPolySupport.coarseSigmaStarInvKappaMeanEntryObservable U r c a = -(HCPolySupport.coarseBlockMatrix U a).lowerLeft r c

noncomputable def HCPolySupport.coarseUpperRightEntryObservable {d : ℕ} (U : Set (Vec d)) (r c : Fin d) : CoeffField d → ℝ

The (r,c) entry of the upper-right block of the doubled coarse matrix.

Equations

• HCPolySupport.coarseUpperRightEntryObservable U r c a = (HCPolySupport.coarseBlockMatrix U a).upperRight r c

noncomputable def HCPolySupport.coarseLowerLeftEntryObservable {d : ℕ} (U : Set (Vec d)) (r c : Fin d) : CoeffField d → ℝ

The (r,c) entry of the lower-left block of the doubled coarse matrix.

Equations

• HCPolySupport.coarseLowerLeftEntryObservable U r c a = (HCPolySupport.coarseBlockMatrix U a).lowerLeft r c

noncomputable def HCPolySupport.coarseFullBlockMatrixObservable {d : ℕ} (U : Set (Vec d)) : CoeffField d → FullBlockMat d

The full doubled coarse matrix observable in the unfolded 2d × 2d form.

Equations

• HCPolySupport.coarseFullBlockMatrixObservable U a = HCPolySupport.toFullBlockMat (HCPolySupport.coarseBlockMatrix U a)

def HCPolySupport.fullBlockMatUpperLeft {d : ℕ} : FullBlockMat d → Mat d

The upper-left d × d block of an unfolded coarse matrix.

Equations

• HCPolySupport.fullBlockMatUpperLeft M i j = M (Sum.inl i) (Sum.inl j)

def HCPolySupport.fullBlockMatUpperRight {d : ℕ} : FullBlockMat d → Mat d

The upper-right d × d block of an unfolded coarse matrix.

Equations

• HCPolySupport.fullBlockMatUpperRight M i j = M (Sum.inl i) (Sum.inr j)

def HCPolySupport.fullBlockMatLowerLeft {d : ℕ} : FullBlockMat d → Mat d

The lower-left d × d block of an unfolded coarse matrix.

Equations

• HCPolySupport.fullBlockMatLowerLeft M i j = M (Sum.inr i) (Sum.inl j)

def HCPolySupport.fullBlockMatLowerRight {d : ℕ} : FullBlockMat d → Mat d

The lower-right d × d block of an unfolded coarse matrix.

Equations

• HCPolySupport.fullBlockMatLowerRight M i j = M (Sum.inr i) (Sum.inr j)

def HCPolySupport.fullBlockMatNegLowerLeft {d : ℕ} : FullBlockMat d → Mat d

The negative lower-left block, matching the note-facing observable \sigma_*^{-1}(U; a)\kappa(U; a).

Equations

• HCPolySupport.fullBlockMatNegLowerLeft M i j = -M (Sum.inr i) (Sum.inl j)

noncomputable def HCPolySupport.coarseSigmaStarInvObservable {d : ℕ} (U : Set (Vec d)) : CoeffField d → Mat d

The full coarse inverse-star matrix observable a ↦ \sigma_*^{-1}(U; a).

Equations

• HCPolySupport.coarseSigmaStarInvObservable U = HCPolySupport.fullBlockMatLowerRight ∘ HCPolySupport.coarseFullBlockMatrixObservable U

noncomputable def HCPolySupport.coarseBObservable {d : ℕ} (U : Set (Vec d)) : CoeffField d → Mat d

The full coarse upper-left block observable a ↦ b(U; a).

Equations

• HCPolySupport.coarseBObservable U = HCPolySupport.fullBlockMatUpperLeft ∘ HCPolySupport.coarseFullBlockMatrixObservable U

noncomputable def HCPolySupport.coarseSigmaStarInvKappaMeanObservable {d : ℕ} (U : Set (Vec d)) : CoeffField d → Mat d

The full mean mixed observable a ↦ \sigma_*^{-1}(U; a)\kappa(U; a).

Equations

• HCPolySupport.coarseSigmaStarInvKappaMeanObservable U = HCPolySupport.fullBlockMatNegLowerLeft ∘ HCPolySupport.coarseFullBlockMatrixObservable U

@[simp]

theorem HCPolySupport.fullBlockMatUpperLeft_apply {d : ℕ} (M : FullBlockMat d) (i j : Fin d) : fullBlockMatUpperLeft M i j = M (Sum.inl i) (Sum.inl j)

@[simp]

theorem HCPolySupport.fullBlockMatUpperRight_apply {d : ℕ} (M : FullBlockMat d) (i j : Fin d) : fullBlockMatUpperRight M i j = M (Sum.inl i) (Sum.inr j)

@[simp]

theorem HCPolySupport.fullBlockMatLowerLeft_apply {d : ℕ} (M : FullBlockMat d) (i j : Fin d) : fullBlockMatLowerLeft M i j = M (Sum.inr i) (Sum.inl j)

@[simp]

theorem HCPolySupport.fullBlockMatLowerRight_apply {d : ℕ} (M : FullBlockMat d) (i j : Fin d) : fullBlockMatLowerRight M i j = M (Sum.inr i) (Sum.inr j)

@[simp]

theorem HCPolySupport.fullBlockMatNegLowerLeft_apply {d : ℕ} (M : FullBlockMat d) (i j : Fin d) : fullBlockMatNegLowerLeft M i j = -M (Sum.inr i) (Sum.inl j)

@[simp]

theorem HCPolySupport.coarseSigmaStarInvEntryObservable_apply {d : ℕ} (U : Set (Vec d)) (r c : Fin d) (a : CoeffField d) : coarseSigmaStarInvEntryObservable U r c a = (coarseBlockMatrix U a).lowerRight r c

@[simp]

theorem HCPolySupport.coarseSigmaStarInvObservable_apply {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : coarseSigmaStarInvObservable U a = (coarseBlockMatrix U a).lowerRight

@[simp]

theorem HCPolySupport.coarseBEntryObservable_apply {d : ℕ} (U : Set (Vec d)) (r c : Fin d) (a : CoeffField d) : coarseBEntryObservable U r c a = (coarseBlockMatrix U a).upperLeft r c

@[simp]

theorem HCPolySupport.coarseBObservable_apply {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : coarseBObservable U a = (coarseBlockMatrix U a).upperLeft

@[simp]

theorem HCPolySupport.coarseSigmaStarInvKappaMeanEntryObservable_apply {d : ℕ} (U : Set (Vec d)) (r c : Fin d) (a : CoeffField d) : coarseSigmaStarInvKappaMeanEntryObservable U r c a = -(coarseBlockMatrix U a).lowerLeft r c

@[simp]

theorem HCPolySupport.coarseUpperRightEntryObservable_apply {d : ℕ} (U : Set (Vec d)) (r c : Fin d) (a : CoeffField d) : coarseUpperRightEntryObservable U r c a = (coarseBlockMatrix U a).upperRight r c

@[simp]

theorem HCPolySupport.coarseLowerLeftEntryObservable_apply {d : ℕ} (U : Set (Vec d)) (r c : Fin d) (a : CoeffField d) : coarseLowerLeftEntryObservable U r c a = (coarseBlockMatrix U a).lowerLeft r c

@[simp]

theorem HCPolySupport.coarseSigmaStarInvKappaMeanObservable_apply {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : coarseSigmaStarInvKappaMeanObservable U a = -(coarseBlockMatrix U a).lowerLeft

@[simp]

theorem HCPolySupport.coarseFullBlockMatrixObservable_apply {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : coarseFullBlockMatrixObservable U a = toFullBlockMat (coarseBlockMatrix U a)

theorem HCPolySupport.measurable_fullBlockMatUpperLeft {d : ℕ} : Measurable fullBlockMatUpperLeft

theorem HCPolySupport.measurable_fullBlockMatUpperRight {d : ℕ} : Measurable fullBlockMatUpperRight

theorem HCPolySupport.measurable_fullBlockMatLowerLeft {d : ℕ} : Measurable fullBlockMatLowerLeft

theorem HCPolySupport.measurable_fullBlockMatLowerRight {d : ℕ} : Measurable fullBlockMatLowerRight

theorem HCPolySupport.measurable_fullBlockMatNegLowerLeft {d : ℕ} : Measurable fullBlockMatNegLowerLeft

theorem HCPolySupport.integral_matrix_apply {α : Type u_1} {m : Type u_2} {n : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Fintype m] [Fintype n] {f : α → Matrix m n ℝ} (hf : MeasureTheory.Integrable f μ) (i : m) (j : n) : (∫ (x : α), f x ∂μ) i j = ∫ (x : α), f x i j ∂μ

Entrywise evaluation of a Bochner integral of matrix-valued functions.

theorem HCPolySupport.integrable_coarseSigmaStarInvObservable_of_integrable_coarseFullBlockMatrixObservable {d : ℕ} {P : MeasureTheory.Measure (CoeffField d)} {U : Set (Vec d)} (hInt : MeasureTheory.Integrable (coarseFullBlockMatrixObservable U) P) : MeasureTheory.Integrable (coarseSigmaStarInvObservable U) P

theorem HCPolySupport.integrable_coarseBObservable_of_integrable_coarseFullBlockMatrixObservable {d : ℕ} {P : MeasureTheory.Measure (CoeffField d)} {U : Set (Vec d)} (hInt : MeasureTheory.Integrable (coarseFullBlockMatrixObservable U) P) : MeasureTheory.Integrable (coarseBObservable U) P

theorem HCPolySupport.integrable_coarseSigmaStarInvKappaMeanObservable_of_integrable_coarseFullBlockMatrixObservable {d : ℕ} {P : MeasureTheory.Measure (CoeffField d)} {U : Set (Vec d)} (hInt : MeasureTheory.Integrable (coarseFullBlockMatrixObservable U) P) : MeasureTheory.Integrable (coarseSigmaStarInvKappaMeanObservable U) P

theorem HCPolySupport.isLocalObservable_Mu {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (P : BlockVec d) : IsRestrictionLocalObservable U fun (a : CoeffField d) => Mu U P a

theorem HCPolySupport.isLocalObservable_coarseBlockMatrix {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) : IsRestrictionLocalObservable U fun (a : CoeffField d) => coarseBlockMatrix U a

theorem HCPolySupport.isLocalObservable_coarseFullBlockMatrixObservable {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) : IsRestrictionLocalObservable U (coarseFullBlockMatrixObservable U)

theorem HCPolySupport.isLocalObservable_coarseSigmaStarInvObservable {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) : IsRestrictionLocalObservable U (coarseSigmaStarInvObservable U)

theorem HCPolySupport.isLocalObservable_coarseBObservable {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) : IsRestrictionLocalObservable U (coarseBObservable U)

theorem HCPolySupport.isLocalObservable_coarseSigmaStarInvKappaMeanObservable {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) : IsRestrictionLocalObservable U (coarseSigmaStarInvKappaMeanObservable U)

theorem HCPolySupport.measurable_coarseSigmaStarInvEntryObservable_of_hasMeasurableMuFamily {d : ℕ} {U : Set (Vec d)} (hMu : HasMeasurableMuFamily U) (r c : Fin d) : Measurable (coarseSigmaStarInvEntryObservable U r c)

theorem HCPolySupport.measurable_coarseBEntryObservable_of_hasMeasurableMuFamily {d : ℕ} {U : Set (Vec d)} (hMu : HasMeasurableMuFamily U) (r c : Fin d) : Measurable (coarseBEntryObservable U r c)

theorem HCPolySupport.measurable_coarseSigmaStarInvKappaMeanEntryObservable_of_hasMeasurableMuFamily {d : ℕ} {U : Set (Vec d)} (hMu : HasMeasurableMuFamily U) (r c : Fin d) : Measurable (coarseSigmaStarInvKappaMeanEntryObservable U r c)

theorem HCPolySupport.measurable_coarseUpperRightEntryObservable_of_hasMeasurableMuFamily {d : ℕ} {U : Set (Vec d)} (hMu : HasMeasurableMuFamily U) (r c : Fin d) : Measurable (coarseUpperRightEntryObservable U r c)

theorem HCPolySupport.measurable_coarseLowerLeftEntryObservable_of_hasMeasurableMuFamily {d : ℕ} {U : Set (Vec d)} (hMu : HasMeasurableMuFamily U) (r c : Fin d) : Measurable (coarseLowerLeftEntryObservable U r c)

theorem HCPolySupport.measurable_coarseFullBlockMatrixObservable_of_hasMeasurableMuFamily {d : ℕ} {U : Set (Vec d)} (hMu : HasMeasurableMuFamily U) : Measurable (coarseFullBlockMatrixObservable U)

theorem HCPolySupport.measurable_coarseSigmaStarInvObservable_of_hasMeasurableMuFamily {d : ℕ} {U : Set (Vec d)} (hMu : HasMeasurableMuFamily U) : Measurable (coarseSigmaStarInvObservable U)

theorem HCPolySupport.measurable_coarseBObservable_of_hasMeasurableMuFamily {d : ℕ} {U : Set (Vec d)} (hMu : HasMeasurableMuFamily U) : Measurable (coarseBObservable U)

theorem HCPolySupport.measurable_coarseSigmaStarInvKappaMeanObservable_of_hasMeasurableMuFamily {d : ℕ} {U : Set (Vec d)} (hMu : HasMeasurableMuFamily U) : Measurable (coarseSigmaStarInvKappaMeanObservable U)

noncomputable def HCPolySupport.muLocalObservable {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (hMu : HasMeasurableMuFamily U) (P : BlockVec d) : MeasurableRestrictionLocalObservable d U ℝ

The minimum block energy for P, bundled as a measurable observable depending only on U.

Equations

• HCPolySupport.muLocalObservable hU hMu P = { toFun := fun (a : HCPolySupport.CoeffField d) => HCPolySupport.Mu U P a, measurable_toFun := ⋯, isLocal_toFun := ⋯ }

noncomputable def HCPolySupport.coarseSigmaStarInverseEntryLocalObservable {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (hMu : HasMeasurableMuFamily U) (r c : Fin d) : MeasurableRestrictionLocalObservable d U ℝ

An entry of the lower-right coarse block matrix, bundled as a measurable observable local to U.

Equations

• HCPolySupport.coarseSigmaStarInverseEntryLocalObservable hU hMu r c = { toFun := HCPolySupport.coarseSigmaStarInvEntryObservable U r c, measurable_toFun := ⋯, isLocal_toFun := ⋯ }

noncomputable def HCPolySupport.coarseBEntryLocalObservable {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (hMu : HasMeasurableMuFamily U) (r c : Fin d) : MeasurableRestrictionLocalObservable d U ℝ

An entry of the upper-left coarse block matrix, bundled as a measurable observable local to U.

Equations

• HCPolySupport.coarseBEntryLocalObservable hU hMu r c = { toFun := HCPolySupport.coarseBEntryObservable U r c, measurable_toFun := ⋯, isLocal_toFun := ⋯ }

noncomputable def HCPolySupport.coarseSigmaStarInverseKappaMeanEntryLocalObservable {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (hMu : HasMeasurableMuFamily U) (r c : Fin d) : MeasurableRestrictionLocalObservable d U ℝ

A negated lower-left coarse block entry, bundled as a measurable observable local to U.

Equations

• HCPolySupport.coarseSigmaStarInverseKappaMeanEntryLocalObservable hU hMu r c = { toFun := HCPolySupport.coarseSigmaStarInvKappaMeanEntryObservable U r c, measurable_toFun := ⋯, isLocal_toFun := ⋯ }

noncomputable def HCPolySupport.coarseBlockMatrixLocalObservable {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (hMu : HasMeasurableMuFamily U) : MeasurableRestrictionLocalObservable d U (FullBlockMat d)

The full coarse block matrix, bundled as a measurable observable depending only on U.

Equations

• HCPolySupport.coarseBlockMatrixLocalObservable hU hMu = { toFun := HCPolySupport.coarseFullBlockMatrixObservable U, measurable_toFun := ⋯, isLocal_toFun := ⋯ }

noncomputable def HCPolySupport.coarseSigmaStarInverseLocalObservable {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (hMu : HasMeasurableMuFamily U) : MeasurableRestrictionLocalObservable d U (Mat d)

The lower-right coarse matrix block, bundled as a measurable observable local to U.

Equations

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

noncomputable def HCPolySupport.coarseBLocalObservable {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (hMu : HasMeasurableMuFamily U) : MeasurableRestrictionLocalObservable d U (Mat d)

The upper-left coarse matrix block, bundled as a measurable observable local to U.

Equations

• HCPolySupport.coarseBLocalObservable hU hMu = HCPolySupport.MeasurableLocalObservable.comp (HCPolySupport.coarseBlockMatrixLocalObservable hU hMu) HCPolySupport.fullBlockMatUpperLeft ⋯

noncomputable def HCPolySupport.coarseSigmaStarInverseKappaMeanLocalObservable {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (hMu : HasMeasurableMuFamily U) : MeasurableRestrictionLocalObservable d U (Mat d)

The negated lower-left coarse matrix block, bundled as a measurable observable local to U.

Equations

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