English
For PMF p and a, p(a) = 1 iff supp(p) = {a}.
Русский
Для PMF p и a верно: p(a) = 1 тогда когда опора p равна {a}.
LaTeX
$$$ p(a) = 1 \iff \mathrm{supp}(p) = \{ a \} $$$
Lean4
theorem apply_eq_one_iff (p : PMF α) (a : α) : p a = 1 ↔ p.support = { a } :=
by
refine
⟨fun h =>
Set.Subset.antisymm (fun a' ha' => by_contra fun ha => ?_) fun a' ha' =>
ha'.symm ▸ (p.mem_support_iff a).2 fun ha => zero_ne_one <| ha.symm.trans h,
fun h =>
_root_.trans (symm <| tsum_eq_single a fun a' ha' => (p.apply_eq_zero_iff a').2 (h.symm ▸ ha')) p.tsum_coe⟩
suffices 1 < ∑' a, p a from ne_of_lt this p.tsum_coe.symm
classical
have : 0 < ∑' b, ite (b = a) 0 (p b) :=
lt_of_le_of_ne' zero_le'
(ENNReal.summable.tsum_ne_zero_iff.2 ⟨a', ite_ne_left_iff.2 ⟨ha, Ne.symm <| (p.mem_support_iff a').2 ha'⟩⟩)
calc
1 = 1 + 0 := (add_zero 1).symm
_ < p a + ∑' b, ite (b = a) 0 (p b) := (ENNReal.add_lt_add_of_le_of_lt ENNReal.one_ne_top (le_of_eq h.symm) this)
_ = ite (a = a) (p a) 0 + ∑' b, ite (b = a) 0 (p b) := by rw [eq_self_iff_true, if_true]
_ = (∑' b, ite (b = a) (p b) 0) + ∑' b, ite (b = a) 0 (p b) :=
by
congr
exact symm (tsum_eq_single a fun b hb => if_neg hb)
_ = ∑' b, (ite (b = a) (p b) 0 + ite (b = a) 0 (p b)) := ENNReal.tsum_add.symm
_ = ∑' b, p b := tsum_congr fun b => by split_ifs <;> simp only [zero_add, add_zero]
