English
If X is constant, Var[X; μ | m] = 0.
Русский
Если X константна, Var[X; μ | m] = 0.
LaTeX
$$$ Var[\text{const}; μ | m] = 0 $$$
Lean4
@[simp]
theorem condVar_const (hm : m ≤ m₀) (c : ℝ) : Var[fun _ ↦ c; μ | m] = 0 :=
by
obtain rfl | hc := eq_or_ne c 0
· simp [← Pi.zero_def]
by_cases hμm : IsFiniteMeasure μ
· simp [condVar, hm]
·
simp [condVar, condExp_of_not_integrable, integrable_const_iff_isFiniteMeasure hc,
integrable_const_iff_isFiniteMeasure <| pow_ne_zero _ hc, hμm, Pi.pow_def]