High-contrast homogenization: Analytic.AffineH10

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

Affine transport of zero-boundary Sobolev functions

Composition with an invertible matrix transports compactly supported smooth approximants, including their scalar and gradient convergence. This gives the corresponding transport of affine Dirichlet data.

theorem HCPolySupport.HighContrast.exists_h10Function_affinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (u : H10Function U) : ∃ (uL : H10Function (matImage L⁻¹ U)), (uL.toFun = fun (y : Vec d) => u.toFun (matVecMul L y)) ∧ uL.grad = fun (y : Vec d) => matVecMul (matTranspose L) (u.grad (matVecMul L y))

An invertible linear pullback sends an actual H¹₀ witness to the inverse-image domain with the transpose-transformed gradient.

theorem HCPolySupport.HighContrast.exists_memAffineH10_affinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (g₀ h : H1Function U) (haff : MemAffineH10 U g₀ h) : ∃ (g₀L : H1Function (matImage L⁻¹ U)) (hL : H1Function (matImage L⁻¹ U)), (g₀L.toFun = fun (y : Vec d) => g₀.toFun (matVecMul L y)) ∧ (g₀L.grad = fun (y : Vec d) => matVecMul (matTranspose L) (g₀.grad (matVecMul L y))) ∧ (hL.toFun = fun (y : Vec d) => h.toFun (matVecMul L y)) ∧ (hL.grad = fun (y : Vec d) => matVecMul (matTranspose L) (h.grad (matVecMul L y))) ∧ MemAffineH10 (matImage L⁻¹ U) g₀L hL

Affine Dirichlet membership transports with constructed pullbacks of both the boundary datum and the solution.