Additional lemmas for the Bochner integral

This file records general-purpose lemmas for Bochner integrals, including bridges between real-valued Bochner integrals and extended-nonnegative Lebesgue integrals, as well as inequalities for set and probability integrals.

Positive parts

• ofReal_integral_le_lintegral_ofReal bounds the positive part of a real-valued function's integral by the integral of its pointwise positive part.

Set and probability integrals

• sq_setIntegral_le_measureReal_mul_setIntegral_sq is Cauchy--Schwarz for a real-valued set integral, in squared form.
• setIntegral_le_setIntegral_sq_mul_of_eqOn compares an integral over a set with a weighted integral over a larger set, for a [0, 1]-valued weight equal to one on the smaller set.
• The set-integral inequality specializes to the second-moment lower bound for a real-valued function on a probability space.
• integral_max_sub_sq_le_mul_measureReal bounds the integral of the squared truncation ((f - l)⁺)² of a function f ≤ M by (M - l)² times the measure of {l ≤ f}.

L¹ convergence

L¹ convergence is often produced in the Bochner form ∫ ω, ‖f i ω - g ω‖ ∂μ → 0 but consumed in the seminorm form eLpNorm (f i - g) 1 μ → 0 (for instance by MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm).

• tendsto_eLpNorm_one_of_tendsto_integral_norm_sub converts the former into the latter.

The conversion is MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm, whose home is Mathlib.MeasureTheory.Integral.Bochner.Basic, plus continuity of ENNReal.ofReal at 0.

Tail lower bounds

A function on the real line whose norm stays above a positive constant on a set of infinite measure cannot be integrable there.

• not_integrableOn_Ioi_of_eventually_le_norm is the half-line form, and not_integrable_of_eventually_le_atTop is its real-valued Lebesgue-integrability consequence.

Reflection across the origin

• integrable_comp_abs extends integrability on the positive half-line to an even function on the whole real line by reflection.

Kernel averages on the real line

• integral_kernel_mem_Icc_of_antitoneOn squeezes the average of a function against a probability density supported in [-ε, 0] between the function's values at t + ε and t, given only antitonicity on the sampled interval [t, t + ε].

Almost-everywhere disjoint finite unions

Mathlib's MeasureTheory.integral_biUnion_finset splits an integral over a finite union into a sum, but asks for genuinely measurable and genuinely disjoint pieces. A family of translates of a fundamental domain need satisfy neither: they overlap on a null set, and MeasureTheory.IsFundamentalDomain records its pieces as MeasureTheory.NullMeasurableSet, pairwise MeasureTheory.AEDisjoint, rather than as disjoint measurable sets.

• integral_biUnion_finset₀ is the almost-everywhere form, in the ₀ convention of MeasureTheory.lintegral_biUnion_finset₀.

Adapted from the AINTLIB LeanModularForms project, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms, commit 6d87d596a5372d5b122c47b7082d4c3afa9b7c3b, Apache-2.0 — HeckeRIngs/GL2/AdjointTheory/SummandAdjoint.lean, setIntegral_biUnion_finset_ae, where it is stated for the same purpose. The name here follows the Mathlib lemma it weakens rather than that source's.

theorem TauCeti.MeasureTheory.integrable_comp_abs {E : Type u_1} [NormedAddCommGroup E] {f : ℝ → E} (hf : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : ℝ) => f |x|) MeasureTheory.volume

An even function obtained by composing with absolute value is integrable on the whole real line whenever the original function is integrable on the positive half-line.

theorem TauCeti.MeasureTheory.not_integrableOn_Ioi_of_eventually_le_norm {E : Type u_1} [NormedAddCommGroup E] {f : ℝ → E} {ε : ℝ} (hε : 0 < ε) (c : ℝ) (hf : ∀ᶠ (x : ℝ) in Filter.atTop, ε ≤ ‖f x‖) : ¬MeasureTheory.IntegrableOn f (Set.Ioi c) MeasureTheory.volume

A function whose norm is eventually at least a positive constant at atTop is not integrable on any right half-line: it is bounded below in norm on a set of infinite measure.

theorem TauCeti.MeasureTheory.not_integrable_of_eventually_le_atTop {f : ℝ → ℝ} {ε : ℝ} (hε : 0 < ε) (hf : ∀ᶠ (x : ℝ) in Filter.atTop, ε ≤ f x) : ¬MeasureTheory.Integrable f MeasureTheory.volume

A real function that is eventually at least a positive constant at atTop is not Lebesgue integrable.

theorem TauCeti.MeasureTheory.sq_setIntegral_le_measureReal_mul_setIntegral_sq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (f : Ω → ℝ) (S : Set Ω) (hS_top : μ S ≠ ⊤) (hf : MeasureTheory.IntegrableOn f S μ) (hf_sq : MeasureTheory.IntegrableOn (fun (x : Ω) => f x ^ 2) S μ) : (∫ (x : Ω) in S, f x ∂μ) ^ 2 ≤ μ.real S * ∫ (x : Ω) in S, f x ^ 2 ∂μ

Cauchy--Schwarz for a real-valued set integral over a set of finite measure, in squared form.

