enorm_toL1 — Mathlib

English

Let f be integrable with respect to μ taking values in a normed additive group. Then the EN-norm of its L1-representation equals the integral of the EN-norm of f: the L1-norm of toL1(f) equals ∫ ‖f‖ dμ.

Русский

Пусть f интегрируема по μ и принимает значения в нормированной аддитивной группе. Тогда EN-норма образа f в пространстве L1 равна интегралу от нормы f: нормa toL1(f) равна ∫ ‖f(x)‖ dμ.

LaTeX

$$$ \\| \\mathrm{toL1}(f) \\|_{\\varepsilon} = \\int\\! d\\mu \\, \\|f(a)\\|_{\\varepsilon} $$$

Lean4

theorem enorm_toL1 {f : α → β} (hf : Integrable f μ) : ‖hf.toL1 f‖ₑ = ∫⁻ a, ‖f a‖ₑ ∂μ :=
  by
  simp only [Lp.enorm_def, toL1_eq_mk, eLpNorm_aeeqFun]
  simp [eLpNorm, eLpNorm']

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