High-contrast homogenization: Provider.Response.SubcellDoubledResponse

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

Doubled response fields on aligned child cells

The optimizer on an adapted parent cell restricts to every aligned child. Subtracting the child's canonical optimizer therefore gives a doubled response field on the child for the actual coefficient-space representative.

theorem HCPolySupport.HighContrast.Response.isDoubledResponseField_diagonalWeakState_sub_childState {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) : Book.Ch02.IsDoubledResponseField (adaptedDomainAt hq k w) (a.coeffOn (adaptedDomainAt hq k w)) { potential := fun (x : Vec d) => (diagonalWeakState hq t a p r x - diagonalWeakChildState hq k w a p r x).1, flux := fun (x : Vec d) => (diagonalWeakState hq t a p r x - diagonalWeakChildState hq k w a p r x).2 }

The parent optimizer state minus the child optimizer state belongs to the doubled response space on the child cell.