High-contrast homogenization: Provider.Regularity.CorrectorWeightedGradientBridge

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

From weighted corrector energy to normalized Euclidean gradient control

The intrinsic good-tail estimate is coefficient-weighted. The Liouville function-growth argument uses ordinary normalized L² Poincare estimates. This module records the exact conversion under a fixed positive global lower ellipticity constant.

theorem HCPolySupport.HighContrast.weightedGradNorm_congr_coeff_ae_on {d : ℕ} {U : Set (Vec d)} {a b : CoeffField d} (F : Vec d → Vec d) (hab : a =ᵐ[volumeMeasureOn U] b) : weightedGradNorm a U F = weightedGradNorm b U F

The weighted norm is invariant under a.e. replacement of its coefficient representative on the integration domain.

theorem HCPolySupport.HighContrast.H1Function.memLp_euclideanGrad_normalizedCubeMeasure {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) : MeasureTheory.MemLp (fun (x : Vec d) => euclideanNorm (u.grad x)) 2 (normalizedCubeMeasure Q)

The Euclidean magnitude of an H¹ weak gradient belongs to normalized L² on its cube.

theorem HCPolySupport.HighContrast.cubeLpNorm_euclideanGrad_sub_const_le {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) (e : Vec d) : (cubeLpNorm Q 2 fun (x : Vec d) => euclideanNorm (u.grad x - e)) ≤ (cubeLpNorm Q 2 fun (x : Vec d) => euclideanNorm (u.grad x)) + euclideanNorm e

Subtracting a constant vector increases the normalized L² norm of the Euclidean magnitude by at most that vector's Euclidean norm.

theorem HCPolySupport.HighContrast.cubeLpNorm_euclideanGrad_le_div_sqrt_of_weightedGradNorm_le {d : ℕ} (Q : TriadicCube d) {b : CoeffField d} {lam Lam B : ℝ} (hlam : 0 < lam) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) b) (u : H1Function (openCubeSet Q)) (hB : 0 ≤ B) (hweighted : weightedGradNorm b (openCubeSet Q) u.grad ≤ ENNReal.ofReal B) : (cubeLpNorm Q 2 fun (x : Vec d) => euclideanNorm (u.grad x)) ≤ B / √lam

A weighted-gradient bound on a cube controls the normalized Euclidean L² norm of the weak gradient, with the expected lam⁻¹/² loss.

theorem HCPolySupport.HighContrast.cubeLpNorm_euclideanGrad_le_div_sqrt_of_ae_weightedGradNorm_le {d : ℕ} (Q : TriadicCube d) {a b : CoeffField d} {lam Lam B : ℝ} (hlam : 0 < lam) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) b) (hab : a =ᵐ[volumeMeasureOn (openCubeSet Q)] b) (u : H1Function (openCubeSet Q)) (hB : 0 ≤ B) (hweighted : weightedGradNorm a (openCubeSet Q) u.grad ≤ ENNReal.ofReal B) : (cubeLpNorm Q 2 fun (x : Vec d) => euclideanNorm (u.grad x)) ≤ B / √lam

The conversion remains valid when the available weighted estimate uses an a.e.-equivalent local coefficient representative.