High-contrast homogenization: Analytic.AffineWeakGradient

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

Affine transport of weak gradients

An invertible matrix pulls a scalar Sobolev function back by composition and transports its weak gradient by the transpose matrix. This file records the weak-gradient and H¹ parts of that change of variables.

theorem HCPolySupport.HighContrast.measurableSet_affinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) : MeasurableSet (matImage L⁻¹ U)

The inverse image domain of a measurable set under an invertible matrix is measurable.

theorem HCPolySupport.HighContrast.map_restrict_volume_affinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) : MeasureTheory.Measure.map (matVecMul L) (MeasureTheory.volume.restrict (matImage L⁻¹ U)) = ENNReal.ofReal |Matrix.det L|⁻¹ • MeasureTheory.volume.restrict U

Restricted volume on an affine pullback has the inverse-determinant Jacobian.

theorem HCPolySupport.HighContrast.memL2On_affinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) {f : Vec d → ℝ} (hf : MemL2On U f) : MemL2On (matImage L⁻¹ U) fun (y : Vec d) => f (matVecMul L y)

Pullback by an invertible matrix preserves local square integrability.

theorem HCPolySupport.HighContrast.smoothGrad_comp_matVecMul {d : ℕ} (L : Mat d) {f : Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (x : Vec d) : smoothGrad (fun (y : Vec d) => f (matVecMul L y)) x = matVecMul (matTranspose L) (smoothGrad f (matVecMul L x))

The smooth gradient obeys the transpose chain rule under a matrix map.

theorem HCPolySupport.HighContrast.isLocalTest_comp_matVecMul_inv {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} {f : Vec d → ℝ} (hf : IsLocalTest (matImage L⁻¹ U) f) : IsLocalTest U fun (x : Vec d) => f (matVecMul L⁻¹ x)

A local test pulls back from the inverse-image domain to the original domain.

theorem HCPolySupport.HighContrast.isLocalTest_comp_matVecMul {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} {f : Vec d → ℝ} (hf : IsLocalTest U f) : IsLocalTest (matImage L⁻¹ U) fun (y : Vec d) => f (matVecMul L y)

A local test on the original domain pulls back to the inverse-image domain.

theorem HCPolySupport.HighContrast.hasWeakGradientOn_affinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) {u : Vec d → ℝ} {Du : Vec d → Vec d} (hu : MemL2On U u) (hDu : GradMemL2On U Du) (hweak : HasWeakGradientOn U u Du) : HasWeakGradientOn (matImage L⁻¹ U) (fun (y : Vec d) => u (matVecMul L y)) fun (y : Vec d) => matVecMul (matTranspose L) (Du (matVecMul L y))

An L² weak-gradient pair pulls back along every invertible matrix.

theorem HCPolySupport.HighContrast.exists_h1Function_affinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (u : H1Function U) : ∃ (uL : H1Function (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))

Every H¹ witness has the exact transpose-gradient affine pullback.