norm_toL1

Mathlib.MeasureTheory.Function.L1Space.AEEqFun

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Integrable.norm_toL1

← MathLib Explorer

English

For an integrable f, the L1-norm equals the Lintegral of the edistance to zero.

Русский

Для интегрируемой f норма L1 равна линегралу edist(f,0).

LaTeX

$$‖hf.toL1 f‖ = ∫⁻ a, edist (f a) 0 ∂μ).toReal$$

Lean4

theorem norm_toL1 (f : α → β) (hf : Integrable f μ) : ‖hf.toL1 f‖ = (∫⁻ a, edist (f a) 0 ∂μ).toReal := by
  simp [toL1, Lp.norm_toLp, eLpNorm, eLpNorm'_eq_lintegral_enorm]

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

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

Разделы

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

Аффилиация

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