mem_Lp_of_ae_bound

Mathlib.MeasureTheory.Function.LpSpace.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Lp.mem_Lp_of_ae_bound

← MathLib Explorer

English

If a.e. nnnorm bound holds, then f ∈ Lp.

Русский

Если а.е. граница по nnnorm выполняется, то f ∈ Lp.

LaTeX

$$$f ∈ Lp\, E\, p\, μ$ при ae-bound on nnnorm$$

Lean4

theorem mem_Lp_of_ae_bound [IsFiniteMeasure μ] {f : α →ₘ[μ] E} (C : ℝ) (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : f ∈ Lp E p μ :=
  mem_Lp_iff_memLp.2 <| MemLp.of_bound f.aestronglyMeasurable _ hfC

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru