lintegral_enorm_eq_lintegral_edist

English

For any f, ∫ ‖f‖ dμ equals ∫ edist(f,0) dμ after converting through EN-norm; equivalently, the ENorm and the lintegral of edist to zero coincide in the appropriate form.

Русский

Для любого f интегрируемого: линтигрально и через норму EN совпадают: интеграл по ‖f‖ равен интегралу edist(f, 0).

LaTeX

$$$ \\int^- a \\, \\mathrm{ENNReal.ofReal}(\\|f(a)\\|) \\, d\\mu = \\int^- a \\, \\mathrm{edist}(f(a), 0) \\, d\\mu(a) $$$

Lean4

theorem lintegral_enorm_eq_lintegral_edist (f : α → β) : ∫⁻ a, ‖f a‖ₑ ∂μ = ∫⁻ a, edist (f a) 0 ∂μ := by
  simp only [edist_zero_eq_enorm]

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