[Merged by Bors] - feat(combinatorics/simple_graph/srg): is_SRG_with for complete graphs, edgeless graphs, and complements

src/combinatorics/simple_graph/basic.lean

@@ -145,6 +145,9 @@ protected lemma adj.ne {G : simple_graph V} {a b : V} (h : G.adj a b) : a ≠ b
 
 protected lemma adj.ne' {G : simple_graph V} {a b : V} (h : G.adj a b) : b ≠ a := h.ne.symm
 
+lemma ne_of_adj_of_not_adj {v w x : V} (h : G.adj v x) (hn : ¬ G.adj w x) : v ≠ w :=
+λ h', hn (h' ▸ h)
+
 section order
 
 /-- The relation that one `simple_graph` is a subgraph of another.
@@ -278,7 +281,7 @@ def edge_set : set (sym2 V) := sym2.from_rel G.symm
 @[simp] lemma mem_edge_set : ⟦(v, w)⟧ ∈ G.edge_set ↔ G.adj v w := iff.rfl
 
 /--
-Two vertices are adjacent iff there is an edge between them.  The
+Two vertices are adjacent iff there is an edge between them. The
 condition `v ≠ w` ensures they are different endpoints of the edge,
 which is necessary since when `v = w` the existential
 `∃ (e ∈ G.edge_set), v ∈ e ∧ w ∈ e` is satisfied by every edge
@@ -450,6 +453,10 @@ instance decidable_mem_common_neighbors [decidable_rel G.adj] (v w : V) :
   decidable_pred (∈ G.common_neighbors v w) :=
 λ a, and.decidable
 
+lemma common_neighbors_top_eq {v w : V} :
+  (⊤ : simple_graph V).common_neighbors v w = set.univ \ {v, w} :=
+by { ext u, simp [common_neighbors, eq_comm, not_or_distrib.symm] }
+
 section incidence
 variable [decidable_eq V]
 
@@ -503,6 +510,8 @@ locally finite at `v`.
 -/
 def neighbor_finset : finset V := (G.neighbor_set v).to_finset
 
+lemma neighbor_finset_def : G.neighbor_finset v = (G.neighbor_set v).to_finset := rfl
+
 @[simp] lemma mem_neighbor_finset (w : V) :
   w ∈ G.neighbor_finset v ↔ G.adj v w :=
 set.mem_to_finset
@@ -562,11 +571,14 @@ A locally finite simple graph is regular of degree `d` if every vertex has degre
 -/
 def is_regular_of_degree (d : ℕ) : Prop := ∀ (v : V), G.degree v = d
 
-lemma is_regular_of_degree_eq {d : ℕ} (h : G.is_regular_of_degree d) (v : V) : G.degree v = d := h v
+variables {G}
+
+lemma is_regular_of_degree.degree_eq {d : ℕ} (h : G.is_regular_of_degree d) (v : V) :
+  G.degree v = d := h v
 
-lemma is_regular_compl_of_is_regular [fintype V] [decidable_eq V]
-  (G : simple_graph V) [decidable_rel G.adj]
-  (k : ℕ) (h : G.is_regular_of_degree k) :
+lemma is_regular_of_degree.compl [fintype V] [decidable_eq V]
+  {G : simple_graph V} [decidable_rel G.adj]
+  {k : ℕ} (h : G.is_regular_of_degree k) :
   Gᶜ.is_regular_of_degree (fintype.card V - 1 - k) :=
 by { intro v, rw [degree_compl, h v] }
 
@@ -583,6 +595,11 @@ lemma neighbor_finset_eq_filter {v : V} [decidable_rel G.adj] :
   G.neighbor_finset v = finset.univ.filter (G.adj v) :=
 by { ext, simp }
 
+lemma neighbor_finset_compl [decidable_eq V] [decidable_rel G.adj] (v : V) :
+  Gᶜ.neighbor_finset v = (G.neighbor_finset v)ᶜ \ {v} :=
+by simp only [neighbor_finset, neighbor_set_compl, set.to_finset_sdiff, set.to_finset_compl,
+    set.to_finset_singleton]
+
 @[simp]
 lemma complete_graph_degree [decidable_eq V] (v : V) :
   (⊤ : simple_graph V).degree v = fintype.card V - 1 :=
