High-contrast homogenization: Analytic.WeakPairing

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

Absolute convergence of the weak flux pairing

The weak interior equation of t.random.homogenization is read against smooth compactly supported tests, and the printed distributional display presupposes that each test pairing converges absolutely. That convergence is derived here rather than assumed: ∇φ is continuous with compact support, the entries of an almost everywhere uniformly elliptic coefficient field are essentially bounded, and a field square integrable on the compact set tsupport φ — which has finite measure whatever V is — pairs with them absolutely. Off tsupport φ the integrand vanishes identically, so nothing about V beyond its measurability is used.

The consequence is that the integrability conjunct carried by IsWeakSolutionOn costs nothing on the coefficient class: for a field of L²(V) the predicate is equivalent to the bare vanishing of every test pairing. A local variant, asking square integrability only on the compact subsets of V, is what applies at V = ℝ^d, where no global L² bound is available.

theorem HCPolySupport.HighContrast.continuous_smoothGrad {d : ℕ} {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : Continuous (smoothGrad φ)

The coordinate gradient of a smooth function is continuous.

theorem HCPolySupport.HighContrast.smoothGrad_eq_zero_of_notMem_tsupport {d : ℕ} {φ : Vec d → ℝ} {x : Vec d} (hx : x ∉ tsupport φ) : smoothGrad φ x = 0

The coordinate gradient vanishes off the topological support.

theorem HCPolySupport.HighContrast.integrableOn_weakPairing_of_integrableOn_tsupport_of_locallyBounded {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {F : Vec d → Vec d} {φ : Vec d → ℝ} (hV : MeasurableSet V) (hbmeas : ∀ (i j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => b x i j) (MeasureTheory.volume.restrict V)) (hbdd : ∀ (K : Set (Vec d)), IsCompact K → ∃ (M : ℝ), 0 ≤ M ∧ ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict K, ∀ (i j : Fin d), |b x i j| ≤ M) (hφ : IsLocalTest V φ) (hFmeas : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => F x j) (MeasureTheory.volume.restrict V)) (hF : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecNormSq (F x)) (tsupport φ) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (smoothGrad φ x) (matVecMul (b x) (F x))) V MeasureTheory.volume

The core convergence lemma. The weak flux pairing of a local test against a field that is square integrable on the test's support is absolutely convergent.

Hypotheses used, in full: V measurable; the entries of b are a.e. strongly measurable and a.e. bounded; φ is a local test on V; the components of F are a.e. strongly measurable; and F ∈ L² on tsupport φ only.

theorem HCPolySupport.HighContrast.ae_abs_entry_le_isCompact_of_ae_abs_entry_le {d : ℕ} {b : CoeffField d} (hbdd : ∃ (M : ℝ), 0 ≤ M ∧ ∀ᵐ (x : Vec d), ∀ (i j : Fin d), |b x i j| ≤ M) (K : Set (Vec d)) (_hK : IsCompact K) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict K, ∀ (i j : Fin d), |b x i j| ≤ M

The entry bound on all of ℝ^d restricts to every compact set.

theorem HCPolySupport.HighContrast.integrableOn_weakPairing_of_integrableOn_tsupport {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {F : Vec d → Vec d} {φ : Vec d → ℝ} (hV : MeasurableSet V) (hbmeas : ∀ (i j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => b x i j) (MeasureTheory.volume.restrict V)) (hbdd : ∃ (M : ℝ), 0 ≤ M ∧ ∀ᵐ (x : Vec d), ∀ (i j : Fin d), |b x i j| ≤ M) (hφ : IsLocalTest V φ) (hFmeas : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => F x j) (MeasureTheory.volume.restrict V)) (hF : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecNormSq (F x)) (tsupport φ) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (smoothGrad φ x) (matVecMul (b x) (F x))) V MeasureTheory.volume

The core convergence lemma, with the entry bound on all of ℝ^d.

theorem HCPolySupport.HighContrast.integrableOn_weakPairing {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {F : Vec d → Vec d} {φ : Vec d → ℝ} (hV : MeasurableSet V) (hbmeas : ∀ (i j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => b x i j) (MeasureTheory.volume.restrict V)) (hbdd : ∃ (M : ℝ), 0 ≤ M ∧ ∀ᵐ (x : Vec d), ∀ (i j : Fin d), |b x i j| ≤ M) (hφ : IsLocalTest V φ) (hFmeas : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => F x j) (MeasureTheory.volume.restrict V)) (hF : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecNormSq (F x)) V MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (smoothGrad φ x) (matVecMul (b x) (F x))) V MeasureTheory.volume

