laverage_eq'

Mathlib.MeasureTheory.Integral.Average

URI: https://scilib.ai/kg/mathlib#MeasureTheory.laverage_eq'

English

If μ is a probability measure, the left average equals the integral with respect to μ.

Русский

Если μ вероятностная мера, левое среднее равно интегралу по μ.

LaTeX

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

Lean4

theorem laverage_eq' (f : α → ℝ≥0∞) : ⨍⁻ x, f x ∂μ = ∫⁻ x, f x ∂(μ univ)⁻¹ • μ :=
  rfl

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

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

Разделы

Аффилиация

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