integrableOn_Lp_of_measure_ne_top

English

If f is in Lp with respect to μ and p ≥ 1, and μ s ≠ ∞ for a set s, then f restricted to s is integrable on Lp.

Русский

Если f принадлежит Lp по μ и p ≥ 1, и μ s ≠ ∞, тогда f на s интегрируем по Lp.

LaTeX

$$$$f ∈ L^p(μ) \wedge μ(s) ≠ ∞ \Rightarrow f|_s ∈ L^p(μ|_s).$$$$

Lean4

theorem integrableOn_Lp_of_measure_ne_top {E} [NormedAddCommGroup E] {p : ℝ≥0∞} {s : Set α} (f : Lp E p μ) (hp : 1 ≤ p)
    (hμs : μ s ≠ ∞) : IntegrableOn f s μ :=
  by
  refine memLp_one_iff_integrable.mp ?_
  have hμ_restrict_univ : (μ.restrict s) Set.univ < ∞ := by
    simpa only [Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply, lt_top_iff_ne_top]
  haveI hμ_finite : IsFiniteMeasure (μ.restrict s) := ⟨hμ_restrict_univ⟩
  exact ((Lp.memLp _).restrict s).mono_exponent hp

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