feat(Combinatorics/SimpleGraph/Bipartite): upper bound on the number of edges of a bipartite graph

Mathlib/Combinatorics/SimpleGraph/Bipartite.lean

@@ -445,4 +445,82 @@ theorem degree_le_between_add_compl (hw : w ∈ sᶜ) :
 
 end Between
 
+section
+
+variable {W₁ W₂ : Type*}
+
+theorem Sym2.eq_out (v : Sym2 V) : v = s(v.out.1, v.out.2) := Sym2.ext (by simp)
+
+theorem edgeSet_eq : G.edgeSet = { x | ∃ v w : V, x = s(v, w) ∧ G.Adj v w } := by
+  refine Set.ext fun x ↦ ⟨fun h ↦ ?_, by grind [mem_edgeSet]⟩
+  exact ⟨x.out.1, x.out.2, by simp [G.mem_edgeSet.mp <| Sym2.eq_out x ▸ h]⟩
+
+theorem completeBipartiteGraph_edgeSet : (completeBipartiteGraph W₁ W₂).edgeSet =
+    Set.range (fun x : W₁ × W₂ ↦ s(.inl x.1, .inr x.2)) := by
+  refine Set.ext fun x ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · simp only [edgeSet_eq, completeBipartiteGraph_adj, Sum.exists, Sum.isRight_inl,
+      Bool.false_eq_true, and_false, Sum.isLeft_inl, and_true, false_or, exists_and_right,
+      Sum.isRight_inr, Sum.isLeft_inr, or_false, Set.mem_setOf_eq] at h
+    rcases h with ⟨_, _, rfl⟩ | ⟨_, _, rfl⟩ <;> simp
+  · obtain ⟨_, _, _⟩ := h
+    simp
+
+theorem completeBipartiteGraph_edgeSet_encard :
+    (completeBipartiteGraph W₁ W₂).edgeSet.encard =
+    ENat.card W₁ * ENat.card W₂ := by
+  let g (x : W₁ × W₂) : Sym2 (W₁ ⊕ W₂) := s(.inl x.1, .inr x.2)
+  have : Function.Injective g := fun _ _ _ ↦ by grind
+  have := this.encard_image Set.univ
+  simpa [completeBipartiteGraph_edgeSet, this]
+
+theorem IsBipartiteWith.nonempty_embedding_completeBipartiteGraph_edgeSet
+    (hG : G.IsBipartiteWith s t) :
+    Nonempty (G.edgeSet ↪ (completeBipartiteGraph s t).edgeSet) := by
+  refine ⟨⟨fun ⟨x, hx⟩ ↦ ?_, fun _ _ _ ↦ ?_⟩⟩
+  · by_cases! h : x.out.1 ∈ s
+    · refine ⟨s(.inl ⟨x.out.1, h⟩, .inr ⟨x.out.2, ?_⟩), by simp⟩
+      grind [hG.disjoint, hG.mem_of_adj, edgeSet_eq, Sym2.eq_out]
+    · refine ⟨s(.inr ⟨x.out.1, ?_⟩, .inl ⟨x.out.2, ?_⟩), by simp⟩
+      · grind [hG.mem_of_adj <| G.mem_edgeSet.mpr <| Sym2.eq_out x ▸ hx]
+      · grind [hG.disjoint, hG.mem_of_adj, edgeSet_eq, Sym2.eq_out]
+  · grind [Sym2.eq_out]
+
+end
+
+section
+
+/-- An upper bound on the cardinality of the edge set of a bipartite graph when the vertex sets
+forming it may also be infinite: in that case as well, the upper bound is the product of
+the cardinalities of these two sets. The statement uses `Set.encard`. -/
+theorem IsBipartiteWith.encard_edgeSet_le (hG : G.IsBipartiteWith s t) :
+    G.edgeSet.encard ≤ s.encard * t.encard := by
+  grw [Classical.choice hG.nonempty_embedding_completeBipartiteGraph_edgeSet |>.encard_le,
+    completeBipartiteGraph_edgeSet_encard]
+  simp
+
+/-- An upper bound on the cardinality of the edge set of a bipartite graph when the cardinality
+of the entire vertex set of the graph is known. That is, the cardinality of the edge set times `4`
+is less or equal to the square of the cardinality of the vertex set.
+The statement uses `Set.encard` and `ENat.card`. -/
+theorem IsBipartite.four_mul_encard_edgeSet_le (h : G.IsBipartite) :
+    4 * G.edgeSet.encard ≤ ENat.card V ^ 2 := by
+  obtain ⟨s, t, h⟩ := isBipartite_iff_exists_isBipartiteWith.mp h
+  have hG := h.encard_edgeSet_le
+  have h₀ : s.encard + t.encard ≤ ENat.card V := by
+    rw [← Set.encard_union_eq h.disjoint]
+    exact Set.encard_le_card
+  by_cases! hv : Infinite V
+  · simp_all
+  rw [ENat.card_eq_coe_natCard V] at h₀ ⊢
+  rw [← s.toFinite.cast_ncard_eq, ← t.toFinite.cast_ncard_eq] at hG h₀
+  rw [← G.edgeSet.toFinite.cast_ncard_eq] at hG ⊢
+  norm_cast at *
+  have h₂ : (s.ncard + t.ncard) ^ 2 ≤ Nat.card V ^ 2 :=
+    Nat.pow_le_pow_left h₀ 2
+  have h₃ : 4 * s.ncard * t.ncard ≤ (s.ncard + t.ncard) ^ 2 :=
+    four_mul_le_pow_two_add s.ncard t.ncard
+  lia
+
+end
+
 end SimpleGraph