High-contrast homogenization: Analytic.NormEquivalence

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

Removing the coefficient field from the approximation conditions

h1sNormSqOn b V u Du is ‖u‖_{L¹(V)}² + ∫_V Du · σ Du, the squared H¹_s norm of s.introduction evaluated on a pair (u, Du). Only the second summand sees the coefficient field, and where the field is uniformly elliptic almost everywhere on V it is pinched between lam and Lam multiples of ∫_V ‖Du‖², with the constants of V. The whole quantity is therefore two-sidedly comparable to an unweighted companion, and a sequence tends to 0 in one exactly when it does in the other: every approximation condition of the membership classes is a condition on the classical unweighted space, with the rough coefficient field absent from it.

The ellipticity hypothesis is not removable, but it is a per-set hypothesis: what the comparison needs on V is a pair of constants for V. Both comparison constants, min 1 lam and max 1 Lam, degenerate without it, and the equivalence fails for a coefficient field whose symmetric part is not bounded below on V.

The second section treats the skew part, which the comparison says nothing about: on every bounded set, with that set's constants, the two inequalities packaged in IsEllipticMatrix bound the whole matrix, hence its skew part, by Lam.

The norm-equivalence reduction

h1sNormSqOn b V u Du = ‖u‖_{L¹(V)}² + ∫_V Du · s Du. Only the second summand sees the coefficient field, and on every bounded set, with that set's constants, it is pinched between lam and Lam multiples of ∫_V ‖Du‖² by the two halves already proved for the weighted energy. Consequently the whole quantity is two-sidedly comparable to the unweighted quantity below, and — the point of this section — a sequence tends to 0 in the weighted quantity exactly when it does in the unweighted one. The rough coefficient field is therefore absent from the residual density question, which becomes a citable classical fact about the ordinary space L¹(V) × L²(V) rather than an open question about weighted spaces.

noncomputable def HCPolySupport.HighContrast.h1NormSqOnUnweighted {d : ℕ} (V : Set (Vec d)) (u : Vec d → ℝ) (Du : Vec d → Vec d) : ENNReal

The unweighted companion of h1sNormSqOn: ‖u‖_{L¹(V)}² + ∫_V ‖Du‖².

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.ofReal_min_mul_h1NormSqOnUnweighted_le_h1sNormSqOn_restrict {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hell : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict V, IsEllipticMatrix lam Lam (b x)) (u : Vec d → ℝ) (Du : Vec d → Vec d) : ENNReal.ofReal (min 1 lam) * h1NormSqOnUnweighted V u Du ≤ h1sNormSqOn b V u Du

The lower half of the two-sided comparison. The constant min 1 lam is the worse of the two summandwise constants: 1 on the L¹ term, which carries no weight, and lam on the energy term.

theorem HCPolySupport.HighContrast.ofReal_min_mul_h1NormSqOnUnweighted_le_h1sNormSqOn {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) (u : Vec d → ℝ) (Du : Vec d → Vec d) : ENNReal.ofReal (min 1 lam) * h1NormSqOnUnweighted V u Du ≤ h1sNormSqOn b V u Du

The lower half of the two-sided comparison, with the pinching read on all of ℝ^d.

theorem HCPolySupport.HighContrast.h1sNormSqOn_le_ofReal_max_mul_h1NormSqOnUnweighted_restrict {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hell : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict V, IsEllipticMatrix lam Lam (b x)) (u : Vec d → ℝ) (Du : Vec d → Vec d) : h1sNormSqOn b V u Du ≤ ENNReal.ofReal (max 1 Lam) * h1NormSqOnUnweighted V u Du

The upper half of the two-sided comparison, with constant max 1 Lam and the pinching read on V alone.

theorem HCPolySupport.HighContrast.h1sNormSqOn_le_ofReal_max_mul_h1NormSqOnUnweighted {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) (u : Vec d → ℝ) (Du : Vec d → Vec d) : h1sNormSqOn b V u Du ≤ ENNReal.ofReal (max 1 Lam) * h1NormSqOnUnweighted V u Du

The upper half of the two-sided comparison, with constant max 1 Lam.

theorem HCPolySupport.HighContrast.tendsto_zero_of_le_of_tendsto_zero {ι : Type u_1} {l : Filter ι} {f g : ι → ENNReal} (hfg : ∀ (n : ι), f n ≤ g n) (hg : Filter.Tendsto g l (nhds 0)) : Filter.Tendsto f l (nhds 0)

Domination transfers a limit 0 in ℝ≥0∞.

theorem HCPolySupport.HighContrast.tendsto_h1sNormSqOn_zero_iff_restrict {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hell : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict V, IsEllipticMatrix lam Lam (b x)) {ι : Type u_1} {l : Filter ι} (u : ι → Vec d → ℝ) (Du : ι → Vec d → Vec d) : Filter.Tendsto (fun (n : ι) => h1sNormSqOn b V (u n) (Du n)) l (nhds 0) ↔ Filter.Tendsto (fun (n : ι) => h1NormSqOnUnweighted V (u n) (Du n)) l (nhds 0)

The reduction. On every bounded set, with that set's constants, convergence to 0 in the weighted H¹_s quantity is equivalent to convergence to 0 in the unweighted quantity. The coefficient field b has disappeared from the right hand side: every remaining density question about the H¹_s part of MemH1a, MemH1a0 and MemH1sLoc is a question about the classical unweighted space.

