High-contrast homogenization: Provider.Response.DiagonalWeakOptimizerStationarity

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

Stationarity of aligned optimizer averages

Aligned and centered optimizer averages differ only by sample translation. Stationarity and the mean-one cutoff therefore cancel their weighted means.

theorem HCPolySupport.HighContrast.Response.exists_blockCellAverage_diagonalWeakChildState_subSkew_eq_translateCoeff {d : ℕ} {l s : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) (hls : l ≤ s) (w : Fin d → ℤ) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) : ∃ (z : Fin d → ℤ), (adaptedCellCenter q s w = fun (i : Fin d) => ↑(z i)) ∧ ∀ (a : CoeffSpace d), blockCellAverage (adaptedCellAt q s w) (diagonalWeakChildState ⋯ s w (a.subSkew g hg) p r) = blockCellAverage (adaptedCell q s) (diagonalWeakState ⋯ s ((translateCoeff z a).subSkew g hg) p r)

Constant-skew recentering preserves aligned translation covariance.

theorem HCPolySupport.HighContrast.Response.exists_blockCellAverage_diagonalWeakChildState_adjointSubSkew_eq_translateCoeff {d : ℕ} {l s : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) (hls : l ≤ s) (w : Fin d → ℤ) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) : ∃ (z : Fin d → ℤ), (adaptedCellCenter q s w = fun (i : Fin d) => ↑(z i)) ∧ ∀ (a : CoeffSpace d), blockCellAverage (adaptedCellAt q s w) (diagonalWeakChildState ⋯ s w (a.subSkew g hg).transpose p r) = blockCellAverage (adaptedCell q s) (diagonalWeakState ⋯ s ((translateCoeff z a).subSkew g hg).transpose p r)

The recentered adjoint optimizer has its own aligned covariance.

theorem HCPolySupport.HighContrast.Response.avsum_one_sub_cutoffAverage_mul_integral_childState_subSkew_eq_zero {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l s t : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) (hls : l ≤ s) (hst : s ≤ t) (hint : HasFiniteAdaptedMean P q s) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) (α : BlockCoord d) : (avsum (alignedIndex q s t) fun (w : Fin d → ℤ) => (1 - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q ⋯ t)) * ∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (diagonalWeakChildState ⋯ s w (a.subSkew g hg) p r)) α ∂P) = 0

The same cancellation holds for the literal constant-skew primal state.

theorem HCPolySupport.HighContrast.Response.avsum_one_sub_cutoffAverage_mul_integral_childState_adjointSubSkew_eq_zero {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l s t : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) (hls : l ≤ s) (hst : s ≤ t) (hint : HasFiniteAdaptedMean P q s) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) (α : BlockCoord d) : (avsum (alignedIndex q s t) fun (w : Fin d → ℤ) => (1 - volumeAverage (adaptedCellAt q s w) (adaptedPreYoungCutoff q ⋯ t)) * ∫ (a : CoeffSpace d), toFullBlockVec (blockCellAverage (adaptedCellAt q s w) (diagonalWeakChildState ⋯ s w (a.subSkew g hg).transpose p r)) α ∂P) = 0

The literal constant-skew adjoint state has the independent cancellation.