High-contrast homogenization: Provider.Regularity.RoundedCoefficientWeightedNormGauge

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

Scalar and skew-gauge cancellation for the rounded coefficient

The R3-A rounded coefficient is built from a positive scalar multiple of the physical coefficient after subtraction of the constant comparison skew part. This module records the exact effect of those two operations on the normalized weighted gradient norm, so estimates can be returned to the original physical coefficient without adding a hypothesis.

theorem HCPolySupport.HighContrast.weightedGradNorm_smul_coefficient {d : ℕ} {U : Set (Vec d)} (b : CoeffField d) (F : Vec d → Vec d) {mu : ℝ} (hmu : 0 ≤ mu) : weightedGradNorm (fun (x : Vec d) => mu • b x) U F = ENNReal.ofReal mu ^ (1 / 2) * weightedGradNorm b U F

Positive scalar multiplication of the coefficient multiplies the weighted gradient norm by the square root of that scalar.

theorem HCPolySupport.HighContrast.weightedGradNorm_normalizedSkewGauge {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (a : CoeffField d) (U : Set (Vec d)) (F : Vec d → Vec d) : weightedGradNorm (fun (x : Vec d) => specBound (symmPart abar)⁻¹ • (a x - skewPart abar)) U F = ENNReal.ofReal (specBound (symmPart abar)⁻¹) ^ (1 / 2) * weightedGradNorm a U F

The exact scalar-normalized skew gauge used by the rounded map differs from the original physical weighted norm only by its positive scalar factor.

theorem HCPolySupport.HighContrast.weightedGradNorm_le_of_normalizedSkewGauge_le {d : ℕ} [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (a : CoeffField d) (U V : Set (Vec d)) (F : Vec d → Vec d) (C : ENNReal) (hbound : weightedGradNorm (fun (x : Vec d) => specBound (symmPart abar)⁻¹ • (a x - skewPart abar)) U F ≤ C * weightedGradNorm (fun (x : Vec d) => specBound (symmPart abar)⁻¹ • (a x - skewPart abar)) V F) : weightedGradNorm a U F ≤ C * weightedGradNorm a V F

A weighted-norm comparison in the scalar-normalized skew gauge cancels back to the same comparison for the original coefficient.