theorem TauCeti.MeasureTheory.setIntegral_le_setIntegral_sq_mul_of_eqOn {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {s t : Set X} {f ψ : X → ℝ} (hf : MeasureTheory.IntegrableOn f s μ) (hf0 : ∀ (x : X), 0 ≤ f x) (hψ : MeasureTheory.AEStronglyMeasurable ψ (μ.restrict s)) (hψ01 : Set.range ψ ⊆ Set.Icc 0 1) (ht : MeasurableSet t) (hψ1 : Set.EqOn ψ 1 t) (hts : t ⊆ s) : ∫ (x : X) in t, f x ∂μ ≤ ∫ (x : X) in s, ψ x ^ 2 * f x ∂μ

A weight ψ with values in [0, 1] that equals one on a measurable set t ⊆ s bounds the integral of a nonnegative function over t by the ψ²-weighted integral over s.

theorem TauCeti.MeasureTheory.integral_max_sub_sq_le_mul_measureReal {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ω → ℝ} (hf : Measurable f) {l M : ℝ} (hM : ∀ᵐ (x : Ω) ∂μ, f x ≤ M) : ∫ (x : Ω), max (f x - l) 0 ^ 2 ∂μ ≤ (M - l) ^ 2 * μ.real {x : Ω | l ≤ f x}

On a finite measure space where f ≤ M almost everywhere, the integral of the squared truncation ((f - l)⁺)² is at most (M - l)² times the measure of the upper level set {l ≤ f}. In De Giorgi's method this turns a measure estimate for upper level sets into an L² estimate for truncations.

theorem TauCeti.MeasureTheory.ofReal_integral_le_lintegral_ofReal {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {f : Ω → ℝ} : ENNReal.ofReal (∫ (x : Ω), f x ∂μ) ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ

The positive part of the integral of a real-valued function is at most the integral of its pointwise positive part. No integrability or pointwise sign assumption on f is needed.

theorem TauCeti.MeasureTheory.tendsto_eLpNorm_one_of_tendsto_integral_norm_sub {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [NormedAddCommGroup E] {μ : MeasureTheory.Measure Ω} {l : Filter ι} {f : ι → Ω → E} {g : Ω → E} (hf : ∀ (i : ι), MeasureTheory.Integrable (f i) μ) (hg : MeasureTheory.Integrable g μ) (h : Filter.Tendsto (fun (i : ι) => ∫ (ω : Ω), ‖f i ω - g ω‖ ∂μ) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (f i - g) 1 μ) l (nhds 0)

L¹ convergence in Bochner form is eLpNorm _ 1 convergence. If ∫ ‖f i - g‖ → 0 along l, with every f i and g integrable, then eLpNorm (f i - g) 1 μ → 0.

theorem TauCeti.MeasureTheory.integral_kernel_mem_Icc_of_antitoneOn {μ : MeasureTheory.Measure ℝ} {ψ F : ℝ → ℝ} {ε t : ℝ} (hFanti : AntitoneOn F (Set.Icc t (t + ε))) (hψ0 : ∀ (s : ℝ), 0 ≤ ψ s) (hψint : ∫ (s : ℝ), ψ s ∂μ = 1) (hsupp : ∀ (s : ℝ), ψ s ≠ 0 → s ∈ Set.Icc (-ε) 0) : ∫ (s : ℝ), ψ s * F (t - s) ∂μ ∈ Set.Icc (F (t + ε)) (F t)

Averaging against a kernel supported in [-ε, 0] samples only [t, t + ε]. If ψ is a nonnegative probability density with respect to μ vanishing outside [-ε, 0], and F is antitone on [t, t + ε], then the average ∫ s, ψ s * F (t - s) ∂μ lies between F (t + ε) and F t.

Use this to bound a mollification of a monotone function by two of its values. No separate integrability hypotheses or sign assumption on ε are needed.

theorem TauCeti.MeasureTheory.integral_biUnion_finset₀ {X : Type u_1} {E : Type u_2} {ι : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure X} {f : X → E} (s : Finset ι) {t : ι → Set X} (hd : (↑s).Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) t)) (hm : ∀ i ∈ s, MeasureTheory.NullMeasurableSet (t i) μ) (hf : MeasureTheory.IntegrableOn f (⋃ i ∈ s, t i) μ) : ∫ (x : X) in ⋃ i ∈ s, t i, f x ∂μ = ∑ i ∈ s, ∫ (x : X) in t i, f x ∂μ

A Bochner integral over a finite almost-everywhere disjoint union splits as a sum.

The almost-everywhere counterpart of MeasureTheory.integral_biUnion_finset, which asks for genuinely measurable and genuinely disjoint pieces: here the pieces need only be MeasureTheory.NullMeasurableSet and pairwise MeasureTheory.AEDisjoint, which is what MeasureTheory.IsFundamentalDomain supplies for a family of translates of a fundamental domain.

Integrability is asked for once, on the union, rather than on each piece. The two are equivalent — MeasureTheory.integrableOn_finset_iUnion — and the union is the form MeasureTheory.integral_iUnion_ae consumes.