laverage_eq_lintegral

Mathlib.MeasureTheory.Integral.Average

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

← MathLib Explorer

English

For normalized μ, laverage coincides with lintegral.

Русский

При нормировке μ laverage совпадает с lintegral.

LaTeX

$$$\\mathrm{laverage}(μ,f) = \\mathrm{lintegral}(μ,f)$$$

Lean4

theorem laverage_eq_lintegral [IsProbabilityMeasure μ] (f : α → ℝ≥0∞) : ⨍⁻ x, f x ∂μ = ∫⁻ x, f x ∂μ := by
  rw [laverage, measure_univ, inv_one, one_smul]

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

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

Разделы

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

Аффилиация

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