laverage_const

Mathlib.MeasureTheory.Integral.Average

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

← MathLib Explorer

English

Lintegral with laverage equals laverage integral identity.

Русский

Линтеграл лаverage равен интегралу лаverage.

LaTeX

$$$\\lintegral^{\\infty}_{\\mu} (f) = \\lintegral^{\\infty}_{\\mu} (\\laverage_{\\mu} f)\\, d\\mu$$$

Lean4

@[simp]
theorem laverage_const (μ : Measure α) [IsFiniteMeasure μ] [h : NeZero μ] (c : ℝ≥0∞) : ⨍⁻ _x, c ∂μ = c := by
  simp only [laverage, lintegral_const, measure_univ, mul_one]

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

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

Разделы

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

Аффилиация

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