condExp_neg — Mathlib

English

The conditional expectation is linear: the conditional expectation of the negation of a function is the negation of its conditional expectation, a.e.

Русский

Условное ожидание является линейным: E[-f|m] = - E[f|m] почти наверняка.

LaTeX

$$$\mu[-f|m] =^{\mathrm{ae}}_{\mu} -\mu[f|m]$$$

Lean4

theorem condExp_neg (f : α → E) (m : MeasurableSpace α) : μ[-f|m] =ᵐ[μ] -μ[f|m] := by
  calc
    μ[-f|m] = μ[(-1 : ℝ) • f|m] := by rw [neg_one_smul ℝ f]
    _ =ᵐ[μ] (-1 : ℝ) • μ[f|m] := condExp_smul ..
    _ = -μ[f|m] := neg_one_smul ℝ (μ[f|m])

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