norm_def

Mathlib.MeasureTheory.Function.L1Space.AEEqFun

URI: https://scilib.ai/kg/mathlib#MeasureTheory.L1.norm_def

English

The real-valued norm of an L1 element corresponds to the lintegral of its norm.

Русский

Действительная норма элемента L1 равна линтегралу нормы.

LaTeX

$$ENNReal.ofReal \|f\| = ∫⁻ a, \|f(a)\| dμ$$

Lean4

theorem norm_def (f : α →₁[μ] β) : ‖f‖ = (∫⁻ a, ‖f a‖ₑ ∂μ).toReal := by
  simp [Lp.norm_def, eLpNorm, eLpNorm'_eq_lintegral_enorm]

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

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

Разделы

Аффилиация

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