High-contrast homogenization: Provider.Response.DiagonalWeakNormRecentEnergy

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

The optimizer-difference energy on recent cells

The parent optimizer is an admissible child solution. Expanding the child functional around its canonical maximizer identifies the block energy of the optimizer difference with four times the corresponding response deficit.

theorem HCPolySupport.HighContrast.Response.responseIntegrand_diagonalWeakOptimizer_integrableOn {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) (p r : Vec d) : MeasureTheory.IntegrableOn (Book.Ch02.responseIntegrand (adaptedDomain hq t) (a.coeffOn (adaptedDomain hq t)) p r (diagonalWeakOptimizer hq t a p r)) (adaptedCell q t) MeasureTheory.volume

The response integrand of the canonical parent optimizer is integrable on the parent cell, so its averages may be recombined across the aligned partition.

theorem HCPolySupport.HighContrast.Response.diagonalWeak_child_difference_energy_eq {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (a : CoeffSpace d) (p r : Vec d) : ∃ (u : Book.Ch02.Solution (adaptedDomainAt hq k w) (a.coeffOn (adaptedDomainAt hq k w))), u.toH1.grad = (diagonalWeakOptimizer hq t a p r).toH1.grad ∧ (Book.Ch02.average (adaptedDomainAt hq k w) fun (x : Vec d) => blockVecDot (diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑a x)) (diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x))) = 4 * (Book.Ch02.responseJ (adaptedDomainAt hq k w) (a.coeffOn (adaptedDomainAt hq k w)) p r - Book.Ch02.responseValue (adaptedDomainAt hq k w) (a.coeffOn (adaptedDomainAt hq k w)) p r u)

On one aligned child, the optimizer-difference block energy is four times the child response deficit of the restricted parent optimizer.