High-contrast homogenization: Provider.Response.ProfileSkewMeasurability

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

Measurability after constant-skew recentering

The response energy has the same load covariance as the response functional. The resulting identities transport the profile measurability inputs to a constant-skew recentered coefficient sample without any invariance assumption on its law.

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

The terminal spatial average of the primal optimizer state is almost everywhere measurable.

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

The terminal spatial average of the adjoint optimizer state is almost everywhere measurable.

theorem HCPolySupport.HighContrast.Response.blockCellAverage_diagonalWeakState_subSkew {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) : blockCellAverage (adaptedCell q t) (diagonalWeakState hq t (a.subSkew g hg) p r) = have Y := blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p (r - matVecMul g p)); (Y.1, Y.2 - matVecMul g Y.1)

Constant-skew recentering shears the averaged primal state after the load correction.

theorem HCPolySupport.HighContrast.Response.aemeasurable_blockCellAverage_diagonalWeakState_subSkew {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) : AEMeasurable (fun (a : CoeffSpace d) => blockCellAverage (adaptedCell q t) (diagonalWeakState hq t (a.subSkew g hg) p r)) P

The terminal spatial average remains almost everywhere measurable after constant-skew recentering.

theorem HCPolySupport.HighContrast.Response.aemeasurable_blockCellAverage_diagonalWeakAdjointState_subSkew {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) : AEMeasurable (fun (a : CoeffSpace d) => blockCellAverage (adaptedCell q t) (diagonalWeakAdjointState hq t (a.subSkew g hg) p r)) P

The terminal adjoint average remains almost everywhere measurable after constant-skew recentering.

theorem HCPolySupport.HighContrast.Response.diagonalWeakEnergy_subSkew {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) : diagonalWeakEnergy hq t (a.subSkew g hg) p r = diagonalWeakEnergy hq t a p (r - matVecMul g p)

The primal terminal energy transforms by subtracting the skew action from the second load.

theorem HCPolySupport.HighContrast.Response.diagonalWeakAdjointEnergy_subSkew {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) : diagonalWeakAdjointEnergy hq t (a.subSkew g hg) p r = diagonalWeakAdjointEnergy hq t a p (r + matVecMul g p)

The adjoint terminal energy transforms with the opposite load shift.

theorem HCPolySupport.HighContrast.Response.aemeasurable_diagonalWeakCellSum_subSkew {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) (s : ℝ) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (g : Mat d) (hg : IsSkewMat g) : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakCellSum q t H s (skewBlockCongr g E) (a.subSkew g hg)) P

The recentered recent cell sum is almost everywhere measurable.

theorem HCPolySupport.HighContrast.Response.aemeasurable_diagonalWeakMaximum_subSkew {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {rho : ℝ} {q : Mat d} (hq : Matrix.PosDef q) {t : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (g : Mat d) (hg : IsSkewMat g) : AEMeasurable (fun (a : CoeffSpace d) => diagonalWeakMaximum rho q t (skewBlockCongr g E) (a.subSkew g hg)) P

The recentered all-scale maximum is almost everywhere measurable.

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

The recentered primal terminal energy is almost everywhere measurable at the correctly shifted load.

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

The recentered adjoint terminal energy is almost everywhere measurable at the correctly shifted load.