laverage_lt_top

Mathlib.MeasureTheory.Integral.Average

URI: https://scilib.ai/kg/mathlib#MeasureTheory.laverage_lt_top

Lean4

theorem laverage_lt_top (hf : ∫⁻ x, f x ∂μ ≠ ∞) : ⨍⁻ x, f x ∂μ < ∞ :=
  by
  obtain rfl | hμ := eq_or_ne μ 0
  · simp
  · rw [laverage_eq]
    have := measure_univ_ne_zero.2 hμ
    finiteness

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

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

Разделы

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

Аффилиация

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