Lebesgue integrals of truncations

The truncations min f M of a function f : α → ℝ≥0∞ at finite levels M increase to f, so by monotone convergence their Lebesgue integrals tend to that of f as M → ∞. Neither f nor its integral needs to be finite.

Cutting the truncations off outside the sets spanning a σ-finite measure also makes every power of them integrable, so a bound on ∫⁻ φ ^ q proved for all φ ≤ G with ∫⁻ φ ^ q finite passes to ∫⁻ G ^ q. This is the usual way to divide an inequality by a power of the quantity being estimated.

Main statements

• TauCeti.tendsto_lintegral_min_atTop: ∫⁻ x, min (f x) M ∂μ → ∫⁻ x, f x ∂μ as M → ∞.
• TauCeti.lintegral_enorm_rpow_eq_setLIntegral: the q-th power integral of a truncation to a measurable set is the truncated integral.
• TauCeti.lintegral_rpow_le_of_forall_le: a bound on ∫⁻ φ ^ q for the measurable φ ≤ G with ∫⁻ φ ^ q finite is a bound on ∫⁻ G ^ q.

theorem TauCeti.tendsto_lintegral_min_atTop {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) : Filter.Tendsto (fun (M : NNReal) => ∫⁻ (x : α), min (f x) ↑M ∂μ) Filter.atTop (nhds (∫⁻ (x : α), f x ∂μ))

Integrals of truncations. If f : α → ℝ≥0∞ is almost everywhere measurable, then the integrals of its truncations min f M tend to the integral of f as the finite level M tends to ∞, whether or not that integral is finite.

theorem TauCeti.lintegral_enorm_rpow_eq_setLIntegral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : Type u_2} [TopologicalSpace E] [ESeminormedAddMonoid E] {q : ℝ} {f g : α → E} {R : Set α} (hR : MeasurableSet R) (hg : g =ᵐ[μ] R.indicator f) (hq : 0 < q) : ∫⁻ (x : α), ‖g x‖ₑ ^ q ∂μ = ∫⁻ (x : α) in R, ‖f x‖ₑ ^ q ∂μ

The q-th power integral of a truncation of f is a truncated integral of ‖f‖ ^ q.

theorem TauCeti.lintegral_rpow_le_of_forall_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {G : α → ENNReal} (hG : Measurable G) {q : ℝ} (hq : 0 < q) {C : ENNReal} (h : ∀ (φ : α → ENNReal), Measurable φ → (∀ (x : α), φ x ≤ G x) → ∫⁻ (x : α), φ x ^ q ∂μ ≠ ⊤ → ∫⁻ (x : α), φ x ^ q ∂μ ≤ C) : ∫⁻ (x : α), G x ^ q ∂μ ≤ C

Monotone convergence through truncations. For a σ-finite measure μ and 0 < q, if ∫⁻ φ ^ q ≤ C for every measurable φ ≤ G with ∫⁻ φ ^ q finite, then ∫⁻ G ^ q ≤ C.

The truncations min G N, cut off outside the N-th spanning set of μ, have finite ∫⁻ φ ^ q and increase to G.