High-contrast homogenization: Provider.Regularity.AffineTransfer

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

Affine transfer for large-scale regularity

This file collects the elementary interfaces that move between physical coordinates and the scalar coordinates determined by the symmetric square root of the homogenized coefficient. The results compose the constant-skew gauge with affine covariance of weak gradients, weak solutions, normalized norms, and fluxes.

The geometric results identify the pullback of an adapted ellipsoid exactly and compare it with centered Euclidean cubes under explicit scale inequalities.

theorem HCPolySupport.HighContrast.vecDot_matSqrt_mulVec {d : ℕ} (S : Mat d) (e y : Vec d) : vecDot e (matVecMul (matSqrt S) y) = vecDot (matVecMul (matSqrt S) e) y

The symmetric square root may be moved between the two entries of the Euclidean pairing.

theorem HCPolySupport.HighContrast.euclideanNorm_matSqrt_eq_sqrt_vecDot {d : ℕ} {S : Mat d} (hS : Matrix.PosSemidef S) (e : Vec d) : euclideanNorm (matVecMul (matSqrt S) e) = √(vecDot e (matVecMul S e))

The Euclidean norm of a square-root-transformed vector is the square root of its quadratic energy.

theorem HCPolySupport.HighContrast.matImage_matSqrt_inv_ellipsoid_eq {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (r : ℝ) : matImage (matSqrt (symmPart abar))⁻¹ (ellipsoid abar r) = {y : Vec d | vecNormSq y ≤ specBound (symmPart abar)⁻¹ * r ^ 2}

Pulling an adapted ellipsoid back by the symmetric square root gives its exact Euclidean quadratic sublevel set.

theorem HCPolySupport.HighContrast.isWeakSolutionOn_skewCentered_matSqrtPullback_iff {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} (hU : IsOpen U) (a : CoeffField d) {u : Vec d → ℝ} {Du : Vec d → Vec d} (hu : MemScalarL2 U u) (hDu : ∀ (i : Fin d), MemScalarL2 U fun (x : Vec d) => Du x i) (hweak : HasWeakGradientOn U u Du) : IsWeakSolutionOn a U Du ↔ IsWeakSolutionOn (affineCoefficient (matSqrt (symmPart abar)) ⋯ fun (x : Vec d) => a x - skewPart abar) (matImage (matSqrt (symmPart abar))⁻¹ U) fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (Du (matVecMul (matSqrt (symmPart abar)) y))

A physical weak solution is equivalent to the square-root pullback of its skew-centered weak equation. The Sobolev data are explicit because the skew gauge acts only on actual weak gradients.

theorem HCPolySupport.HighContrast.matSqrt_gradient_difference_affinePullback {d : ℕ} {abar : Mat d} (F G : Vec d → Vec d) : (fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (F (matVecMul (matSqrt (symmPart abar)) y) - G (matVecMul (matSqrt (symmPart abar)) y))) = fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (F (matVecMul (matSqrt (symmPart abar)) y)) - matVecMul (matSqrt (symmPart abar)) (G (matVecMul (matSqrt (symmPart abar)) y))

A gradient difference in physical coordinates becomes the difference of the two square-root-transformed gradients.

theorem HCPolySupport.HighContrast.skewCenteredFlux_affinePullback {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (a : CoeffField d) (F G : Vec d → Vec d) : (fun (y : Vec d) => matVecMul (affineCoefficient (matSqrt (symmPart abar)) ⋯ (fun (x : Vec d) => a x - skewPart abar) y) (matVecMul (matSqrt (symmPart abar)) (F (matVecMul (matSqrt (symmPart abar)) y))) - matVecMul (matSqrt (symmPart abar)) (G (matVecMul (matSqrt (symmPart abar)) y))) = fun (y : Vec d) => matVecMul (matSqrt (symmPart abar))⁻¹ (matVecMul (a (matVecMul (matSqrt (symmPart abar)) y) - skewPart abar) (F (matVecMul (matSqrt (symmPart abar)) y)) - matVecMul (symmPart abar) (G (matVecMul (matSqrt (symmPart abar)) y)))

The normalized flux difference is exactly the inverse-square-root image of the physical skew-centered flux difference.