@@ -591,7 +608,13 @@ begin
   erw [degree, neighbor_finset_eq_filter, filter_ne, card_erase_of_mem (mem_univ v)],
 end
 
-lemma complete_graph_is_regular [decidable_eq V] :
+lemma bot_degree (v : V) : (⊥ : simple_graph V).degree v = 0 :=
+begin
+  erw [degree, neighbor_finset_eq_filter, filter_false],
+  exact finset.card_empty,
+end
+
+lemma is_regular_of_degree.top [decidable_eq V] :
   (⊤ : simple_graph V).is_regular_of_degree (fintype.card V - 1) :=
 by { intro v, simp }
 
@@ -632,11 +655,7 @@ defined to be a natural.
 lemma le_min_degree_of_forall_le_degree [decidable_rel G.adj] [nonempty V] (k : ℕ)
   (h : ∀ v, k ≤ G.degree v) :
   k ≤ G.min_degree :=
-begin
-  rcases G.exists_minimal_degree_vertex with ⟨v, hv⟩,
-  rw hv,
-  apply h
-end
+by { rcases G.exists_minimal_degree_vertex with ⟨v, hv⟩, rw hv, apply h }
 
 /--
 The maximum degree of all vertices (and `0` if there are no vertices).
@@ -750,6 +769,18 @@ begin
       exact G.common_neighbors_subset_neighbor_set_left _ _ } }
 end
 
+lemma card_common_neighbors_top [decidable_eq V] {v w : V} (h : v ≠ w) :
+  fintype.card ((⊤ : simple_graph V).common_neighbors v w) = fintype.card V - 2 :=
+begin
+  simp only [common_neighbors_top_eq, ← set.to_finset_card, set.to_finset_sdiff],
+  rw finset.card_sdiff,
+  { congr' 1,
+    { simp_rw [← finset.card_univ, ← set.to_finset_univ],
+      congr, },
+    { simp [h], } },
+  { simp only [←set.subset_iff_to_finset_subset, set.subset_univ] },
+end
+
 end finite
 
 section maps

src/combinatorics/simple_graph/strongly_regular.lean

@@ -10,58 +10,162 @@ import data.set.finite
 
 ## Main definitions
 
-* `G.is_SRG_of n k l m` (see `is_simple_graph.is_SRG_of`) is a structure for a `simple_graph`
-  satisfying the following conditions:
+* `G.is_SRG_with n k ℓ μ` (see `simple_graph.is_SRG_with`) is a structure for
+  a `simple_graph` satisfying the following conditions:
   * The cardinality of the vertex set is `n`
   * `G` is a regular graph with degree `k`
-  * The number of common neighbors between any two adjacent vertices in `G` is `l`
-  * The number of common neighbors between any two nonadjacent vertices in `G` is `m`
+  * The number of common neighbors between any two adjacent vertices in `G` is `ℓ`
+  * The number of common neighbors between any two nonadjacent vertices in `G` is `μ`
 
 ## TODO
-- Prove that the complement of a strongly regular graph is strongly regular with parameters
-  `is_SRG_of n (n - k - 1) (n - 2 - 2k + m) (v - 2k + l)`
 - Prove that the parameters of a strongly regular graph
-  obey the relation `(n - k - 1) * m = k * (k - l - 1)`
+  obey the relation `(n - k - 1) * μ = k * (k - ℓ - 1)`
 - Prove that if `I` is the identity matrix and `J` is the all-one matrix,
-  then the adj matrix `A` of SRG obeys relation `A^2 = kI + lA + m(J - I - A)`
+  then the adj matrix `A` of SRG obeys relation `A^2 = kI + ℓA + μ(J - I - A)`
 -/
 
+open finset
+
 universes u
 
 namespace simple_graph
 variables {V : Type u}
-variables (G : simple_graph V) [decidable_rel G.adj]
-
 variables [fintype V] [decidable_eq V]
+variables (G : simple_graph V) [decidable_rel G.adj]
 
 /--
-A graph is strongly regular with parameters `n k l m` if
+A graph is strongly regular with parameters `n k ℓ μ` if
  * its vertex set has cardinality `n`
  * it is regular with degree `k`
- * every pair of adjacent vertices has `l` common neighbors
- * every pair of nonadjacent vertices has `m` common neighbors
+ * every pair of adjacent vertices has `ℓ` common neighbors
+ * every pair of nonadjacent vertices has `μ` common neighbors
 -/
