High-contrast homogenization: Provider.Response.AdaptedFiveTermProfile

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

Physical response defects for the adapted cutoff rows

The energy defect in a cutoff row is one half of the doubled energy of the child optimizer minus the parent optimizer. Its annealed normalized average is twice the corresponding response defect. Aligned-cell stationarity identifies the child expectations directly on the physical domains.

The primal row energy

theorem HCPolySupport.HighContrast.Response.profilePrimalRecentEnergyDefect {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) (hintt : HasFiniteAdaptedMean P q t) (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)); have defect := fun (w : Fin d → ℤ) => ∫ (a : CoeffSpace d), energy w a ∂P; (∀ w ∈ alignedIndex q s t, MeasureTheory.Integrable (energy w) P) → (∀ w ∈ alignedIndex q s t, 0 ≤ defect w) ∧ avsum (alignedIndex q s t) defect = 2 * profilePrimalResponseDefect P hq g hg s t p r

The actual primal child--parent half doubled-energy is nonnegative on each aligned cell, and its normalized annealed average is twice the physical primal response defect.

The adjoint row energy

theorem HCPolySupport.HighContrast.Response.profileAdjointRecentEnergyDefect {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) (hintt : HasFiniteAdaptedMean P q t) (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)); have defect := fun (w : Fin d → ℤ) => ∫ (a : CoeffSpace d), energy w a ∂P; (∀ w ∈ alignedIndex q s t, MeasureTheory.Integrable (energy w) P) → (∀ w ∈ alignedIndex q s t, 0 ≤ defect w) ∧ avsum (alignedIndex q s t) defect = 2 * profileAdjointResponseDefect P hq g hg s t p r

The coefficient-transpose row has the independently transported physical half doubled-energy and the adjoint response defect.