High-contrast homogenization: Analytic.AffineH1a0Skew #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Skew-flux pairings under affine transport #
The divergence-form pullback preserves the skew-flux integrand under the dual actions on gradients and fluxes. The determinant Jacobian then controls the associated coefficient-weighted dual norm.
theorem
HCPolySupport.HighContrast.skewFluxPairing_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)
{f : Vec d → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
:
skewFluxPairing (affineCoefficient L hL b) (matImage L⁻¹ U)
(fun (y : Vec d) => matVecMul (matTranspose L) (F (matVecMul L y))) f = ENNReal.ofReal |Matrix.det L|⁻¹ * skewFluxPairing b U F fun (x : Vec d) => f (matVecMul L⁻¹ x)
The skew-flux pairing has the exact inverse-determinant Jacobian under affine pullback.
theorem
HCPolySupport.HighContrast.h1sNormSqOn_affinePushforward_le
{d : ℕ}
{L : Mat d}
(hL : IsUnit (Matrix.det L))
{U : Set (Vec d)}
(hU : MeasurableSet U)
(b : CoeffField d)
(f : Vec d → ℝ)
(Df : Vec d → Vec d)
:
(h1sNormSqOn b U (fun (x : Vec d) => f (matVecMul L⁻¹ x)) fun (x : Vec d) =>
matVecMul (matTranspose L⁻¹) (Df (matVecMul L⁻¹ x))) ≤ max (ENNReal.ofReal |Matrix.det L| ^ 2) (ENNReal.ofReal |Matrix.det L|) * h1sNormSqOn (affineCoefficient L hL b) (matImage L⁻¹ U) f Df
Pulling a field from the affine domain back to the original domain costs the maximum of the value and energy Jacobian factors.
theorem
HCPolySupport.HighContrast.skewFluxDualNorm_affinePullback_le
{d : ℕ}
{L : Mat d}
(hL : IsUnit (Matrix.det L))
{U : Set (Vec d)}
(hU : MeasurableSet U)
(b : CoeffField d)
(F : Vec d → Vec d)
:
(skewFluxDualNorm (affineCoefficient L hL b) (matImage L⁻¹ U) fun (y : Vec d) =>
matVecMul (matTranspose L) (F (matVecMul L y))) ≤ ENNReal.ofReal (|Matrix.det L|⁻¹ * max |Matrix.det L| 1) * skewFluxDualNorm b U F
The affine pullback of a skew flux is controlled in its weighted dual norm by a finite determinant factor.