High-contrast homogenization: Provider.Quenched.CoarseExcessMeasurability

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Measurability of the normalized coarse-block excess

The rows of the annealed-to-quenched endgame (e.random.quenched.row) are built from the normalized excess of the coarse response over the homogenized block, maximized over the standard cells centered inside an outer cube. On the coefficient space the coarse response is positive semidefinite, so its excess is the positive part of the relative size already carried by the coarse-block measurability engine. This file records that identity and the two measurability statements it yields.

theorem HCPolySupport.HighContrast.Quenched.blockExcess_eq_max_blockSize_sub_one {d : ℕ} {H F : BlockMat d} (hH : IsSymmetricBlockMat H) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) (hHps : Matrix.PosSemidef (toFullBlockMat H)) : blockExcess H F = max (blockSize H F - 1) 0

On a positive semidefinite block the normalized excess is the positive part of the relative size.

theorem HCPolySupport.HighContrast.Quenched.measurable_blockExcess_coarseBlock {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hUvol : 0 < (MeasureTheory.volume U).toReal) {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) : Measurable fun (a : CoeffSpace d) => blockExcess (coarseBlock U a) F

The normalized excess of the coarse response on a bounded open convex cell is measurable.