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

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 Mu block quadratic form X ↦ (½) ⟨X, A X⟩ is measurable in the coefficient field via the unfolded 2d × 2d block-matrix representation. This is the measurable bridge from full-block measurability to the scalar Mu energy used by all downstream operator/recovery machinery.

Consumed by: every FixedCompetitorEnergyMeasurability/*.lean file (Measurability, LipschitzBounds, Integrals, BlockEnergyAverage, MuObservable), which in turn feeds the AEE assembly and ultimately Theorems/Mu.lean :: aemeasurable_Mu_cubeSet and Theorems/CanonicalSolutions.lean :: aestronglyMeasurable_canonicalMuHilbertMinimizer_cubeSet.

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

theorem HCPolySupport.measurable_half_blockVecDot_blockMatVecMul_of_measurable_fullBlockMat {α : Type u_1} [MeasurableSpace α] {d : ℕ} {f : α → FullBlockMat d} (hf : Measurable f) (X : BlockVec d) : Measurable fun (a : α) => 1 / 2 * blockVecDot X (blockMatVecMul (ofFullBlockMat (f a)) X)

Measurability of the quadratic form X ↦ (1/2) X · (A X) when the block matrix observable is supplied in unfolded 2d × 2d coordinates.

theorem HCPolySupport.measurable_coarseSigmaStarInvEntryObservable_of_measurable_Mu_pureFlux {d : ℕ} {U : Set (Vec d)} (hDiag : ∀ (i : Fin d), Measurable fun (a : CoeffField d) => Mu U (0, Pi.single i 1) a) (hPair : ∀ (i j : Fin d), Measurable fun (a : CoeffField d) => Mu U ((0, Pi.single i 1) + (0, Pi.single j 1)) a) (r c : Fin d) : Measurable (coarseSigmaStarInvEntryObservable U r c)

The lower-right coarse entry is measurable once the pure-flux Mu coordinate slices are measurable.

theorem HCPolySupport.measurable_coarseBEntryObservable_of_measurable_Mu_pureGradient {d : ℕ} {U : Set (Vec d)} (hDiag : ∀ (i : Fin d), Measurable fun (a : CoeffField d) => Mu U (Pi.single i 1, 0) a) (hPair : ∀ (i j : Fin d), Measurable fun (a : CoeffField d) => Mu U ((Pi.single i 1, 0) + (Pi.single j 1, 0)) a) (r c : Fin d) : Measurable (coarseBEntryObservable U r c)

The upper-left coarse entry is measurable once the pure-gradient Mu coordinate slices are measurable.

theorem HCPolySupport.measurable_coarseSigmaStarInvKappaMeanEntryObservable_of_measurable_Mu_mixed {d : ℕ} {U : Set (Vec d)} (hFlux : ∀ (i : Fin d), Measurable fun (a : CoeffField d) => Mu U (0, Pi.single i 1) a) (hGrad : ∀ (i : Fin d), Measurable fun (a : CoeffField d) => Mu U (Pi.single i 1, 0) a) (hMixed : ∀ (i j : Fin d), Measurable fun (a : CoeffField d) => Mu U ((Pi.single i 1, 0) + (0, Pi.single j 1)) a) (r c : Fin d) : Measurable (coarseSigmaStarInvKappaMeanEntryObservable U r c)

The mixed mean entry is measurable once the mixed and pure coordinate Mu slices are measurable.

theorem HCPolySupport.measurable_coarseUpperRightEntryObservable_of_measurable_Mu_mixed {d : ℕ} {U : Set (Vec d)} (hFlux : ∀ (i : Fin d), Measurable fun (a : CoeffField d) => Mu U (0, Pi.single i 1) a) (hGrad : ∀ (i : Fin d), Measurable fun (a : CoeffField d) => Mu U (Pi.single i 1, 0) a) (hMixed : ∀ (i j : Fin d), Measurable fun (a : CoeffField d) => Mu U ((Pi.single i 1, 0) + (0, Pi.single j 1)) a) (r c : Fin d) : Measurable (coarseUpperRightEntryObservable U r c)

The upper-right coarse entry is measurable once the mixed and pure coordinate Mu slices are measurable.

theorem HCPolySupport.measurable_coarseLowerLeftEntryObservable_of_measurable_Mu_mixed {d : ℕ} {U : Set (Vec d)} (hFlux : ∀ (i : Fin d), Measurable fun (a : CoeffField d) => Mu U (0, Pi.single i 1) a) (hGrad : ∀ (i : Fin d), Measurable fun (a : CoeffField d) => Mu U (Pi.single i 1, 0) a) (hMixed : ∀ (i j : Fin d), Measurable fun (a : CoeffField d) => Mu U ((Pi.single i 1, 0) + (0, Pi.single j 1)) a) (r c : Fin d) : Measurable (coarseLowerLeftEntryObservable U r c)

The lower-left coarse entry is measurable once the mixed and pure coordinate Mu slices are measurable.

theorem HCPolySupport.measurable_coarseFullBlockMatrixObservable_of_measurable_coordinate_Mu {d : ℕ} {U : Set (Vec d)} (hFlux : ∀ (i : Fin d), Measurable fun (a : CoeffField d) => Mu U (0, Pi.single i 1) a) (hFluxPair : ∀ (i j : Fin d), Measurable fun (a : CoeffField d) => Mu U ((0, Pi.single i 1) + (0, Pi.single j 1)) a) (hGrad : ∀ (i : Fin d), Measurable fun (a : CoeffField d) => Mu U (Pi.single i 1, 0) a) (hGradPair : ∀ (i j : Fin d), Measurable fun (a : CoeffField d) => Mu U ((Pi.single i 1, 0) + (Pi.single j 1, 0)) a) (hMixed : ∀ (i j : Fin d), Measurable fun (a : CoeffField d) => Mu U ((Pi.single i 1, 0) + (0, Pi.single j 1)) a) : Measurable (coarseFullBlockMatrixObservable U)

Measurability of the full coarse block matrix from the finite coordinate Mu slices that generate its entries.

theorem HCPolySupport.hasMeasurableMuFamily_of_measurable_coarseFullBlockMatrixObservable_of_hasQuadraticMu {d : ℕ} {U : Set (Vec d)} (hBlockMeas : Measurable (coarseFullBlockMatrixObservable U)) (hquad : ∀ (a : CoeffField d), HasQuadraticMu U a) : HasMeasurableMuFamily U

Once the coarse block matrix is measurable and Mu is known to be quadratic pointwise, the full ambient Mu family is measurable.

theorem HCPolySupport.hasMeasurableMuFamily_of_measurable_coordinate_Mu_of_hasQuadraticMu {d : ℕ} {U : Set (Vec d)} (hFlux : ∀ (i : Fin d), Measurable fun (a : CoeffField d) => Mu U (0, Pi.single i 1) a) (hFluxPair : ∀ (i j : Fin d), Measurable fun (a : CoeffField d) => Mu U ((0, Pi.single i 1) + (0, Pi.single j 1)) a) (hGrad : ∀ (i : Fin d), Measurable fun (a : CoeffField d) => Mu U (Pi.single i 1, 0) a) (hGradPair : ∀ (i j : Fin d), Measurable fun (a : CoeffField d) => Mu U ((Pi.single i 1, 0) + (Pi.single j 1, 0)) a) (hMixed : ∀ (i j : Fin d), Measurable fun (a : CoeffField d) => Mu U ((Pi.single i 1, 0) + (0, Pi.single j 1)) a) (hquad : ∀ (a : CoeffField d), HasQuadraticMu U a) : HasMeasurableMuFamily U

Finite coordinate Mu measurability plus pointwise quadraticity upgrades to the full ambient Mu family.