integrable_iff_mem_L1 — Mathlib

English

An AEEqFun f is integrable iff it belongs to the L1 space, i.e., f ∈ (α →₁[μ] β).

Русский

Для AEEqFun f интегрируемость эквивалентна тому, что f принадлежит пространству L1.

LaTeX

$$Integrable(f) \iff f \in (\alpha \to_1[\mu] β)$$

Lean4

theorem integrable_iff_mem_L1 {f : α →ₘ[μ] β} : Integrable f ↔ f ∈ (α →₁[μ] β) := by
  rw [← integrable_coeFn, ← memLp_one_iff_integrable, Lp.mem_Lp_iff_memLp]
    -- TODO: generalise these lemmas to `ENormedSpace` or similar

Похожие утверждения