High-contrast homogenization: Analytic.SkewGauge

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

Constant-skew gauge covariance

A constant skew matrix sends a Sobolev gradient to a solenoidal field. This makes its pairing with every compactly supported smooth gradient vanish and shows that adding it to a coefficient field does not change the weak equation. The same shift leaves every quantity built from the symmetric coefficient part unchanged. The final identities record the already available covariance of the variational response under the matching shear of its loads.

theorem HCPolySupport.HighContrast.weakPairing_add_const {d : ℕ} (b : CoeffField d) (k : Mat d) (F : Vec d → Vec d) (φ : Vec d → ℝ) : (fun (x : Vec d) => vecDot (smoothGrad φ x) (matVecMul (b x + k) (F x))) = fun (x : Vec d) => vecDot (smoothGrad φ x) (matVecMul (b x) (F x)) + vecDot (smoothGrad φ x) (matVecMul k (F x))

The weak pairing for a coefficient shifted by a constant matrix splits into the original pairing and the constant-matrix pairing.

theorem HCPolySupport.HighContrast.integrableOn_and_integral_smoothGrad_skew_weakGradient_eq_zero {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {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) (k : Mat d) (hk : IsSkewMat k) {φ : Vec d → ℝ} (hφ : IsLocalTest U φ) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (smoothGrad φ x) (matVecMul k (Du x))) U MeasureTheory.volume ∧ ∫ (x : Vec d) in U, vecDot (smoothGrad φ x) (matVecMul k (Du x)) = 0

A constant skew matrix paired with a weak gradient and a smooth test gradient is absolutely integrable and has integral zero.

theorem HCPolySupport.HighContrast.isWeakSolutionOn_add_constSkew_iff {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) (b : 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) (k : Mat d) (hk : IsSkewMat k) : IsWeakSolutionOn (fun (x : Vec d) => b x + k) U Du ↔ IsWeakSolutionOn b U Du

Adding a constant skew matrix to a coefficient field leaves its weak solution class unchanged on Sobolev gradients.

theorem HCPolySupport.HighContrast.weightedGradNorm_add_constSkew {d : ℕ} (b : CoeffField d) (U : Set (Vec d)) (F : Vec d → Vec d) (k : Mat d) (hk : IsSkewMat k) : weightedGradNorm (fun (x : Vec d) => b x + k) U F = weightedGradNorm b U F

Adding a constant skew matrix does not change the weighted gradient norm.

theorem HCPolySupport.HighContrast.sEnergyOn_add_constSkew {d : ℕ} (b : CoeffField d) (U : Set (Vec d)) (F : Vec d → Vec d) (k : Mat d) (hk : IsSkewMat k) : sEnergyOn (fun (x : Vec d) => b x + k) U F = sEnergyOn b U F

Adding a constant skew matrix does not change the symmetric energy.

theorem HCPolySupport.HighContrast.h1sNormSqOn_add_constSkew {d : ℕ} (b : CoeffField d) (U : Set (Vec d)) (u : Vec d → ℝ) (Du : Vec d → Vec d) (k : Mat d) (hk : IsSkewMat k) : h1sNormSqOn (fun (x : Vec d) => b x + k) U u Du = h1sNormSqOn b U u Du

The full symmetric Sobolev energy is invariant under a constant skew shift of the coefficient.