-structure is_SRG_of (n k l m : ℕ) : Prop :=
+structure is_SRG_with (n k ℓ μ : ℕ) : Prop :=
 (card : fintype.card V = n)
 (regular : G.is_regular_of_degree k)
-(adj_common : ∀ (v w : V), G.adj v w → fintype.card (G.common_neighbors v w) = l)
-(nadj_common : ∀ (v w : V), ¬ G.adj v w ∧ v ≠ w → fintype.card (G.common_neighbors v w) = m)
+(of_adj : ∀ (v w : V), G.adj v w → fintype.card (G.common_neighbors v w) = ℓ)
+(of_not_adj : ∀ (v w : V), v ≠ w → ¬G.adj v w → fintype.card (G.common_neighbors v w) = μ)
 
-open finset
+variables {G} {n k ℓ μ : ℕ}
+
+/-- Empty graphs are strongly regular. Note that `ℓ` can take any value
+  for empty graphs, since there are no pairs of adjacent vertices. -/
+lemma bot_strongly_regular :
+  (⊥ : simple_graph V).is_SRG_with (fintype.card V) 0 ℓ 0 :=
+{ card := rfl,
+  regular := bot_degree,
+  of_adj := λ v w h, h.elim,
+  of_not_adj := λ v w h, begin
+    simp only [card_eq_zero, filter_congr_decidable, fintype.card_of_finset, forall_true_left,
+      not_false_iff, bot_adj],
+    ext,
+    simp [mem_common_neighbors],
+  end }
 
