English
The pushforward of a measure μ by a constant function to c is μ(univ) times the Dirac measure at c.
Русский
Образ меры μ по константной функции в точку c равен μ(всё пространство) умноженной на меру Дирака в точке c.
LaTeX
$$$ \\mu.map (\\lambda _ => c) = (\\mu Set.univ) \\cdot dirac c $$$
Lean4
@[simp]
theorem map_const (μ : Measure α) (c : β) : μ.map (fun _ ↦ c) = (μ Set.univ) • dirac c :=
by
ext s hs
simp only [Measure.coe_smul, Pi.smul_apply, dirac_apply' _ hs, smul_eq_mul]
classical
rw [Measure.map_apply measurable_const hs, Set.preimage_const]
by_cases hsc : c ∈ s
· rw [(Set.indicator_eq_one_iff_mem _).mpr hsc, mul_one, if_pos hsc]
· rw [if_neg hsc, (Set.indicator_eq_zero_iff_notMem _).mpr hsc, measure_empty, mul_zero]
