condExp_ofNat — Mathlib

English

Conditioning a Nat-scaled function scales the conditional expectation by the Nat.

Русский

Условное ожидание от функции, умноженной на натуральное число, равно натуральному числу умноженному на условное ожидание.

LaTeX

$$$\mu[\mathrm{ofNat}(n) \cdot f|m] =^{\mathrm{ae}}_{\mu} \mathrm{ofNat}(n) \cdot \mu[f|m]$$$

Lean4

@[simp]
theorem condExp_ofNat (n : ℕ) [n.AtLeastTwo] (f : α → R) : μ[ofNat(n) * f|m] =ᵐ[μ] ofNat(n) * μ[f|m] := by
  simpa [Nat.cast_smul_eq_nsmul] using condExp_smul (μ := μ) (m := m) (n : ℝ) f

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