cond_cond_eq_cond_inter' — Mathlib

English

If S is measurable and μ(S) ≠ ∞, then μ[|S][|T] = μ[|S ∩ T].

Русский

Если S измеримо и μ(S) ≠ ∞, то условное повторное условие равно условному на пересечение.

LaTeX

$$$\\text{MeasurableSet}(S) \\;\\land\\; μ(S) \\neq \\infty \\Rightarrow μ[|S][|T] = μ[|S \\cap T]$$$

Lean4

theorem cond_cond_eq_cond_inter' (hms : MeasurableSet s) (hmt : MeasurableSet t) (hcs : μ s ≠ ∞) :
    μ[|s][|t] = μ[|s ∩ t] := by
  ext u
  obtain hst | hst := eq_or_ne (μ (s ∩ t)) 0
  · have : μ (s ∩ t ∩ u) = 0 := measure_mono_null Set.inter_subset_left hst
    simp [cond_apply, *, ← Set.inter_assoc]
  · have hs : μ s ≠ 0 := (measure_pos_of_superset Set.inter_subset_left hst).ne'
    simp [*, hms.inter hmt, cond_apply, ← Set.inter_assoc, ENNReal.mul_inv, ← mul_assoc, mul_comm _ (μ s)⁻¹,
      ENNReal.inv_mul_cancel]

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