condVar_const — Mathlib

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]

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