High-contrast homogenization: Analytic.LocalIntegrability #

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

Local integrability of a member of `H¹_{s,loc}(ℝ^d)` #

The class H¹_{s,loc}(ℝ^d) of s.introduction, in the local form read by the Liouville class e.random.liouville.growth, is defined by approximation in the H¹_s norm on every centred ball. That norm is built from the L¹ mass ∫ |u| and the weighted energy ∫ ∇u · s ∇u, both taken as lower Lebesgue integrals of nonnegative integrands.

This module extracts from the definition the integrability facts that the weak-gradient relation needs in order to be an identity between convergent integrals. The mechanism is the L¹ term: convergence to 0 in ℝ≥0∞ forces (∫⁻ |w n - v|)² to be eventually finite, so ∫⁻ |w n - v| < ∞ for some n; the smooth approximant w n is bounded on the bounded ball; hence ∫⁻ |v| < ∞ there.

The L¹ half of that statement needs no measurability input at all, because the lower Lebesgue integral is defined for every function. Upgrading it to genuine integrability does need a measurability hypothesis, and that hypothesis is not removable: the lower Lebesgue integral is a supremum over simple functions below the integrand and is therefore blind to a perturbation supported on a set of inner measure zero, while the Bochner integrals compared by the weak-gradient relation value a non-integrable integrand at 0. A function invisible to both would satisfy the defining conditions without being almost everywhere strongly measurable, hence without being integrable on any ball. In the formalization the measurability is supplied by the class itself, which carries it as part of its definition; the lemmas here are stated with it explicit so that the dependence is visible.

The `L¹` mass of a member of the local class #

source

theorem HCPolySupport.HighContrast.exists_lintegral_ofReal_abs_sub_ne_top {d : ℕ} {b : CoeffField d} {V : Set (Vec d)} {u : Vec d → ℝ} {Du : Vec d → Vec d} {w : ℕ → Vec d → ℝ} (htend : Filter.Tendsto (fun (n : ℕ) => h1sNormSqOn b V (fun (x : Vec d) => w n x - u x) fun (x : Vec d) => smoothGrad (w n) x - Du x) Filter.atTop (nhds 0)) :

∃ (n : ℕ), ∫⁻ (x : Vec d) in V, ENNReal.ofReal |w n x - u x| ≠ ⊤

Along a sequence whose H¹_s distance to the pair tends to 0, some approximant is at finite L¹ distance.

source

theorem HCPolySupport.HighContrast.lintegral_ofReal_abs_ne_top_of_isBounded {d : ℕ} {V : Set (Vec d)} (hV : Bornology.IsBounded V) {g : Vec d → ℝ} (hg : Continuous g) :

∫⁻ (x : Vec d) in V, ENNReal.ofReal |g x| ≠ ⊤

A continuous function has finite L¹ mass on a bounded set.

source

theorem HCPolySupport.HighContrast.lintegral_ofReal_abs_ne_top_of_sub {d : ℕ} {V : Set (Vec d)} {g h : Vec d → ℝ} (hgmeas : AEMeasurable (fun (x : Vec d) => ENNReal.ofReal |g x|) (MeasureTheory.volume.restrict V)) (hg : ∫⁻ (x : Vec d) in V, ENNReal.ofReal |g x| ≠ ⊤) (hd : ∫⁻ (x : Vec d) in V, ENNReal.ofReal |g x - h x| ≠ ⊤) :

∫⁻ (x : Vec d) in V, ENNReal.ofReal |h x| ≠ ⊤

The L¹ triangle step.

source

theorem HCPolySupport.HighContrast.lintegral_ofReal_abs_ne_top_of_memH1sLoc {d : ℕ} {b : CoeffField d} {v : Vec d → ℝ} {Dv : Vec d → Vec d} (hv : MemH1sLoc b v Dv) {R : ℝ} (hR : 0 < R) :

∫⁻ (x : Vec d) in euclideanBall d R, ENNReal.ofReal |v x| ≠ ⊤

The L¹ half of the local class is honest, with no measurability input at all: the lower Lebesgue integral of |v| over any centred ball is finite.

source

theorem HCPolySupport.HighContrast.integrableOn_of_memH1sLoc {d : ℕ} {b : CoeffField d} {v : Vec d → ℝ} {Dv : Vec d → Vec d} (h : MemH1sLoc b v Dv) {R : ℝ} (hR : 0 < R) (hvmeas : MeasureTheory.AEStronglyMeasurable v (MeasureTheory.volume.restrict (euclideanBall d R))) :

MeasureTheory.IntegrableOn v (euclideanBall d R) MeasureTheory.volume

A pair of the local class has an L¹ representative on every centred ball.

The measurability hypothesis hvmeas is not removable. Membership in MemH1sLoc is blind to a perturbation of v by the indicator of a set of inner measure zero — the lower Lebesgue integral does not see it, and the Bochner integrals of HasWeakGradientOn fall into the branch that values a non-integrable integrand at 0 — so membership alone does not make v almost everywhere strongly measurable.