laverage_zero_measure

Mathlib.MeasureTheory.Integral.Average

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

English

Equality laverage and lintegral for general μ and f.

Русский

Равенство laverage и lintegral для произвольной μ и f.

LaTeX

$$$\\mathrm{laverage}\\;μ\\;f = \\mathrm{lintegral}\\;μ\\; f$$$

Lean4

@[simp]
theorem laverage_zero_measure (f : α → ℝ≥0∞) : ⨍⁻ x, f x ∂(0 : Measure α) = 0 := by simp [laverage]

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

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

Разделы

Аффилиация

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