lintegral_laverage

Mathlib.MeasureTheory.Integral.Average

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

English

The lintegral of laverage with respect to μ equals the lintegral of f with respect to μ.

Русский

Линтеграл лаverage по μ равен линтегралу f по μ.

LaTeX

$$$\\lintegral⁻ f\\, dμ = \\lintegral⁻ (laverage_{μ}(f))\\, dμ$$$

Lean4

theorem lintegral_laverage (μ : Measure α) [IsFiniteMeasure μ] (f : α → ℝ≥0∞) : ∫⁻ _x, ⨍⁻ a, f a ∂μ ∂μ = ∫⁻ x, f x ∂μ :=
  by simp

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

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

Разделы

Аффилиация

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