integral_eq_const

Mathlib.MeasureTheory.Integral.Bochner.Basic

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

English

If f is ae-equal to c under a probability measure μ, then ∫ f = c.

Русский

Если f равна почти повсюду константе c по мере μ, то интеграл равен c.

LaTeX

$$$\\\\text{ae}(f)=c \\\\Rightarrow \\\\int f dμ = c$$$

Lean4

theorem integral_eq_const [IsProbabilityMeasure μ] {f : α → E} {c : E} (hf : ∀ᵐ x ∂μ, f x = c) : ∫ x, f x ∂μ = c := by
  simp [integral_congr_ae hf]

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

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

Разделы

Аффилиация

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