-/-- Complete graphs are strongly regular. Note that the parameter `m` can take any value
-  for complete graphs, since there are no distinct pairs of nonadjacent vertices. -/
-lemma complete_strongly_regular (m : ℕ) :
-  (⊤ : simple_graph V).is_SRG_of (fintype.card V) (fintype.card V - 1) (fintype.card V - 2) m :=
+/-- Complete graphs are strongly regular. Note that `μ` can take any value
+  for complete graphs, since there are no distinct pairs of non-adjacent vertices. -/
+lemma is_SRG_with.top :
+  (⊤ : simple_graph V).is_SRG_with (fintype.card V) (fintype.card V - 1) (fintype.card V - 2) μ :=
 { card := rfl,
-  regular := complete_graph_degree,
-  adj_common := λ v w (h : v ≠ w),
-    begin
-      simp only [fintype.card_of_finset, mem_common_neighbors, filter_not, ←not_or_distrib,
-                 filter_eq, filter_or, card_univ_diff, mem_univ, if_pos, ←insert_eq, top_adj],
-      rw [card_insert_of_not_mem, card_singleton],
-      simp [h]
-    end,
-  nadj_common := λ v w (h : ¬(v ≠ w) ∧ _), (h.1 h.2).elim }
+  regular := is_regular_of_degree.top,
+  of_adj := λ v w h, begin
+    rw card_common_neighbors_top,
+    exact h,
+  end,
+  of_not_adj := λ v w h h', false.elim $ by simpa using h }
+
+lemma is_SRG_with.card_neighbor_finset_union_eq {v w : V} (h : G.is_SRG_with n k ℓ μ) :
+  (G.neighbor_finset v ∪ G.neighbor_finset w).card =
+    2 * k - fintype.card (G.common_neighbors v w) :=
+begin
+  apply @nat.add_right_cancel _ (fintype.card (G.common_neighbors v w)),
+  rw [nat.sub_add_cancel, ← set.to_finset_card],
+  { simp [neighbor_finset, common_neighbors, set.to_finset_inter, finset.card_union_add_card_inter,
+      h.regular.degree_eq, two_mul], },
+  { apply le_trans (card_common_neighbors_le_degree_left _ _ _),
+    simp [h.regular.degree_eq, two_mul], },
+end
+
+/-- Assuming `G` is strongly regular, `2*(k + 1) - m` in `G` is the number of vertices that are
+  adjacent to either `v` or `w` when `¬G.adj v w`. So it's the cardinality of
+  `G.neighbor_set v ∪ G.neighbor_set w`. -/
+lemma is_SRG_with.card_neighbor_finset_union_of_not_adj {v w : V} (h : G.is_SRG_with n k ℓ μ)
+  (hne : v ≠ w) (ha : ¬G.adj v w) :
+  (G.neighbor_finset v ∪ G.neighbor_finset w).card = 2 * k - μ :=
+begin
+  rw ← h.of_not_adj v w hne ha,
+  apply h.card_neighbor_finset_union_eq,
+end
+
+lemma is_SRG_with.card_neighbor_finset_union_of_adj {v w : V} (h : G.is_SRG_with n k ℓ μ)
+  (ha : G.adj v w) :
+  (G.neighbor_finset v ∪ G.neighbor_finset w).card = 2 * k - ℓ :=
+begin
+  rw ← h.of_adj v w ha,
+  apply h.card_neighbor_finset_union_eq,
+end
+
+lemma compl_neighbor_finset_sdiff_inter_eq {v w : V} :
+  (G.neighbor_finset v)ᶜ \ {v} ∩ ((G.neighbor_finset w)ᶜ \ {w}) =
+    (G.neighbor_finset v)ᶜ ∩ (G.neighbor_finset w)ᶜ \ ({w} ∪ {v}) :=
+by { ext, rw ← not_iff_not, simp [imp_iff_not_or, or_assoc, or_comm, or.left_comm], }
+
+lemma sdiff_compl_neighbor_finset_inter_eq {v w : V} (h : G.adj v w) :
+  (G.neighbor_finset v)ᶜ ∩ (G.neighbor_finset w)ᶜ \ ({w} ∪ {v}) =
+    (G.neighbor_finset v)ᶜ ∩ (G.neighbor_finset w)ᶜ :=
+begin
+  ext,
+  simp only [and_imp, mem_union, mem_sdiff, mem_compl, and_iff_left_iff_imp,
+    mem_neighbor_finset, mem_inter, mem_singleton],
+  rintros hnv hnw (rfl|rfl),
+  { exact hnv h, },
+  { apply hnw, rwa adj_comm, },
+end
+
+lemma is_SRG_with.compl_is_regular (h : G.is_SRG_with n k ℓ μ) :
+  Gᶜ.is_regular_of_degree (n - k - 1) :=
+begin
+  rw [← h.card, nat.sub_sub, add_comm, ←nat.sub_sub],
+  exact h.regular.compl,
+end
+
+lemma is_SRG_with.card_common_neighbors_eq_of_adj_compl (h : G.is_SRG_with n k ℓ μ)
+  {v w : V} (ha : Gᶜ.adj v w) :
+  fintype.card ↥(Gᶜ.common_neighbors v w) = n - (2 * k - μ) - 2 :=
+begin
+  simp only [←set.to_finset_card, common_neighbors, set.to_finset_inter, neighbor_set_compl,
+    set.to_finset_sdiff, set.to_finset_singleton, set.to_finset_compl, ←neighbor_finset_def],
+  simp_rw compl_neighbor_finset_sdiff_inter_eq,
+  have hne : v ≠ w := ne_of_adj _ ha,
+  rw compl_adj at ha,
+  rw [card_sdiff, ← insert_eq, card_insert_of_not_mem, card_singleton, ← finset.compl_union],
+  { change (1 + 1) with 2,
+    rw [card_compl, h.card_neighbor_finset_union_of_not_adj hne ha.2, ← h.card], },
+  { simp only [hne.symm, not_false_iff, mem_singleton], },
+  { intro u,
+    simp only [mem_union, mem_compl, mem_neighbor_finset, mem_inter, mem_singleton],
+    rintro (rfl|rfl);
+    simpa [adj_comm] using ha.2, },
+end
+
+lemma is_SRG_with.card_common_neighbors_eq_of_not_adj_compl (h : G.is_SRG_with n k ℓ μ)
+  {v w : V} (hn : v ≠ w) (hna : ¬Gᶜ.adj v w)  :
+  fintype.card ↥(Gᶜ.common_neighbors v w) = n - (2 * k - ℓ) :=
+begin
+  simp only [←set.to_finset_card, common_neighbors, set.to_finset_inter, neighbor_set_compl,
+    set.to_finset_sdiff, set.to_finset_singleton, set.to_finset_compl, ←neighbor_finset_def],
+  simp only [not_and, not_not, compl_adj] at hna,
+  have h2' := hna hn,
+  simp_rw [compl_neighbor_finset_sdiff_inter_eq, sdiff_compl_neighbor_finset_inter_eq h2'],
+  rwa [← finset.compl_union, card_compl, h.card_neighbor_finset_union_of_adj, ← h.card],
+end
+
+/-- The complement of a strongly regular graph is strongly regular. -/
+lemma is_SRG_with.compl (h : G.is_SRG_with n k ℓ μ) :
+  Gᶜ.is_SRG_with n (n - k - 1) (n - (2 * k - μ) - 2) (n - (2 * k - ℓ)) :=
+{ card := h.card,
+  regular := h.compl_is_regular,
+  of_adj := λ v w ha, h.card_common_neighbors_eq_of_adj_compl ha,
+  of_not_adj := λ v w hn hna, h.card_common_neighbors_eq_of_not_adj_compl hn hna, }
 
 end simple_graph

src/data/fintype/basic.lean

@@ -142,7 +142,13 @@ set.ext $ λ x, mem_compl
 
 @[simp] lemma compl_empty : (∅ : finset α)ᶜ = univ := compl_bot
 
-@[simp] lemma union_compl (s : finset α) : s ∪ sᶜ = finset.univ := sup_compl_eq_top
+@[simp] lemma union_compl (s : finset α) : s ∪ sᶜ = univ := sup_compl_eq_top
+
+@[simp] lemma inter_compl (s : finset α) : s ∩ sᶜ = ∅ := inf_compl_eq_bot
+
+@[simp] lemma compl_union (s t : finset α) : (s ∪ t)ᶜ = sᶜ ∩ tᶜ := compl_sup
+
+@[simp] lemma compl_inter (s t : finset α) : (s ∩ t)ᶜ = sᶜ ∪ tᶜ := compl_inf
 
 @[simp] lemma compl_erase : (s.erase a)ᶜ = insert a sᶜ :=
 by { ext, simp only [or_iff_not_imp_left, mem_insert, not_and, mem_compl, mem_erase] }

src/data/set/finite.lean

@@ -215,6 +215,8 @@ fintype.card_of_subsingleton _
 lemma subsingleton.finite {s : set α} (h : s.subsingleton) : finite s :=
 h.induction_on finite_empty finite_singleton
 
+lemma to_finset_singleton (a : α) : ({a} : set α).to_finset = {a} := rfl
+
 lemma finite_is_top (α : Type*) [partial_order α] : finite {x : α | is_top x} :=
 (subsingleton_is_top α).finite
 
@@ -756,6 +758,15 @@ lemma to_finset_union {α : Type*} [decidable_eq α] (s t : set α) [fintype (s
   [fintype s] [fintype t] : (s ∪ t).to_finset = s.to_finset ∪ t.to_finset :=
 by ext; simp
 
+instance fintype_sdiff  {α : Type*} [decidable_eq α]
+  (s t : set α) [fintype s] [fintype t] :
+  fintype (s \ t : set α) :=
+fintype.of_finset (s.to_finset \ t.to_finset) $ by simp
+
+lemma to_finset_sdiff {α : Type*} [decidable_eq α] (s t : set α) [fintype s] [fintype t]
+  [fintype (s \ t : set α)] : (s \ t).to_finset = s.to_finset \ t.to_finset :=
+by ext; simp
+
 lemma to_finset_ne_eq_erase {α : Type*} [decidable_eq α] [fintype α] (a : α)
   [fintype {x : α | x ≠ a}] : {x : α | x ≠ a}.to_finset = finset.univ.erase a :=
 by ext; simp

src/measure_theory/measure/outer_measure.lean

@@ -702,7 +702,7 @@ lemma is_caratheodory_Union_lt {s : ℕ → set α} :
 
 lemma is_caratheodory_inter (h₁ : is_caratheodory s₁) (h₂ : is_caratheodory s₂) :
   is_caratheodory (s₁ ∩ s₂) :=
-by { rw [← is_caratheodory_compl_iff, compl_inter],
+by { rw [← is_caratheodory_compl_iff, set.compl_inter],
   exact is_caratheodory_union _ (is_caratheodory_compl _ h₁) (is_caratheodory_compl _ h₂) }
 
 lemma is_caratheodory_sum {s : ℕ → set α} (h : ∀i, is_caratheodory (s i))