The weak flux pairing of a local test on V against a field of L²(V) is absolutely convergent.

theorem HCPolySupport.HighContrast.integrableOn_weakPairing_of_integrableOn_compacts {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {F : Vec d → Vec d} {φ : Vec d → ℝ} (hV : MeasurableSet V) (hbmeas : ∀ (i j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => b x i j) (MeasureTheory.volume.restrict V)) (hbdd : ∃ (M : ℝ), 0 ≤ M ∧ ∀ᵐ (x : Vec d), ∀ (i j : Fin d), |b x i j| ≤ M) (hφ : IsLocalTest V φ) (hFmeas : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => F x j) (MeasureTheory.volume.restrict V)) (hFloc : ∀ (K : Set (Vec d)), IsCompact K → K ⊆ V → MeasureTheory.IntegrableOn (fun (x : Vec d) => vecNormSq (F x)) K MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (smoothGrad φ x) (matVecMul (b x) (F x))) V MeasureTheory.volume

The local form. Only square integrability on the compact subsets of V is needed; this is the form that applies at V = Set.univ, where no global L² bound is available.

theorem HCPolySupport.HighContrast.integrableOn_weakPairing_of_integrableOn_compacts_of_locallyBounded {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {F : Vec d → Vec d} {φ : Vec d → ℝ} (hV : MeasurableSet V) (hbmeas : ∀ (i j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => b x i j) (MeasureTheory.volume.restrict V)) (hbdd : ∀ (K : Set (Vec d)), IsCompact K → ∃ (M : ℝ), 0 ≤ M ∧ ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict K, ∀ (i j : Fin d), |b x i j| ≤ M) (hφ : IsLocalTest V φ) (hFmeas : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => F x j) (MeasureTheory.volume.restrict V)) (hFloc : ∀ (K : Set (Vec d)), IsCompact K → K ⊆ V → MeasureTheory.IntegrableOn (fun (x : Vec d) => vecNormSq (F x)) K MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (smoothGrad φ x) (matVecMul (b x) (F x))) V MeasureTheory.volume

The local form, with the entry bound read on each compact set. This is the form the whole-space reading takes on the coefficient class, where no entry bound on all of ℝ^d is available.

theorem HCPolySupport.HighContrast.isWeakSolutionOn_iff {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {F : Vec d → Vec d} (hV : MeasurableSet V) (hbmeas : ∀ (i j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => b x i j) (MeasureTheory.volume.restrict V)) (hbdd : ∃ (M : ℝ), 0 ≤ M ∧ ∀ᵐ (x : Vec d), ∀ (i j : Fin d), |b x i j| ≤ M) (hFmeas : ∀ (j : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => F x j) (MeasureTheory.volume.restrict V)) (hF : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecNormSq (F x)) V MeasureTheory.volume) : IsWeakSolutionOn b V F ↔ ∀ (φ : Vec d → ℝ), IsLocalTest V φ → ∫ (x : Vec d) in V, vecDot (smoothGrad φ x) (matVecMul (b x) (F x)) = 0

The design justification for IsWeakSolutionOn. On the coefficient class, and for a field of L²(V), the integrability conjunct of IsWeakSolutionOn costs nothing: the predicate is equivalent to the bare vanishing of every test pairing.

theorem HCPolySupport.HighContrast.ae_abs_entry_le_isCompact_of_ae_isEllipticMatrix_restrict {d : ℕ} {b : CoeffField d} {lam Lam : ℝ} {K : Set (Vec d)} (hlam : 0 < lam) (hle : lam ≤ Lam) (hell : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict K, IsEllipticMatrix lam Lam (b x)) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict K, ∀ (i j : Fin d), |b x i j| ≤ M

The essential entry bound of the coefficient class on a compact set, in the form the pairing lemmas take it: the upper constant of the set bounds every entry there.

theorem HCPolySupport.HighContrast.ae_abs_entry_le_of_ae_isEllipticMatrix {d : ℕ} {b : CoeffField d} {lam Lam : ℝ} (hlam : 0 < lam) (hle : lam ≤ Lam) (hell : ∀ᵐ (x : Vec d), IsEllipticMatrix lam Lam (b x)) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ᵐ (x : Vec d), ∀ (i j : Fin d), |b x i j| ≤ M

The essential entry bound of the coefficient class, in the form the pairing lemmas take it.