integral_eq — Mathlib

English

For X with law μ, P and AEStronglyMeasurable f, the integral with respect to P of f(X) equals the integral with respect to μ of f.

Русский

Для X с законом μ и P и AEStronglyMeasurable f справедливо интеграл по P от f(X) равен интегралу по μ от f.

LaTeX

$$$$ \\int f(X) \\, dP = \\int f \\, d\\mu $$$$

Lean4

theorem integral_eq {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E]
    {mE : MeasurableSpace E} [OpensMeasurableSpace E] {μ : Measure E} {X : Ω → E} (hX : HasLaw X μ P) :
    P[X] = ∫ x, x ∂μ := by
  rw [← Function.id_comp X, hX.integral_comp aestronglyMeasurable_id]
  simp

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