High-contrast homogenization: Provider.Response.RecentDifferenceEnergyIntegrability

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

Integrability of recent optimizer-difference energies

A fixed child energy is controlled by the sum of the nonnegative child responses. The exact recent-energy identity supplies the factor two after the half-energy normalization. Finite adapted means then make the response sum integrable.

theorem HCPolySupport.HighContrast.Response.profilePrimalRecentEnergy_le_two_mul_sum_responseJ {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hst : s ≤ t) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q s t) (a : CoeffSpace d) : (1 / 2 * Book.Ch02.average (adaptedDomainAt hq s w) fun (x : Vec d) => blockVecDot (diagonalWeakChildState hq s w (a.subSkew g hg) p r x - diagonalWeakState hq t (a.subSkew g hg) p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑(a.subSkew g hg) x)) (diagonalWeakChildState hq s w (a.subSkew g hg) p r x - diagonalWeakState hq t (a.subSkew g hg) p r x))) ≤ 2 * ∑ z ∈ alignedIndex q s t, Book.Ch02.responseJ (adaptedDomainAt hq s z) ((a.subSkew g hg).coeffOn (adaptedDomainAt hq s z)) p r

A primal child half-energy is at most twice the sum of the nonnegative child responses.

theorem HCPolySupport.HighContrast.Response.profilePrimalRecentEnergy_integrable {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) (hints : HasFiniteAdaptedMean P q s) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) : have hq := ⋯; have energy := fun (w : Fin d → ℤ) (a : CoeffSpace d) => 1 / 2 * Book.Ch02.average (adaptedDomainAt hq s w) fun (x : Vec d) => blockVecDot (diagonalWeakChildState hq s w (a.subSkew g hg) p r x - diagonalWeakState hq t (a.subSkew g hg) p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑(a.subSkew g hg) x)) (diagonalWeakChildState hq s w (a.subSkew g hg) p r x - diagonalWeakState hq t (a.subSkew g hg) p r x)); ∀ w ∈ alignedIndex q s t, MeasureTheory.Integrable (energy w) P

The literal primal energy is measurable, and finite adapted means imply its integrability on every aligned child.

theorem HCPolySupport.HighContrast.Response.profileAdjointRecentEnergy_le_two_mul_sum_responseJ {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hst : s ≤ t) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q s t) (a : CoeffSpace d) : (1 / 2 * Book.Ch02.average (adaptedDomainAt hq s w) fun (x : Vec d) => blockVecDot (diagonalWeakChildState hq s w (a.subSkew g hg).transpose p r x - diagonalWeakState hq t (a.subSkew g hg).transpose p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑(a.subSkew g hg).transpose x)) (diagonalWeakChildState hq s w (a.subSkew g hg).transpose p r x - diagonalWeakState hq t (a.subSkew g hg).transpose p r x))) ≤ 2 * ∑ z ∈ alignedIndex q s t, Book.Ch02.responseJ (adaptedDomainAt hq s z) ((a.subSkew g hg).transpose.coeffOn (adaptedDomainAt hq s z)) p r

An adjoint child half-energy obeys the same response-sum domination, with the transpose retained on the coefficient carrier.

theorem HCPolySupport.HighContrast.Response.profileAdjointRecentEnergy_integrable {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) (hints : HasFiniteAdaptedMean P q s) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) : have hq := ⋯; have energy := fun (w : Fin d → ℤ) (a : CoeffSpace d) => 1 / 2 * Book.Ch02.average (adaptedDomainAt hq s w) fun (x : Vec d) => blockVecDot (diagonalWeakChildState hq s w (a.subSkew g hg).transpose p r x - diagonalWeakState hq t (a.subSkew g hg).transpose p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑(a.subSkew g hg).transpose x)) (diagonalWeakChildState hq s w (a.subSkew g hg).transpose p r x - diagonalWeakState hq t (a.subSkew g hg).transpose p r x)); ∀ w ∈ alignedIndex q s t, MeasureTheory.Integrable (energy w) P

The independently transformed adjoint responses dominate every adjoint child half-energy by an integrable finite sum.