English
The mass value at any point is not infinite: p(a) ≠ ∞.
Русский
Масса в любой точке не равна бесконечности: p(a) ≠ ∞.
LaTeX
$$$ p(a) \neq \infty $$$
Lean4
theorem toOuterMeasure_apply_eq_one_iff : p.toOuterMeasure s = 1 ↔ p.support ⊆ s :=
by
refine (p.toOuterMeasure_apply s).symm ▸ ⟨fun h a hap => ?_, fun h => ?_⟩
· refine by_contra fun hs => ne_of_lt ?_ (h.trans p.tsum_coe.symm)
have hs' : s.indicator p a = 0 := Set.indicator_apply_eq_zero.2 fun hs' => False.elim <| hs hs'
have hsa : s.indicator p a < p a := hs'.symm ▸ (p.apply_pos_iff a).2 hap
exact ENNReal.tsum_lt_tsum (p.tsum_coe_indicator_ne_top s) (fun x => Set.indicator_apply_le fun _ => le_rfl) hsa
· classical
suffices ∀ (x) (_ : x ∉ s), p x = 0 from
_root_.trans (tsum_congr fun a => (Set.indicator_apply s p a).trans (ite_eq_left_iff.2 <| symm ∘ this a))
p.tsum_coe
exact fun a ha => (p.apply_eq_zero_iff a).2 <| Set.notMem_subset h ha
