average_zero

Mathlib.MeasureTheory.Integral.Average

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

English

Definition of average value of a function with respect to a measure.

Русский

Определение среднего значения функции по мере.

LaTeX

$$$\\text{average}(f) := ∫ x f(x) dμ \\;∕\\; μ(Ω)$$$

Lean4

@[simp]
theorem average_zero : ⨍ _, (0 : E) ∂μ = 0 := by rw [average, integral_zero]

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

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

Разделы

Аффилиация

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