card_singleton

formal source

  68        have hy_union : y ∈ (ballFS (α:=α) x n).biUnion (fun z => B.neighbors z) :=
  69          Finset.mem_biUnion.mpr ⟨z, hz', hstep'⟩
  70        exact Finset.mem_union.mpr (Or.inr hy_union)
  71theorem card_singleton {x : α} : ({x} : Finset α).card = 1 :=
  72  Finset.card_singleton x
  73theorem card_union_le (s t : Finset α) : (s ∪ t).card ≤ s.card + t.card :=
  74  Finset.card_union_le s t
  75theorem card_bind_le_sum (s : Finset α) (f : α → Finset α) :
  76  (s.biUnion f).card ≤ Finset.sum s (fun z => (f z).card) :=
  77  Finset.card_biUnion_le
  78theorem sum_card_neighbors_le (s : Finset α) :
  79  Finset.sum s (fun z => (B.neighbors z).card) ≤ d * s.card := by
  80  have h1 : Finset.sum s (fun z => (B.neighbors z).card) ≤ Finset.sum s (fun _ => d) := by
  81    apply Finset.sum_le_sum
  82    intro z _
  83    exact B.degree_bound_holds z
  84  have h2 : Finset.sum s (fun _ => d) = s.card * d := by
  85    simp [Finset.sum_const]
  86  rw [h2, Nat.mul_comm] at h1
  87  exact h1
  88theorem card_bind_neighbors_le (s : Finset α) :
  89  (s.biUnion (fun z => B.neighbors z)).card ≤ d * s.card := by
  90  have h1 := card_bind_le_sum s (fun z => B.neighbors z)
  91  have h2 := sum_card_neighbors_le s
  92  exact Nat.le_trans h1 h2
  93theorem card_ballFS_succ_le (x : α) (n : Nat) :
  94  (ballFS (α:=α) x (n+1)).card ≤ (1 + d) * (ballFS (α:=α) x n).card := by
  95  dsimp [ballFS]
  96  let prev := ballFS (α:=α) x n
  97  let new_neighbors := prev.biUnion (fun z => B.neighbors z)
  98  have h_union := card_union_le prev new_neighbors
  99  have h_neighbors := card_bind_neighbors_le prev
 100  have h_combined : (prev ∪ new_neighbors).card ≤ prev.card + d * prev.card :=
 101    Nat.le_trans h_union (Nat.add_le_add_left h_neighbors prev.card)