withDensity_const

Mathlib.MeasureTheory.Measure.WithDensity

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

English

If the density is a constant c, then μ.f equals c times μ.

Русский

Если плотность константна и равна c, то μ с плотностью f равно c·μ.

LaTeX

$$$(\\mu_f) = c\\cdot \\mu \\quad (f\\equiv c)$$$

Lean4

@[simp]
theorem withDensity_const (c : ℝ≥0∞) : μ.withDensity (fun _ ↦ c) = c • μ :=
  by
  ext1 s hs
  simp [withDensity_apply _ hs]

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

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

Разделы

Аффилиация

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