High-contrast homogenization: Provider.Response.ProfileEnergyMeasurability

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

Measurability of terminal optimizer energies

The squared canonical optimizer energy is a fixed quadratic reading of the terminal coarse block. Entrywise coarse-block measurability therefore gives measurability of both the primal and coefficient-transpose energies.

theorem HCPolySupport.HighContrast.Response.aemeasurable_blockQuadratic_coarseBlock {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hU : HasMeasurableCoarseBlock P U) (X : BlockVec d) : AEMeasurable (fun (a : CoeffSpace d) => blockVecDot X (blockMatVecMul (coarseBlock U a) X)) P

A fixed quadratic reading of a random coarse block is almost everywhere measurable.

theorem HCPolySupport.HighContrast.Response.sq_diagonalWeakEnergy_eq_coarseBlock {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : diagonalWeakEnergy hq t a p r ^ 2 = blockVecDot (-p, r) (blockMatVecMul (coarseBlock (adaptedCell q t) a) (-p, r)) - 2 * vecDot p r

The primal optimizer energy squared is its terminal block quadratic form minus the load product.

theorem HCPolySupport.HighContrast.Response.sq_diagonalWeakAdjointEnergy_eq_coarseBlock {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : diagonalWeakAdjointEnergy hq t a p r ^ 2 = blockVecDot (p, r) (blockMatVecMul (coarseBlock (adaptedCell q t) a) (p, r)) - 2 * vecDot p r

The adjoint optimizer energy squared is the plus-load quadratic reading of the original terminal block.

theorem HCPolySupport.HighContrast.Response.aemeasurable_diagonalWeakEnergy {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (p r : Vec d) : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakEnergy hq t a p r) P

The primal terminal optimizer energy is almost everywhere measurable.

theorem HCPolySupport.HighContrast.Response.aemeasurable_diagonalWeakAdjointEnergy {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (p r : Vec d) : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakAdjointEnergy hq t a p r) P

The adjoint terminal optimizer energy is almost everywhere measurable.