integrable_norm_rpow' — Mathlib

English

If [IsFiniteMeasure μ], MemLp f p μ for p ∈ ENNReal, then Integrable (‖f‖^p.toReal) μ.

Русский

Если μ конечна и f ∈ L^p(μ) для p ∈ ENNReal, то Integrable(‖f‖^p) по μ.

LaTeX

$$$[IsFiniteMeasure \\mu] \\Rightarrow (\\forall f,p)(MemLp(f,p,μ) \\Rightarrow Integrable (‖f‖^p) μ).$$$

Lean4

theorem integrable_norm_rpow' [IsFiniteMeasure μ] {f : α → β} {p : ℝ≥0∞} (hf : MemLp f p μ) :
    Integrable (fun x : α => ‖f x‖ ^ p.toReal) μ :=
  by
  by_cases h_zero : p = 0
  · simp [h_zero]
  by_cases h_top : p = ∞
  · simp [h_top]
  exact hf.integrable_norm_rpow h_zero h_top

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