High-contrast homogenization: Analytic.AffineH1a0Pairing

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

Affine transport for coefficient-weighted zero-trace data

The inverse-image convention for an invertible linear change of variables transports measurable gradient pairs, weak gradients with locally integrable components, and the unnormalized symmetric energy with its exact Jacobian.

theorem HCPolySupport.HighContrast.lintegral_affinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (f : Vec d → ENNReal) : ∫⁻ (y : Vec d) in matImage L⁻¹ U, f (matVecMul L y) = ENNReal.ofReal |Matrix.det L|⁻¹ * ∫⁻ (x : Vec d) in U, f x

An unnormalized nonnegative integral on an affine pullback carries the inverse-determinant Jacobian, without a measurability assumption on the integrand.

theorem HCPolySupport.HighContrast.isMeasurableGradientPair_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} (hpair : IsMeasurableGradientPair (MeasureTheory.volume.restrict U) u Du) : IsMeasurableGradientPair (MeasureTheory.volume.restrict (matImage L⁻¹ U)) (fun (y : Vec d) => u (matVecMul L y)) fun (y : Vec d) => matVecMul (matTranspose L) (Du (matVecMul L y))

Measurability of a function-gradient pair is preserved by the affine pullback and the transpose action on its gradient.

theorem HCPolySupport.HighContrast.hasWeakGradientOn_affinePullback_of_integrable {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 : MeasureTheory.IntegrableOn u U MeasureTheory.volume) (hDu : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => Du x i) U MeasureTheory.volume) (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 affine pullback preserves a weak gradient when the function and every gradient component are integrable on the source domain.

theorem HCPolySupport.HighContrast.sEnergyOn_affinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (b : CoeffField d) (F : Vec d → Vec d) : (sEnergyOn (affineCoefficient L hL b) (matImage L⁻¹ U) fun (y : Vec d) => matVecMul (matTranspose L) (F (matVecMul L y))) = ENNReal.ofReal |Matrix.det L|⁻¹ * sEnergyOn b U F

The symmetric energy of a transpose-transformed field has the exact inverse-determinant Jacobian on the affine pullback domain.

theorem HCPolySupport.HighContrast.h1sNormSqOn_affinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (b : CoeffField d) (u : Vec d → ℝ) (Du : Vec d → Vec d) : (h1sNormSqOn (affineCoefficient L hL b) (matImage L⁻¹ U) (fun (y : Vec d) => u (matVecMul L y)) fun (y : Vec d) => matVecMul (matTranspose L) (Du (matVecMul L y))) = (ENNReal.ofReal |Matrix.det L|⁻¹ * ∫⁻ (x : Vec d) in U, ENNReal.ofReal |u x|) ^ 2 + ENNReal.ofReal |Matrix.det L|⁻¹ * sEnergyOn b U Du

The full symmetric Sobolev quantity obeys the sharp two-term Jacobian formula under affine pullback.

theorem HCPolySupport.HighContrast.h1sNormSqOn_affinePullback_le {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) (b : CoeffField d) (u : Vec d → ℝ) (Du : Vec d → Vec d) : (h1sNormSqOn (affineCoefficient L hL b) (matImage L⁻¹ U) (fun (y : Vec d) => u (matVecMul L y)) fun (y : Vec d) => matVecMul (matTranspose L) (Du (matVecMul L y))) ≤ max (ENNReal.ofReal |Matrix.det L|⁻¹ ^ 2) (ENNReal.ofReal |Matrix.det L|⁻¹) * h1sNormSqOn b U u Du

A single finite determinant factor controls both terms of the transported coefficient-weighted Sobolev quantity.