High-contrast homogenization: Analytic.AffineWeakSolution

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

Affine transport of weak solutions

The divergence-form coefficient, transpose gradient, and inverse-coordinate domain transform together. Both absolute convergence of every weak pairing and its vanishing are preserved in each direction.

theorem HCPolySupport.HighContrast.isWeakSolutionOn_affinePullback_iff {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (a : CoeffField d) (F : Vec d → Vec d) : IsWeakSolutionOn a U F ↔ IsWeakSolutionOn (affineCoefficient L hL a) (matImage L⁻¹ U) fun (y : Vec d) => matVecMul (matTranspose L) (F (matVecMul L y))

Weak solutions, including integrability of every test pairing, are equivalent before and after an invertible divergence-form pullback.