High-contrast homogenization: Analytic.ClassPairing

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

From class membership to absolute convergence of the flux pairing

Chaining the finite weighted energy of the coefficient-Sobolev classes through the two-sided energy comparison puts the weak gradient in L², which is exactly what the absolute convergence of the flux pairing needs. No integrability side condition appears in the classes, and none has to be added where the weak interior equation of t.random.homogenization is asserted of a member of one of them.

Three readings are covered: H¹_a(V) on a bounded V; H¹_{a,0}(V) on an arbitrary measurable V; and, at V = ℝ^d, the local class H¹_{s,loc}(ℝ^d) through which the Liouville space e.random.liouville.growth reads the equation. A fourth reading is the affine one of e.random.dirichlet, which carries membership of the shifted pair together with an essential bound on the gradient of the boundary datum; the two together put the unshifted gradient in L².

The chain: class membership implies absolute convergence of the pairing

theorem HCPolySupport.HighContrast.integrableOn_weakPairing_of_memH1a {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) (hV : MeasurableSet V) (hVb : Bornology.IsBounded V) (hbmeas : ∀ (i j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => b x i j) (MeasureTheory.volume.restrict V)) {u : Vec d → ℝ} {Du : Vec d → Vec d} (hDmeas : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => Du x j) (MeasureTheory.volume.restrict V)) (hu : MemH1a b V u Du) {φ : Vec d → ℝ} (hφ : IsLocalTest V φ) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (smoothGrad φ x) (matVecMul (b x) (Du x))) V MeasureTheory.volume

The chain, for H¹_a on a bounded V. Membership in the class forces finite weighted energy, hence Du ∈ L²(V), hence absolute convergence of every weak pairing of Du against a local test. No integrability side condition appears in the class, and none is needed at the statement.

theorem HCPolySupport.HighContrast.integrableOn_weakPairing_of_memH1a0 {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) (hV : MeasurableSet V) (hbmeas : ∀ (i j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => b x i j) (MeasureTheory.volume.restrict V)) {u : Vec d → ℝ} {Du : Vec d → Vec d} (hDmeas : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => Du x j) (MeasureTheory.volume.restrict V)) (hu : MemH1a0 b V u Du) {φ : Vec d → ℝ} (hφ : IsLocalTest V φ) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (smoothGrad φ x) (matVecMul (b x) (Du x))) V MeasureTheory.volume

The chain, for H¹_{a,0} on an arbitrary V.

theorem HCPolySupport.HighContrast.isWeakSolutionOn_iff_of_memH1a {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) (hV : MeasurableSet V) (hVb : Bornology.IsBounded V) (hbmeas : ∀ (i j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => b x i j) (MeasureTheory.volume.restrict V)) {u : Vec d → ℝ} {Du : Vec d → Vec d} (hDmeas : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => Du x j) (MeasureTheory.volume.restrict V)) (hu : MemH1a b V u Du) : IsWeakSolutionOn b V Du ↔ ∀ (φ : Vec d → ℝ), IsLocalTest V φ → ∫ (x : Vec d) in V, vecDot (smoothGrad φ x) (matVecMul (b x) (Du x)) = 0

The design justification for IsWeakSolutionOn on the H¹_a class.

The chain for the affine (Dirichlet) clause

The estimate e.random.dirichlet carries MemH1a0 b U (u - g₀) (Du - Dg) for the shifted pair, together with an essential bound on Dg on the bounded cell U. Those two are enough for Du ∈ L²(U), hence for absolute convergence of the pairing that IsWeakSolutionOn b U Du asserts.

theorem HCPolySupport.HighContrast.integrableOn_vecNormSq_of_memH1a0_sub {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) (hVb : Bornology.IsBounded V) {u g : Vec d → ℝ} {Du Dg : Vec d → Vec d} {L : ℝ} (hDg : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict V, √(vecNormSq (Dg x)) ≤ L) (hDgmeas : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => Dg x j) (MeasureTheory.volume.restrict V)) (hDumeas : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => Du x j) (MeasureTheory.volume.restrict V)) (hu : MemH1a0 b V (fun (x : Vec d) => u x - g x) fun (x : Vec d) => Du x - Dg x) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecNormSq (Du x)) V MeasureTheory.volume

The chain for the Dirichlet clause: shifted class membership plus the clause's own essential bound on the boundary datum give Du ∈ L²(V).

theorem HCPolySupport.HighContrast.integrableOn_weakPairing_of_memH1a0_sub {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) (hV : MeasurableSet V) (hVb : Bornology.IsBounded V) (hbmeas : ∀ (i j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => b x i j) (MeasureTheory.volume.restrict V)) {u g : Vec d → ℝ} {Du Dg : Vec d → Vec d} {L : ℝ} (hDg : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict V, √(vecNormSq (Dg x)) ≤ L) (hDgmeas : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => Dg x j) (MeasureTheory.volume.restrict V)) (hDumeas : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => Du x j) (MeasureTheory.volume.restrict V)) (hu : MemH1a0 b V (fun (x : Vec d) => u x - g x) fun (x : Vec d) => Du x - Dg x) {φ : Vec d → ℝ} (hφ : IsLocalTest V φ) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (smoothGrad φ x) (matVecMul (b x) (Du x))) V MeasureTheory.volume

Absolute convergence of the pairing for the Dirichlet clause.

The chain at V = Set.univ, through H¹_{s,loc}

The Liouville space e.random.liouville.growth asserts IsWeakSolutionOn b Set.univ Dv for a pair that also lies in MemH1sLoc b v Dv. No global L² bound is available there, but MemH1sLoc gives finite weighted energy on every centered Euclidean ball, and every compact set sits inside such a ball; so the local L² hypothesis of integrableOn_weakPairing_of_integrableOn_compacts is derivable.

theorem HCPolySupport.HighContrast.exists_euclideanBall_superset_of_isCompact {d : ℕ} {K : Set (Vec d)} (hK : IsCompact K) : ∃ (R : ℝ), 0 < R ∧ K ⊆ euclideanBall d R

Every compact subset of ℝ^d sits inside a centered Euclidean ball.

theorem HCPolySupport.HighContrast.integrableOn_vecNormSq_isCompact_of_memH1sLoc {d : ℕ} {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) {v : Vec d → ℝ} {Dv : Vec d → Vec d} (hDmeas : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => Dv x j) MeasureTheory.volume) (hv : MemH1sLoc b v Dv) {K : Set (Vec d)} (hK : IsCompact K) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecNormSq (Dv x)) K MeasureTheory.volume

The H¹_{s,loc} class gives local square integrability of the weak gradient on every compact set, with that set's ellipticity constants.

theorem HCPolySupport.HighContrast.isWeakSolutionOn_univ_iff_of_memH1sLoc {d : ℕ} {b : CoeffField d} (hb : IsAELocallyUniformlyElliptic b) (hbmeas : ∀ (i j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => b x i j) MeasureTheory.volume) {v : Vec d → ℝ} {Dv : Vec d → Vec d} (hDmeas : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => Dv x j) MeasureTheory.volume) (hv : MemH1sLoc b v Dv) : IsWeakSolutionOn b Set.univ Dv ↔ ∀ (φ : Vec d → ℝ), IsLocalTest Set.univ φ → ∫ (x : Vec d) in Set.univ, vecDot (smoothGrad φ x) (matVecMul (b x) (Dv x)) = 0

The chain at V = Set.univ, for the Liouville class. Membership in MemH1sLoc makes the integrability conjunct of IsWeakSolutionOn b Set.univ Dv derivable, so it is a consequence of the class rather than a further hypothesis imposed on it.