measure_eq_zero_or_one_or_top_of_indepSet_self

English

If s is an independent family of sets, then the family of indicator functions 1_{s_n} is independent in the iIndepFun sense with respect to κ and μ.

Русский

Если семейство множеств независимo, то семейство индикаторных функций 1_{s_n} является независимым в смысле iIndepFun относительно κ и μ.

LaTeX

$$$\\text{iIndepFun}\\left(n \\mapsto (s_n).indicator 1\\right)\\kappa\\mu$$$

Lean4

theorem measure_eq_zero_or_one_or_top_of_indepSet_self {t : Set Ω} (h_indep : Kernel.IndepSet t t κ μα) :
    ∀ᵐ a ∂μα, κ a t = 0 ∨ κ a t = 1 ∨ κ a t = ∞ :=
  by
  specialize
    h_indep t t (measurableSet_generateFrom (Set.mem_singleton t)) (measurableSet_generateFrom (Set.mem_singleton t))
  filter_upwards [h_indep] with a ha
  by_cases h0 : κ a t = 0
  · exact Or.inl h0
  by_cases h_top : κ a t = ∞
  · exact Or.inr (Or.inr h_top)
  rw [← one_mul (κ a (t ∩ t)), Set.inter_self, ENNReal.mul_left_inj h0 h_top] at ha
  exact Or.inr (Or.inl ha.symm)

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