measure_preimage — Mathlib

English

For any measurable A, the probability of X landing in A equals μ(s ∩ A) divided by μ(s).

Русский

Для любого измеримого множества A вероятность того, что X попадёт в A, равна μ( s ∩ A ) / μ(s).

LaTeX

$$$\\mathbb{P}(X^{-1}(A))=\\dfrac{\\mu(s\\cap A)}{\\mu(s)}$ для измеримого A при μ(s) ≠ 0 и μ(s) ≠ ∞$$

Lean4

theorem measure_preimage {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞) (hu : IsUniform X s ℙ μ) {A : Set E}
    (hA : MeasurableSet A) : ℙ (X ⁻¹' A) = μ (s ∩ A) / μ s := by
  rwa [← map_apply_of_aemeasurable (hu.aemeasurable hns hnt) hA, hu, ProbabilityTheory.cond_apply',
    ENNReal.div_eq_inv_mul]

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