average_const

Mathlib.MeasureTheory.Integral.Average

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

← MathLib Explorer

English

For constant function c, the average over μ is c: average_μ(c) = c.

Русский

Для константы c среднее по мере равно самой константе: average_μ(c) = c.

LaTeX

$$$\operatorname{average}_\mu c = c$$$

Lean4

@[simp]
theorem average_const (μ : Measure α) [IsFiniteMeasure μ] [h : NeZero μ] (c : E) : ⨍ _x, c ∂μ = c := by
  rw [average, integral_const, measureReal_def, measure_univ, ENNReal.toReal_one, one_smul]

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

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

Разделы

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

Аффилиация

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