theorem HCPolySupport.HighContrast.tendsto_h1sNormSqOn_zero_iff {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) {ι : Type u_1} {l : Filter ι} (u : ι → Vec d → ℝ) (Du : ι → Vec d → Vec d) : Filter.Tendsto (fun (n : ι) => h1sNormSqOn b V (u n) (Du n)) l (nhds 0) ↔ Filter.Tendsto (fun (n : ι) => h1NormSqOnUnweighted V (u n) (Du n)) l (nhds 0)

The reduction, with the pinching read on all of ℝ^d.

theorem HCPolySupport.HighContrast.tendsto_h1sNormSqOn_sub_zero_iff_restrict {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hell : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict V, IsEllipticMatrix lam Lam (b x)) (u : Vec d → ℝ) (Du : Vec d → Vec d) (v : ℕ → Vec d → ℝ) : Filter.Tendsto (fun (n : ℕ) => h1sNormSqOn b V (fun (x : Vec d) => v n x - u x) fun (x : Vec d) => smoothGrad (v n) x - Du x) Filter.atTop (nhds 0) ↔ Filter.Tendsto (fun (n : ℕ) => h1NormSqOnUnweighted V (fun (x : Vec d) => v n x - u x) fun (x : Vec d) => smoothGrad (v n) x - Du x) Filter.atTop (nhds 0)

The reduction at the exact shape occurring in MemH1a, MemH1a0 and MemH1sLoc, with the pinching read on V alone: the H¹_s approximation condition on a smooth approximating sequence is unweighted H¹ approximation.

theorem HCPolySupport.HighContrast.tendsto_h1sNormSqOn_sub_zero_iff {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) (u : Vec d → ℝ) (Du : Vec d → Vec d) (v : ℕ → Vec d → ℝ) : Filter.Tendsto (fun (n : ℕ) => h1sNormSqOn b V (fun (x : Vec d) => v n x - u x) fun (x : Vec d) => smoothGrad (v n) x - Du x) Filter.atTop (nhds 0) ↔ Filter.Tendsto (fun (n : ℕ) => h1NormSqOnUnweighted V (fun (x : Vec d) => v n x - u x) fun (x : Vec d) => smoothGrad (v n) x - Du x) Filter.atTop (nhds 0)

The reduction at the exact shape occurring in MemH1a, MemH1a0 and MemH1sLoc: the H¹_s approximation condition on a smooth approximating sequence is unweighted H¹ approximation.

The skew flux is not a second obstruction

MemH1a carries a third clause beyond the H¹_s approximation, namely skewFluxDualNorm b V (∇vₙ - Du) → 0, and the previous section says nothing about it. One might fear that this clause is a genuinely separate density problem, with no ambient bound on the skew part k available — that is what "high contrast" would normally mean.

It is not. On the class actually used here, AEUniformlyEllipticField, the two inequalities packaged in IsEllipticMatrix (coercivity of A and coercivity of A⁻¹) already bound the whole matrix on every bounded set, with that set's constants, hence its skew part; the fact is vecNormSq_matVecMul_skewPart_le_of_isEllipticMatrix in CoarseGraining. The three lemmas below are the pointwise ingredients of the resulting domination skewFluxDualNorm b V F ≲ Lam · lam^{-1/2} · ‖F‖_{L²(V)}, which makes the third clause a consequence of the second rather than an independent obligation. Only the integrability bookkeeping of the ⊤ branch of skewFluxPairing separates these ingredients from that statement.

theorem HCPolySupport.HighContrast.ae_vecNormSq_matVecMul_skewPart_le {d : ℕ} {b : CoeffField d} {lam Lam : ℝ} (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) : ∀ᵐ (x : Vec d), ∀ (ξ : Vec d), vecNormSq (matVecMul (skewPart (b x)) ξ) ≤ Lam ^ 2 * vecNormSq ξ

The skew part is bounded on the coefficient class. The uniform ellipticity that AEUniformlyEllipticField supplies on each bounded set bounds the whole matrix there, hence its skew part, by Lam: the high-contrast degeneracy does not reach the skew flux.

theorem HCPolySupport.HighContrast.sq_vecDot_matVecMul_skewPart_le {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (G F : Vec d) : vecDot G (matVecMul (skewPart A) F) ^ 2 ≤ Lam ^ 2 * (vecNormSq G * vecNormSq F)

Cauchy–Schwarz for the integrand of skewFluxPairing: it is bounded by Lam times the product of the two Euclidean norms.

theorem HCPolySupport.HighContrast.lintegral_vecNormSq_le_of_h1sNormSqOn_le_one {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) {φ : Vec d → ℝ} (hφ : h1sNormSqOn b V φ (smoothGrad φ) ≤ 1) : ∫⁻ (x : Vec d) in V, ENNReal.ofReal (vecNormSq (smoothGrad φ x)) ≤ ENNReal.ofReal lam⁻¹

The test class of skewFluxDualNorm is bounded in L². A test of unit weighted H¹_s norm has squared L² gradient at most lam⁻¹, so the supremum defining the dual norm ranges over an L²-bounded family.