eventCount

formal source

 115/-! ## Resolution Count -/
 116
 117/-- Count of distinct events in a neighborhood (when finite) -/
 118noncomputable def eventCount (U : Set C) (hfin : (r.R '' U).Finite) : ℕ :=
 119  hfin.toFinset.card
 120
 121/-- Event count is positive when the neighborhood is nonempty -/
 122theorem eventCount_pos (c : C) (U : Set C) (hU : U ∈ L.N c)
 123    (hfin : (r.R '' U).Finite) :
 124    0 < eventCount r U hfin := by
 125  unfold eventCount
 126  have hc : c ∈ U := L.mem_of_mem_N c U hU
 127  have hne : (r.R '' U).Nonempty := ⟨r.R c, ⟨c, hc, rfl⟩⟩
 128  exact Finset.card_pos.mpr ((Set.Finite.toFinset_nonempty hfin).mpr hne)
 129
 130/-! ## Resolution Bound -/
 131
 132/-- Given a finite set of events, count them -/
 133noncomputable def eventCountFinite (S : Set E) (hfin : S.Finite) : ℕ :=
 134  hfin.toFinset.card
 135
 136/-- Event count is positive for nonempty sets -/
 137theorem eventCountFinite_pos (S : Set E) (hfin : S.Finite) (hne : S.Nonempty) :
 138    0 < eventCountFinite S hfin := by
 139  unfold eventCountFinite
 140  exact Finset.card_pos.mpr ((Set.Finite.toFinset_nonempty hfin).mpr hne)
 141
 142/-- Finite resolution neighborhoods have positive event count -/
 143theorem finite_resolution_pos (c : C) (h : HasFiniteLocalResolution L r c) :
 144    ∃ U ∈ L.N c, ∃ hfin : (r.R '' U).Finite, 0 < eventCountFinite (r.R '' U) hfin := by
 145  obtain ⟨U, hU, hfin⟩ := h
 146  use U, hU, hfin
 147  apply eventCountFinite_pos
 148  exact ⟨r.R c, c, L.mem_of_mem_N c U hU, rfl⟩