/-! # A counterexample to Erdős problem 108 For every chromatic threshold, we construct an arc graph exceeding that threshold whose four-cycle-free subgraphs are six-colorable. Taking girth five and chromatic number seven therefore disproves the assertion in the target. The base graph is obtained by finite counting in a multipartite random model. Its parts have explicitly chosen sizes. All probability estimates, coloring arguments, and the lift to arbitrary universes are proved below. -/ open SimpleGraph universe u section ArcGraph variable {V : Type u} [LinearOrder V] /-- Edges directed from their smaller endpoint to their larger endpoint. -/ abbrev Arc (F : SimpleGraph V) := {e : V × V // e.1 < e.2 ∧ F.Adj e.1 e.2} /-- The undirected graph on concatenating directed edges. -/ def arcGraph (F : SimpleGraph V) : SimpleGraph (Arc F) where Adj a b := a.1.2 = b.1.1 ∨ b.1.2 = a.1.1 symm := ⟨fun _ _ => Or.symm⟩ loopless := ⟨fun a h => (ne_of_lt a.2.1) (h.elim Eq.symm Eq.symm)⟩ /-- The colors appearing on edges directed out of a vertex. -/ def outgoingColors {F : SimpleGraph V} {α : Type*} (c : (arcGraph F).Coloring α) (v : V) : Set α := {i | ∃ a : Arc F, a.1.1 = v ∧ c a = i} theorem outgoingColors_ne {F : SimpleGraph V} {α : Type*} (c : (arcGraph F).Coloring α) (a : Arc F) : outgoingColors c a.1.1 ≠ outgoingColors c a.1.2 := by intro h have hm : c a ∈ outgoingColors c a.1.1 := ⟨a, rfl, rfl⟩ rw [h] at hm obtain ⟨b, hb, hbc⟩ := hm exact c.valid (Or.inl hb.symm) hbc.symm /-- A coloring of the arc graph gives a set-valued coloring of the base graph. -/ def baseColoring {F : SimpleGraph V} {α : Type*} (c : (arcGraph F).Coloring α) : F.Coloring (Set α) := SimpleGraph.Coloring.mk (outgoingColors c) fun {x y} hxy => by rcases lt_or_gt_of_ne hxy.ne with hlt | hgt · exact outgoingColors_ne c ⟨(x, y), hlt, hxy⟩ · exact (outgoingColors_ne c ⟨(y, x), hgt, hxy.symm⟩).symm /-- Lemma 2 of the attachment, stated without natural-valued chromatic numbers. -/ theorem base_colorable_of_arc_colorable {F : SimpleGraph V} {t : ℕ} (h : (arcGraph F).Colorable t) : F.Colorable (2 ^ t) := by obtain ⟨c⟩ := h simpa using (baseColoring c).colorable end ArcGraph /-- Absence of a four-cycle, allowing arbitrary deletions of edges. -/ def FourCycleFree {V : Type*} (H : SimpleGraph V) : Prop := ∀ a b x y, a ≠ b → x ≠ y → H.Adj a x → H.Adj a y → H.Adj b x → H.Adj b y → False theorem fourCycleFree_of_girth_ge_five {V : Type*} {H : SimpleGraph V} (hg : 5 ≤ H.girth) : FourCycleFree H := by intro a b x y hab hxy hax hay hbx hby let w : H.Walk a a := .cons hax (.cons hbx.symm (.cons hby (.cons hay.symm .nil))) have hw : w.IsCycle := { edges_nodup := by simp [w, hab, hab.symm, hxy, hax.ne, hay.ne, hby.ne] ne_nil := by simp [w] support_nodup := by simp [w, hab.symm, hxy, hax.ne.symm, hay.ne.symm, hbx.ne.symm, hby.ne] } have hle := H.girth_le_length hw have hlen : w.length = 4 := rfl omega /-- Distinct vertices with two neighbors in `T` require distinct neighbor pairs. -/ theorem card_le_choose_two_of_fourCycleFree {V : Type*} {H : SimpleGraph V} (h4 : FourCycleFree H) (S T : Finset V) (hS : ∀ a ∈ S, ∃ x ∈ T, ∃ y ∈ T, x ≠ y ∧ H.Adj a x ∧ H.Adj a y) : S.card ≤ T.card.choose 2 := by classical have hpair : ∀ a : S, ∃ p : T.powersetCard 2, ∀ x ∈ p.1, H.Adj a.1 x := by intro a obtain ⟨x, hx, y, hy, hxy, hax, hay⟩ := hS a.1 a.2 refine ⟨⟨{x, y}, ?_⟩, ?_⟩ · refine Finset.mem_powersetCard.mpr ⟨?_, by simp [hxy]⟩ intro z hz rcases Finset.mem_insert.mp hz with rfl | hz · exact hx · simpa only [Finset.mem_singleton.mp hz] using hy · intro z hz simp only [Finset.mem_insert, Finset.mem_singleton] at hz rcases hz with rfl | rfl · exact hax · exact hay choose p hp using hpair have hinj : Function.Injective p := by intro a b heq apply Subtype.ext by_contra hab have hcard : (p a).1.card = 2 := (Finset.mem_powersetCard.mp (p a).2).2 obtain ⟨x, hx, y, hy, hxy⟩ := Finset.one_lt_card.mp (show 1 < (p a).1.card by omega) have hx' : x ∈ (p b).1 := by simpa only [heq] using hx have hy' : y ∈ (p b).1 := by simpa only [heq] using hy exact h4 a b x y hab hxy (hp a x hx) (hp a y hy) (hp b x hx') (hp b y hy') simpa using Fintype.card_le_of_injective p hinj section Selection variable {V : Type u} [LinearOrder V] {F : SimpleGraph V} /-- An arc vertex with at least two distinct outgoing neighbors in `H`. -/ def Branching (H : SimpleGraph (Arc F)) (a : Arc F) : Prop := ∃ b c : Arc F, b ≠ c ∧ H.Adj a b ∧ H.Adj a c ∧ a.1.2 = b.1.1 ∧ a.1.2 = c.1.1 /-- The base graph whose directed edges are the members of `S`. -/ def baseOfArcs (S : Set (Arc F)) : SimpleGraph V where Adj x y := ∃ a ∈ S, (a.1.1 = x ∧ a.1.2 = y) ∨ (a.1.1 = y ∧ a.1.2 = x) symm := ⟨fun _ _ ⟨a, ha, he⟩ => ⟨a, ha, he.symm⟩⟩ loopless := ⟨fun x ⟨a, _, he⟩ => by rcases he with he | he <;> exact (ne_of_lt a.2.1) (he.1.trans he.2.symm)⟩ theorem baseOfArcs_le (S : Set (Arc F)) : baseOfArcs S ≤ F := by intro x y ⟨a, _, he⟩ rcases he with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ · exact a.2.2 · exact a.2.2.symm theorem branching_colorable {H : SimpleGraph (Arc F)} {a : ℕ} (hH : H ≤ arcGraph F) (hc : (baseOfArcs {b | Branching H b}).Colorable a) : (H.induce {b | Branching H b}).Colorable a := by obtain ⟨c⟩ := hc refine ⟨SimpleGraph.Coloring.mk (fun b => c b.1.1.1) ?_⟩ intro b d hbd apply c.valid rcases hH hbd with hbd | hdb · exact ⟨b.1, b.2, Or.inl ⟨rfl, hbd⟩⟩ · exact ⟨d.1, d.2, Or.inr ⟨rfl, hdb⟩⟩ variable [Fintype V] noncomputable def outgoingArcs (F : SimpleGraph V) (v : V) : Finset (Arc F) := by classical exact Finset.univ.filter fun a => a.1.1 = v noncomputable def incomingBranches (H : SimpleGraph (Arc F)) (v : V) : Finset (Arc F) := by classical exact Finset.univ.filter fun a => a.1.2 = v ∧ Branching H a theorem incomingBranches_card_le {H : SimpleGraph (Arc F)} (h4 : FourCycleFree H) (v : V) : (incomingBranches H v).card ≤ (outgoingArcs F v).card.choose 2 := by classical apply card_le_choose_two_of_fourCycleFree h4 intro a ha obtain ⟨hav, b, c, hbc, hab, hac, hbt, hct⟩ := (Finset.mem_filter.mp ha).2 refine ⟨b, ?_, c, ?_, hbc, hab, hac⟩ · simp [outgoingArcs, ← hbt, hav] · simp [outgoingArcs, ← hct, hav] theorem selected_degree_le {H : SimpleGraph (Arc F)} (h4 : FourCycleFree H) (v : V) : Nat.card ((baseOfArcs {a | Branching H a}).neighborSet v) ≤ (outgoingArcs F v).card + (outgoingArcs F v).card.choose 2 := by classical let J := baseOfArcs {a | Branching H a} change Nat.card (J.neighborSet v) ≤ _ rw [Nat.card_eq_fintype_card, SimpleGraph.card_neighborSet_eq_degree] have hsub : J.neighborFinset v ⊆ (outgoingArcs F v).image (fun a => a.1.2) ∪ (incomingBranches H v).image (fun a => a.1.1) := by intro w hw obtain ⟨a, ha, he⟩ := (J.mem_neighborFinset v w).mp hw rcases he with ⟨hat, hah⟩ | ⟨hat, hah⟩ · apply Finset.mem_union_left exact Finset.mem_image.mpr ⟨a, by simp [outgoingArcs, hat], hah⟩ · apply Finset.mem_union_right exact Finset.mem_image.mpr ⟨a, Finset.mem_filter.mpr ⟨Finset.mem_univ a, hah, ha⟩, hat⟩ calc J.degree v = (J.neighborFinset v).card := rfl _ ≤ ((outgoingArcs F v).image (fun a => a.1.2) ∪ (incomingBranches H v).image (fun a => a.1.1)).card := Finset.card_le_card hsub _ ≤ ((outgoingArcs F v).image (fun a => a.1.2)).card + ((incomingBranches H v).image (fun a => a.1.1)).card := Finset.card_union_le _ _ _ ≤ (outgoingArcs F v).card + (incomingBranches H v).card := Nat.add_le_add (Finset.card_image_le) (Finset.card_image_le) _ ≤ _ := Nat.add_le_add_left (incomingBranches_card_le h4 v) _ end Selection /-- Greedy coloring, with a low-degree vertex available in every remaining set. -/ theorem colorable_of_low_degree {V : Type*} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] {k : ℕ} (hk : 0 < k) (hdeg : ∀ S : Finset V, S.Nonempty → ∃ v ∈ S, (S.filter (H.Adj v)).card < k) : H.Colorable k := by classical have hcolor : ∀ S : Finset V, ∃ c : V → Fin k, ∀ x ∈ S, ∀ y ∈ S, H.Adj x y → c x ≠ c y := by intro S induction S using Finset.strongInductionOn with | _ S ih => by_cases hS : S.Nonempty · obtain ⟨v, hv, hvc⟩ := hdeg S hS obtain ⟨c, hc⟩ := ih (S.erase v) (Finset.erase_ssubset hv) have hcard : ((S.filter (H.Adj v)).image c).card < (Finset.univ : Finset (Fin k)).card := by simpa using lt_of_le_of_lt Finset.card_image_le hvc obtain ⟨j, _, hj⟩ := Finset.exists_mem_notMem_of_card_lt_card hcard refine ⟨Function.update c v j, ?_⟩ intro x hx y hy hxy by_cases hxv : x = v · subst x have hyv : y ≠ v := hxy.ne.symm simp only [Function.update_self, Function.update_of_ne hyv] intro heq exact hj (Finset.mem_image.mpr ⟨y, Finset.mem_filter.mpr ⟨hy, hxy⟩, heq.symm⟩) · by_cases hyv : y = v · subst y simp only [Function.update_self, Function.update_of_ne hxv] intro heq exact hj (Finset.mem_image.mpr ⟨x, Finset.mem_filter.mpr ⟨hx, hxy.symm⟩, heq⟩) · simpa only [Function.update_of_ne hxv, Function.update_of_ne hyv] using hc x (Finset.mem_erase.mpr ⟨hxv, hx⟩) y (Finset.mem_erase.mpr ⟨hyv, hy⟩) hxy · refine ⟨fun _ => ⟨0, hk⟩, ?_⟩ intro x hx exact (hS ⟨x, hx⟩).elim obtain ⟨c, hc⟩ := hcolor Finset.univ exact ⟨SimpleGraph.Coloring.mk c fun {x y} hxy => hc x (Finset.mem_univ x) y (Finset.mem_univ y) hxy⟩ theorem colorable_of_partition {V : Type*} {H : SimpleGraph V} (S : Set V) {a b : ℕ} (hS : (H.induce S).Colorable a) (hR : (H.induce Sᶜ).Colorable b) : H.Colorable (a + b) := by classical obtain ⟨cS⟩ := hS obtain ⟨cR⟩ := hR let c : V → Fin a ⊕ Fin b := fun v => if hv : v ∈ S then Sum.inl (cS ⟨v, hv⟩) else Sum.inr (cR ⟨v, hv⟩) have hc : ∀ {x y}, H.Adj x y → c x ≠ c y := by intro x y hxy dsimp [c] split_ifs with hx hy hy · exact fun heq => cS.valid (v := ⟨x, hx⟩) (w := ⟨y, hy⟩) hxy (Sum.inl.inj heq) · exact id · exact id · exact fun heq => cR.valid (v := ⟨x, hx⟩) (w := ⟨y, hy⟩) hxy (Sum.inr.inj heq) simpa using (SimpleGraph.Coloring.mk c hc).colorable section ArcColorBound variable {V : Type u} [LinearOrder V] [Fintype V] {F : SimpleGraph V} /-- The residual arc vertices can be greedily colored with two colors. -/ theorem nonbranching_colorable {H : SimpleGraph (Arc F)} (hH : H ≤ arcGraph F) : (H.induce {a | ¬ Branching H a}).Colorable 2 := by classical apply colorable_of_low_degree _ (by decide) intro S hS obtain ⟨a, ha, hmin⟩ := S.exists_min_image (fun a => a.1.1.1) hS refine ⟨a, ha, ?_⟩ have hforward : ∀ b ∈ S, H.Adj a.1 b.1 → a.1.1.2 = b.1.1.1 := by intro b hb hab rcases hH hab with hab | hba · exact hab · have hlt := b.1.2.1 rw [hba] at hlt exact ((not_lt_of_ge (hmin b hb)) hlt).elim have hcard : (S.filter (fun b => H.Adj a.1 b.1)).card ≤ 1 := by apply Finset.card_le_one.mpr intro b hb c hc obtain ⟨hbS, hab⟩ := Finset.mem_filter.mp hb obtain ⟨hcS, hac⟩ := Finset.mem_filter.mp hc by_contra hbc exact a.2 ⟨b.1, c.1, (fun heq => hbc (Subtype.ext heq)), hab, hac, hforward b hbS hab, hforward c hcS hac⟩ exact Nat.lt_succ_of_le hcard /-- Lemma 1 of the attachment, for arbitrary spanning edge selections. -/ theorem arc_colorable_bound {d a : ℕ} (hout : ∀ v, (outgoingArcs F v).card ≤ d) (hbase : ∀ J : SimpleGraph V, J ≤ F → (∀ v, Nat.card (J.neighborSet v) ≤ d + d.choose 2) → J.Colorable a) {H : SimpleGraph (Arc F)} (hH : H ≤ arcGraph F) (h4 : FourCycleFree H) : H.Colorable (a + 2) := by apply colorable_of_partition {b | Branching H b} · apply branching_colorable hH apply hbase _ (baseOfArcs_le _) intro v exact (selected_degree_le h4 v).trans (Nat.add_le_add (hout v) (Nat.choose_le_choose 2 (hout v))) · exact nonbranching_colorable hH end ArcColorBound theorem FourCycleFree.spanningCoe {V : Type*} {G : SimpleGraph V} {H : G.Subgraph} (h : FourCycleFree H.coe) : FourCycleFree H.spanningCoe := by intro a b x y hab hxy hax hay hbx hby let a' : H.verts := ⟨a, H.edge_vert hax⟩ let b' : H.verts := ⟨b, H.edge_vert hbx⟩ let x' : H.verts := ⟨x, H.edge_vert (H.adj_symm hax)⟩ let y' : H.verts := ⟨y, H.edge_vert (H.adj_symm hay)⟩ exact h a' b' x' y' (fun heq => hab (congrArg Subtype.val heq)) (fun heq => hxy (congrArg Subtype.val heq)) hax hay hbx hby /-- The arc lemma applies to ordinary subgraphs, including vertex and edge deletion. -/ theorem arc_subgraph_colorable_bound {V : Type u} [LinearOrder V] [Fintype V] {F : SimpleGraph V} {d a : ℕ} (hout : ∀ v, (outgoingArcs F v).card ≤ d) (hbase : ∀ J : SimpleGraph V, J ≤ F → (∀ v, Nat.card (J.neighborSet v) ≤ d + d.choose 2) → J.Colorable a) (H : (arcGraph F).Subgraph) (h4 : FourCycleFree H.coe) : H.coe.Colorable (a + 2) := (arc_colorable_bound hout hbase H.spanningCoe_le h4.spanningCoe).of_hom H.coeEmbeddingSpanningCoe.toHom section EdgeCounting variable {V : Type*} /-- Ordered incidences from `X` to `Y`, counted as a real number. -/ noncomputable def crossingCount (G : SimpleGraph V) (X Y : Finset V) : ℝ := by classical exact ∑ x ∈ X, ∑ y ∈ Y, if G.Adj x y then 1 else 0 /-- The number of edges with both endpoints in `X`. -/ noncomputable def internalCount (G : SimpleGraph V) (X : Finset V) : ℝ := crossingCount G X X / 2 theorem crossingCount_nonneg (G : SimpleGraph V) (X Y : Finset V) : 0 ≤ crossingCount G X Y := by classical unfold crossingCount positivity theorem crossingCount_comm (G : SimpleGraph V) (X Y : Finset V) : crossingCount G X Y = crossingCount G Y X := by classical unfold crossingCount rw [Finset.sum_comm] apply Finset.sum_congr rfl intro y hy apply Finset.sum_congr rfl intro x hx rw [G.adj_comm] theorem crossingCount_union_left [DecidableEq V] (G : SimpleGraph V) {X Y : Finset V} (hd : Disjoint X Y) (Z : Finset V) : crossingCount G (X ∪ Y) Z = crossingCount G X Z + crossingCount G Y Z := by classical exact Finset.sum_union hd theorem crossingCount_union_right [DecidableEq V] (G : SimpleGraph V) (X : Finset V) {Y Z : Finset V} (hd : Disjoint Y Z) : crossingCount G X (Y ∪ Z) = crossingCount G X Y + crossingCount G X Z := by rw [crossingCount_comm G X, crossingCount_union_left G hd, crossingCount_comm G Y, crossingCount_comm G Z] theorem crossingCount_graph_mono {F G : SimpleGraph V} (h : F ≤ G) (X Y : Finset V) : crossingCount F X Y ≤ crossingCount G X Y := by classical apply Finset.sum_le_sum intro x hx apply Finset.sum_le_sum intro y hy by_cases hxy : F.Adj x y · simp [hxy, h hxy] · simp only [hxy, if_false] positivity theorem crossingCount_eq_sum_card (G : SimpleGraph V) (X Y : Finset V) [DecidableRel G.Adj] : crossingCount G X Y = ∑ x ∈ X, ((Y.filter (G.Adj x)).card : ℝ) := by classical simp only [crossingCount, Finset.card_filter, Nat.cast_sum, Nat.cast_ite, Nat.cast_one, Nat.cast_zero] apply Finset.sum_congr rfl intro x hx apply Finset.sum_congr rfl intro y hy split_ifs <;> rfl theorem crossingCount_eq_card_product (G : SimpleGraph V) (X Y : Finset V) [DecidableRel G.Adj] : crossingCount G X Y = (((X ×ˢ Y).filter (fun e => G.Adj e.1 e.2)).card : ℝ) := by classical simp only [crossingCount, Finset.card_filter, Finset.sum_product, Nat.cast_sum, Nat.cast_ite, Nat.cast_one, Nat.cast_zero] apply Finset.sum_congr rfl intro x hx apply Finset.sum_congr rfl intro y hy split_ifs <;> rfl theorem crossingCount_le_card_mul (G : SimpleGraph V) (X Y : Finset V) [DecidableRel G.Adj] {k : ℕ} (h : ∀ x ∈ X, (Y.filter (G.Adj x)).card ≤ k) : crossingCount G X Y ≤ X.card * k := by rw [crossingCount_eq_sum_card] calc _ ≤ ∑ _x ∈ X, (k : ℝ) := Finset.sum_le_sum fun x hx => by exact_mod_cast h x hx _ = _ := by simp theorem crossingCount_eq_zero (G : SimpleGraph V) (X Y : Finset V) (h : ∀ x ∈ X, ∀ y ∈ Y, ¬ G.Adj x y) : crossingCount G X Y = 0 := by classical apply Finset.sum_eq_zero intro x hx apply Finset.sum_eq_zero intro y hy simp [h x hx y hy] /-- Deleting all edges incident with `Z` costs at most its total incidence count. -/ theorem internalCount_cut [DecidableEq V] (G : SimpleGraph V) {X Y Z : Finset V} (hXY : Disjoint X Y) (hXZ : Disjoint X Z) (hYZ : Disjoint Y Z) (hY : crossingCount G Y Y = 0) : internalCount G (X ∪ Y ∪ Z) ≤ internalCount G X + crossingCount G X Y + crossingCount G Z (X ∪ Y ∪ Z) := by have hXYZ : Disjoint (X ∪ Y) Z := Finset.disjoint_union_left.mpr ⟨hXZ, hYZ⟩ unfold internalCount rw [crossingCount_union_left G hXYZ, crossingCount_union_left G hXY, crossingCount_union_right G X hXYZ, crossingCount_union_right G X hXY, crossingCount_union_right G Y hXYZ, crossingCount_union_right G Y hXY, crossingCount_union_right G Z hXYZ, crossingCount_union_right G Z hXY, crossingCount_comm G Y X, crossingCount_comm G Z X, crossingCount_comm G Z Y, hY] nlinarith [crossingCount_nonneg G Z Z] end EdgeCounting /-- The numerical core of the deterministic cut in Lemma 3. -/ theorem cut_density_inequality {K s x y z e f : ℝ} (hK : 4 ≤ K) (hs : 0 < s) (_hx : 0 ≤ x) (hy : 0 ≤ y) (hxy : x + y ≤ s) (hz : z < 2 * s / (16 * K * (K + 1))) (he : 2 * s ≤ e + f + K * z) (hfX : f ≤ x) (hfY : f ≤ K * y) : (1 + 1 / (2 * (K + 1))) * x < e := by have hK0 : 0 < K := by linarith have hK1 : 0 < K + 1 := by linarith have hden : 0 < 16 * K * (K + 1) := by positivity have hcross : (K + 1) * f ≤ K * s := by nlinarith have htail : (16 * K * (K + 1)) * z < 2 * s := by nlinarith [(lt_div_iff₀ hden).mp hz] have he' : (K + 1) * (2 * s) ≤ (K + 1) * (e + f + K * z) := mul_le_mul_of_nonneg_left he (le_of_lt hK1) have hmain : 8 * (K + 1) * e > (8 * K + 15) * s := by nlinarith have hxs : x ≤ s := by linarith have htarget : (2 * (K + 1) + 1) * x < 2 * (K + 1) * e := by nlinarith [mul_nonneg (show 0 ≤ 2 * (K + 1) + 1 by positivity) (sub_nonneg.mpr hxs)] have hden2 : 0 < 2 * (K + 1) := by positivity have heq : (1 + 1 / (2 * (K + 1))) * x = ((2 * (K + 1) + 1) * x) / (2 * (K + 1)) := by field_simp rw [heq] exact (div_lt_iff₀ hden2).mpr (by nlinarith) section DeterministicObstruction variable {V : Type*} [Fintype V] [DecidableEq V] /-- The partitions and density estimates used by the deterministic cut argument. -/ def SparseCutProperty (F : SimpleGraph V) (K : ℕ) : Prop := ∀ S : Finset V, S.Nonempty → ∃ X Y Z : Finset V, S = X ∪ Y ∪ Z ∧ Disjoint X Y ∧ Disjoint X Z ∧ Disjoint Y Z ∧ crossingCount F Y Y = 0 ∧ crossingCount F X Y ≤ X.card ∧ (Z.card : ℝ) < 2 * S.card / (16 * K * (K + 1)) ∧ internalCount F X ≤ (1 + 1 / (2 * (K + 1))) * X.card omit [DecidableEq V] in theorem filter_neighbors_card_le (J : SimpleGraph V) [DecidableRel J.Adj] (S : Finset V) (v : V) : (S.filter (J.Adj v)).card ≤ Nat.card (J.neighborSet v) := by classical rw [Nat.card_eq_fintype_card, SimpleGraph.card_neighborSet_eq_degree, ← SimpleGraph.card_neighborFinset_eq_degree] apply Finset.card_le_card intro w hw exact (J.mem_neighborFinset v w).mpr (Finset.mem_filter.mp hw).2 /-- Every bounded-degree subgraph of a graph with the sparse cuts is 4-colorable. -/ theorem colorable_four_of_sparse_cuts {F J : SimpleGraph V} {K : ℕ} (hK : 4 ≤ K) (hcuts : SparseCutProperty F K) (hJF : J ≤ F) (hdeg : ∀ v, Nat.card (J.neighborSet v) ≤ K) : J.Colorable 4 := by classical apply colorable_of_low_degree _ (by decide) intro S hS by_contra! hmin obtain ⟨X, Y, Z, hSXYZ, hXY, hXZ, hYZ, hFY, hFXY, hZ, hFX⟩ := hcuts S hS have hJY : crossingCount J Y Y = 0 := le_antisymm ((crossingCount_graph_mono hJF Y Y).trans_eq hFY) (crossingCount_nonneg J Y Y) have hJS : 2 * (S.card : ℝ) ≤ internalCount J S := by have hsum : (4 : ℝ) * S.card ≤ crossingCount J S S := by rw [crossingCount_eq_sum_card] calc _ = ∑ _v ∈ S, (4 : ℝ) := by simp [mul_comm] _ ≤ _ := Finset.sum_le_sum fun v hv => by exact_mod_cast hmin v hv unfold internalCount linarith have hXYS : (X.card : ℝ) + Y.card ≤ S.card := by norm_cast rw [← Finset.card_union_of_disjoint hXY] apply Finset.card_le_card rw [hSXYZ] exact Finset.subset_union_left have hJXY : crossingCount J X Y ≤ X.card := (crossingCount_graph_mono hJF X Y).trans hFXY have hJYX : crossingCount J X Y ≤ (K : ℝ) * Y.card := by rw [crossingCount_comm J X Y, mul_comm] apply crossingCount_le_card_mul intro v hv exact (filter_neighbors_card_le J X v).trans (hdeg v) have hJZS : crossingCount J Z S ≤ (K : ℝ) * Z.card := by rw [mul_comm] apply crossingCount_le_card_mul intro v hv exact (filter_neighbors_card_le J S v).trans (hdeg v) have hcut : internalCount J S ≤ internalCount J X + crossingCount J X Y + crossingCount J Z S := by rw [hSXYZ] exact internalCount_cut J hXY hXZ hYZ hJY have hbad := cut_density_inequality (K := (K : ℝ)) (s := (S.card : ℝ)) (x := (X.card : ℝ)) (y := (Y.card : ℝ)) (z := (Z.card : ℝ)) (e := internalCount J X) (f := crossingCount J X Y) (by exact_mod_cast hK) (by exact_mod_cast Finset.card_pos.mpr hS) (by positivity) (by positivity) hXYS hZ (by linarith) hJXY hJYX have hJX : internalCount J X ≤ internalCount F X := div_le_div_of_nonneg_right (crossingCount_graph_mono hJF X X) (by positivity) linarith /- Local sparsity in earlier parts yields the cuts used in Lemma 3. -/ omit [Fintype V] in theorem sparse_cuts_of_parts {F : SimpleGraph V} {C K A : ℕ} (part : V → Fin C) (n : Fin C → ℕ) (hsame : ∀ v w, part v = part w → ¬ F.Adj v w) (hone : ∀ v i, part v < i → ∀ w z, part w = i → part z = i → F.Adj v w → F.Adj v z → w = z) (hcut : ∀ S : Finset V, S.Nonempty → ∃ i : Fin C, S.card ≤ A * n i ∧ ((S.filter (fun v => i < part v)).card : ℝ) < 2 * S.card / (16 * K * (K + 1))) (hsparse : ∀ (i : Fin C) (X : Finset V), (∀ v ∈ X, part v < i) → X.card ≤ A * n i → internalCount F X ≤ (1 + 1 / (2 * (K + 1))) * X.card) : SparseCutProperty F K := by classical intro S hS obtain ⟨i, hsize, htail⟩ := hcut S hS let X := S.filter fun v => part v < i let Y := S.filter fun v => part v = i let Z := S.filter fun v => i < part v have hpartition : S = X ∪ Y ∪ Z := by ext v simp only [X, Y, Z, Finset.mem_union, Finset.mem_filter] have htri := lt_trichotomy (part v) i tauto have hXY : Disjoint X Y := by apply Finset.disjoint_left.mpr intro v hx hy have hx' := (Finset.mem_filter.mp hx).2 have hy' := (Finset.mem_filter.mp hy).2 omega have hXZ : Disjoint X Z := by apply Finset.disjoint_left.mpr intro v hx hz have hx' := (Finset.mem_filter.mp hx).2 have hz' := (Finset.mem_filter.mp hz).2 omega have hYZ : Disjoint Y Z := by apply Finset.disjoint_left.mpr intro v hy hz have hy' := (Finset.mem_filter.mp hy).2 have hz' := (Finset.mem_filter.mp hz).2 omega refine ⟨X, Y, Z, hpartition, hXY, hXZ, hYZ, ?_, ?_, htail, ?_⟩ · apply crossingCount_eq_zero intro v hv w hw exact hsame v w ((Finset.mem_filter.mp hv).2.trans (Finset.mem_filter.mp hw).2.symm) · have hbound : crossingCount F X Y ≤ X.card * (1 : ℕ) := by apply crossingCount_le_card_mul intro v hv apply Finset.card_le_one.mpr intro w hw z hz have hw' := Finset.mem_filter.mp hw have hz' := Finset.mem_filter.mp hz exact hone v i (Finset.mem_filter.mp hv).2 w z (Finset.mem_filter.mp hw'.1).2 (Finset.mem_filter.mp hz'.1).2 hw'.2 hz'.2 simpa using hbound · exact hsparse i X (fun v hv => (Finset.mem_filter.mp hv).2) (le_trans (Finset.card_filter_le _ _) hsize) end DeterministicObstruction section FiniteProbability variable {Ω : Type*} [Fintype Ω] /-- Uniform probability on a finite sample space, expressed by counting. -/ noncomputable def finiteProb (A : Set Ω) : ℝ := (A.ncard : ℝ) / Fintype.card Ω theorem finiteProb_nonneg (A : Set Ω) : 0 ≤ finiteProb A := by unfold finiteProb positivity theorem finiteProb_mono {A B : Set Ω} (h : A ⊆ B) : finiteProb A ≤ finiteProb B := by apply div_le_div_of_nonneg_right _ (by positivity) exact_mod_cast Set.ncard_mono h theorem finiteProb_empty : finiteProb (∅ : Set Ω) = 0 := by simp [finiteProb] theorem finiteProb_univ [Nonempty Ω] : finiteProb (Set.univ : Set Ω) = 1 := by simp [finiteProb, Fintype.card_ne_zero] theorem finiteProb_union_le (A B : Set Ω) : finiteProb (A ∪ B) ≤ finiteProb A + finiteProb B := by unfold finiteProb rw [← add_div] apply div_le_div_of_nonneg_right _ (by positivity) exact_mod_cast Set.ncard_union_le A B theorem finiteProb_biUnion_le {ι : Type*} (s : Finset ι) (A : ι → Set Ω) : finiteProb {ω | ∃ i ∈ s, ω ∈ A i} ≤ ∑ i ∈ s, finiteProb (A i) := by classical induction s using Finset.induction_on with | empty => simp [finiteProb] | @insert i s hi ih => have heq : {ω | ∃ j ∈ insert i s, ω ∈ A j} = A i ∪ {ω | ∃ j ∈ s, ω ∈ A j} := by ext ω simp rw [heq, Finset.sum_insert hi] exact (finiteProb_union_le _ _).trans (add_le_add le_rfl ih) theorem exists_avoiding_of_finiteProb_lt_one [Nonempty Ω] (A B : Set Ω) (h : finiteProb A + finiteProb B < 1) : ∃ ω, ω ∉ A ∧ ω ∉ B := by by_contra! hbad have heq : A ∪ B = Set.univ := by ext ω simp only [Set.mem_union, Set.mem_univ, iff_true] by_cases ha : ω ∈ A · exact Or.inl ha · exact Or.inr (hbad ω ha) have hu := finiteProb_union_le A B rw [heq, finiteProb_univ] at hu linarith theorem finiteProb_box {ι : Type*} [Fintype ι] [DecidableEq ι] {α : ι → Type*} [∀ i, Fintype (α i)] (A : ∀ i, Set (α i)) : finiteProb {ω : ∀ i, α i | ∀ i, ω i ∈ A i} = ∏ i, ((A i).ncard : ℝ) / Fintype.card (α i) := by classical unfold finiteProb have hcard : {ω : ∀ i, α i | ∀ i, ω i ∈ A i}.ncard = ∏ i, (A i).ncard := by change Nat.card {ω : ∀ i, α i // ∀ i, ω i ∈ A i} = _ rw [Nat.card_congr (Equiv.subtypePiEquivPi (β := α) (p := fun i x => x ∈ A i)), Nat.card_pi] rfl rw [hcard, Fintype.card_pi] simp only [Nat.cast_prod, Finset.prod_div_distrib] theorem finiteProb_agreement {ι : Type*} [Fintype ι] [DecidableEq ι] {α : ι → Type*} [∀ i, Fintype (α i)] (ω₀ : ∀ i, α i) (s : Finset ι) : finiteProb {ω : ∀ i, α i | ∀ i ∈ s, ω i = ω₀ i} = ∏ i ∈ s, (1 / (Fintype.card (α i) : ℝ)) := by classical let : ∀ i, Nonempty (α i) := fun i => ⟨ω₀ i⟩ let A : ∀ i, Set (α i) := fun i => if i ∈ s then {ω₀ i} else Set.univ have heq : {ω : ∀ i, α i | ∀ i ∈ s, ω i = ω₀ i} = {ω | ∀ i, ω i ∈ A i} := by ext ω simp [A] rw [heq, finiteProb_box] calc _ = ∏ i, if i ∈ s then (1 / (Fintype.card (α i) : ℝ)) else 1 := by apply Finset.prod_congr rfl intro i hi by_cases his : i ∈ s <;> simp [A, his, Fintype.card_ne_zero] _ = _ := Fintype.prod_ite_mem s _ theorem finiteProb_agreement_le {ι : Type*} [Fintype ι] [DecidableEq ι] {α : ι → Type*} [∀ i, Fintype (α i)] (ω₀ : ∀ i, α i) (s : Finset ι) {n : ℕ} (hn : 0 < n) (hcard : ∀ i ∈ s, n ≤ Fintype.card (α i)) : finiteProb {ω : ∀ i, α i | ∀ i ∈ s, ω i = ω₀ i} ≤ (1 / (n : ℝ)) ^ s.card := by rw [finiteProb_agreement] calc _ ≤ ∏ _i ∈ s, (1 / (n : ℝ)) := by apply Finset.prod_le_prod (fun _ _ => by positivity) intro i hi exact one_div_le_one_div_of_le (by exact_mod_cast hn) (by exact_mod_cast hcard i hi) _ = _ := by simp theorem finiteProb_card_ge_le {ε : Type*} [DecidableEq ε] (P : Finset ε) (present : Ω → Finset ε) (hP : ∀ ω, present ω ⊆ P) (m : ℕ) (B : ℝ) (hB : ∀ E ∈ P.powersetCard m, finiteProb {ω | E ⊆ present ω} ≤ B) : finiteProb {ω | m ≤ (present ω).card} ≤ (P.card.choose m : ℝ) * B := by classical have hsub : {ω | m ≤ (present ω).card} ⊆ {ω | ∃ E ∈ P.powersetCard m, E ⊆ present ω} := by intro ω hω obtain ⟨E, hE, hEm⟩ := Finset.exists_subset_card_eq hω exact ⟨E, Finset.mem_powersetCard.mpr ⟨hE.trans (hP ω), hEm⟩, hE⟩ calc _ ≤ finiteProb {ω | ∃ E ∈ P.powersetCard m, E ⊆ present ω} := finiteProb_mono hsub _ ≤ ∑ E ∈ P.powersetCard m, finiteProb {ω | E ⊆ present ω} := finiteProb_biUnion_le _ _ _ ≤ ∑ _E ∈ P.powersetCard m, B := Finset.sum_le_sum hB _ = _ := by simp end FiniteProbability section MultipartiteModel variable {C : ℕ} /-- Vertices in ordered parts of the specified sizes. -/ abbrev ModelVertex (n : Fin C → ℕ) := Lex (Σ i : Fin C, Fin (n i)) /-- Unused choices into earlier parts are retained to make a rectangular product. -/ abbrev ModelSample (n : Fin C → ℕ) := (k : ModelVertex n × Fin C) → Fin (n k.2) /-- Each vertex chooses exactly one neighbor in each later part. -/ def modelGraph {n : Fin C → ℕ} (ω : ModelSample n) : SimpleGraph (ModelVertex n) where Adj v w := (v.1 < w.1 ∧ ω (v, w.1) = w.2) ∨ (w.1 < v.1 ∧ ω (w, v.1) = v.2) symm := ⟨fun _ _ => Or.symm⟩ loopless := ⟨fun v h => h.elim (fun h => (lt_irrefl v.1) h.1) (fun h => (lt_irrefl v.1) h.1)⟩ theorem modelGraph_same_part {n : Fin C → ℕ} (ω : ModelSample n) (v w : ModelVertex n) (hvw : v.1 = w.1) : ¬ (modelGraph ω).Adj v w := by rintro (h | h) <;> have hlt := h.1 <;> rw [hvw] at hlt <;> exact (lt_irrefl _) hlt theorem modelGraph_forward {n : Fin C → ℕ} (ω : ModelSample n) {v w : ModelVertex n} (hvw : v.1 < w.1) : (modelGraph ω).Adj v w ↔ ω (v, w.1) = w.2 := by constructor · rintro (h | h) · exact h.2 · exact (hvw.not_gt h.1).elim · exact fun h => Or.inl ⟨hvw, h⟩ theorem modelGraph_one_neighbor {n : Fin C → ℕ} (ω : ModelSample n) (v : ModelVertex n) (i : Fin C) (hvi : v.1 < i) (w z : ModelVertex n) (hwi : w.1 = i) (hzi : z.1 = i) (hvw : (modelGraph ω).Adj v w) (hvz : (modelGraph ω).Adj v z) : w = z := by obtain ⟨j, w⟩ := w obtain ⟨k, z⟩ := z dsimp at hwi hzi subst j subst k have hw := (modelGraph_forward ω hvi).mp hvw have hz := (modelGraph_forward ω hvi).mp hvz exact congrArg (fun x : Fin (n i) => (⟨i, x⟩ : ModelVertex n)) (hw.symm.trans hz) theorem model_arc_forward {n : Fin C → ℕ} (ω : ModelSample n) (a : Arc (modelGraph ω)) : a.1.1.1 < a.1.2.1 := by rcases a.2.2 with h | h · exact h.1 · rcases Sigma.Lex.lt_def.mp a.2.1 with hlt | ⟨heq, _⟩ · exact (hlt.not_gt h.1).elim · have hlt := h.1 rw [heq] at hlt exact (lt_irrefl _ hlt).elim /-- The maximum outdegree depends only on the number of parts. -/ theorem model_outgoing_card_le {n : Fin C → ℕ} (ω : ModelSample n) (v : ModelVertex n) : (outgoingArcs (modelGraph ω) v).card ≤ C - 1 := by classical let S := outgoingArcs (modelGraph ω) v let f : Arc (modelGraph ω) → Fin C := fun a => a.1.2.1 have hinj : Set.InjOn f (S : Set (Arc (modelGraph ω))) := by intro a ha b hb hab have hat : a.1.1 = v := (Finset.mem_filter.mp ha).2 have hbt : b.1.1 = v := (Finset.mem_filter.mp hb).2 apply Subtype.ext apply Prod.ext (hat.trans hbt.symm) have hav : (modelGraph ω).Adj v a.1.2 := by simpa only [hat] using a.2.2 have hbv : (modelGraph ω).Adj v b.1.2 := by simpa only [hbt] using b.2.2 have hvi : v.1 < a.1.2.1 := by simpa only [hat] using model_arc_forward ω a exact modelGraph_one_neighbor ω v a.1.2.1 hvi a.1.2 b.1.2 rfl hab.symm hav hbv have hsub : S.image f ⊆ (Finset.univ : Finset (Fin C)).erase v.1 := by intro j hj obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hj have hat : a.1.1 = v := (Finset.mem_filter.mp ha).2 have hlt : v.1 < f a := by simpa only [f, hat] using model_arc_forward ω a exact Finset.mem_erase.mpr ⟨hlt.ne.symm, Finset.mem_univ _⟩ calc S.card = (S.image f).card := (Finset.card_image_of_injOn hinj).symm _ ≤ ((Finset.univ : Finset (Fin C)).erase v.1).card := Finset.card_le_card hsub _ = C - 1 := by simp /-- The probability of a specified set of distinct forward edges. -/ theorem model_contains_probability_le {n : Fin C → ℕ} (E : Finset (ModelVertex n × ModelVertex n)) (hE : ∀ e ∈ E, e.1.1 < e.2.1) {N : ℕ} (hN : 0 < N) (hsize : ∀ e ∈ E, N ≤ n e.2.1) : finiteProb {ω : ModelSample n | ∀ e ∈ E, (modelGraph ω).Adj e.1 e.2} ≤ (1 / (N : ℝ)) ^ E.card := by classical let A : Set (ModelSample n) := {ω | ∀ e ∈ E, (modelGraph ω).Adj e.1 e.2} by_cases hA : A.Nonempty · obtain ⟨ω₀, hω₀⟩ := hA let key : ModelVertex n × ModelVertex n → ModelVertex n × Fin C := fun e => (e.1, e.2.1) have hinj : Set.InjOn key (E : Set (ModelVertex n × ModelVertex n)) := by intro a ha b hb hab have hs : a.1 = b.1 := congrArg (fun k : ModelVertex n × Fin C => k.1) hab have ht : a.2.1 = b.2.1 := congrArg (fun k : ModelVertex n × Fin C => k.2) hab apply Prod.ext hs apply modelGraph_one_neighbor ω₀ a.1 a.2.1 (hE a ha) a.2 b.2 rfl ht.symm · exact hω₀ a ha · simpa only [hs] using hω₀ b hb have hsub : A ⊆ {ω : ModelSample n | ∀ k ∈ E.image key, ω k = ω₀ k} := by intro ω hω k hk obtain ⟨e, he, rfl⟩ := Finset.mem_image.mp hk exact ((modelGraph_forward ω (hE e he)).mp (hω e he)).trans ((modelGraph_forward ω₀ (hE e he)).mp (hω₀ e he)).symm have hsz : ∀ k ∈ E.image key, N ≤ Fintype.card (Fin (n k.2)) := by intro k hk obtain ⟨e, he, rfl⟩ := Finset.mem_image.mp hk simpa using hsize e he have hb := (finiteProb_mono hsub).trans (finiteProb_agreement_le ω₀ (E.image key) hN hsz) simpa only [Finset.card_image_of_injOn hinj] using hb · have heq : A = ∅ := Set.not_nonempty_iff_eq_empty.mp hA change finiteProb A ≤ _ rw [heq, finiteProb_empty] positivity noncomputable def possibleEdges {n : Fin C → ℕ} (X : Finset (ModelVertex n)) : Finset (ModelVertex n × ModelVertex n) := by classical exact (X ×ˢ X).filter fun e => e.1.1 < e.2.1 noncomputable def modelEdges {n : Fin C → ℕ} (ω : ModelSample n) (X : Finset (ModelVertex n)) : Finset (ModelVertex n × ModelVertex n) := by classical exact (possibleEdges X).filter fun e => (modelGraph ω).Adj e.1 e.2 /-- Each internal edge has precisely one orientation from an earlier to a later part. -/ theorem internalCount_modelGraph {n : Fin C → ℕ} (ω : ModelSample n) (X : Finset (ModelVertex n)) : internalCount (modelGraph ω) X = (modelEdges ω X).card := by classical let A := (X ×ˢ X).filter fun e => (modelGraph ω).Adj e.1 e.2 let B := A.filter fun e => ¬ e.1.1 < e.2.1 have hA : A.filter (fun e => e.1.1 < e.2.1) = modelEdges ω X := by ext e simp [A, modelEdges, possibleEdges, and_left_comm, and_comm] have hB : (modelEdges ω X).card = B.card := by apply Finset.card_bij (fun e _ => (e.2, e.1)) · intro e he have he' : (e.1 ∈ X ∧ e.2 ∈ X) ∧ e.1.1 < e.2.1 ∧ (modelGraph ω).Adj e.1 e.2 := by simpa [modelEdges, possibleEdges, and_assoc] using he apply Finset.mem_filter.mpr refine ⟨Finset.mem_filter.mpr ⟨Finset.mem_product.mpr ⟨he'.1.2, he'.1.1⟩, he'.2.2.symm⟩, ?_⟩ exact he'.2.1.not_gt · intro a ha b hb hab exact Prod.ext (congrArg Prod.snd hab) (congrArg Prod.fst hab) · intro e he obtain ⟨heA, heback⟩ := Finset.mem_filter.mp he obtain ⟨heX, heAdj⟩ := Finset.mem_filter.mp heA have hedir : e.2.1 < e.1.1 := by rcases heAdj with h | h · exact (heback h.1).elim · exact h.1 refine ⟨(e.2, e.1), ?_, rfl⟩ have hx := Finset.mem_product.mp heX simp only [modelEdges, possibleEdges, Finset.mem_filter, Finset.mem_product] exact ⟨⟨⟨hx.2, hx.1⟩, hedir⟩, heAdj.symm⟩ have hc : (modelEdges ω X).card + (modelEdges ω X).card = A.card := by have h := Finset.card_filter_add_card_filter_not (s := A) (fun e => e.1.1 < e.2.1) rw [hA] at h change (modelEdges ω X).card + B.card = A.card at h rw [← hB] at h exact h rw [internalCount, crossingCount_eq_card_product] change (A.card : ℝ) / 2 = _ have hcR : ((modelEdges ω X).card : ℝ) + (modelEdges ω X).card = A.card := by exact_mod_cast hc linarith theorem model_many_edges_probability_le {n : Fin C → ℕ} (X : Finset (ModelVertex n)) (m : ℕ) {N : ℕ} (hN : 0 < N) (hsize : ∀ v ∈ X, N ≤ n v.1) : finiteProb {ω : ModelSample n | m ≤ (modelEdges ω X).card} ≤ ((X.card ^ 2).choose m : ℝ) * (1 / (N : ℝ)) ^ m := by classical have hbound := finiteProb_card_ge_le (possibleEdges X) (fun ω : ModelSample n => modelEdges ω X) (fun _ => Finset.filter_subset _ _) m ((1 / (N : ℝ)) ^ m) (by intro E hE obtain ⟨hEP, hEm⟩ := Finset.mem_powersetCard.mp hE have hsub : {ω : ModelSample n | E ⊆ modelEdges ω X} ⊆ {ω | ∀ e ∈ E, (modelGraph ω).Adj e.1 e.2} := by intro ω hω e he exact (Finset.mem_filter.mp (hω he)).2 have hdir : ∀ e ∈ E, e.1.1 < e.2.1 := fun e he => (Finset.mem_filter.mp (hEP he)).2 have hsz : ∀ e ∈ E, N ≤ n e.2.1 := by intro e he exact hsize e.2 (Finset.mem_product.mp (Finset.mem_filter.mp (hEP he)).1).2 exact (finiteProb_mono hsub).trans (by simpa only [hEm] using model_contains_probability_le E hdir hN hsz)) apply hbound.trans apply mul_le_mul_of_nonneg_right _ (by positivity) exact_mod_cast Nat.choose_le_choose m (show (possibleEdges X).card ≤ X.card ^ 2 by calc _ ≤ (X ×ˢ X).card := Finset.card_filter_le _ _ _ = _ := by simp [pow_two]) noncomputable def modelFiber {n : Fin C → ℕ} (I : Finset (ModelVertex n)) (i : Fin C) : Finset (Fin (n i)) := by classical exact Finset.univ.filter fun x => (⟨i, x⟩ : ModelVertex n) ∈ I noncomputable def modelDensity {n : Fin C → ℕ} (I : Finset (ModelVertex n)) (i : Fin C) : ℝ := ((modelFiber I i).card : ℝ) / n i noncomputable def modelWeight {n : Fin C → ℕ} (I : Finset (ModelVertex n)) : ℝ := ∑ i, modelDensity I i theorem modelDensity_nonneg {n : Fin C → ℕ} (I : Finset (ModelVertex n)) (i : Fin C) : 0 ≤ modelDensity I i := by unfold modelDensity; positivity theorem modelDensity_le_one {n : Fin C → ℕ} (I : Finset (ModelVertex n)) (i : Fin C) (hn : 0 < n i) : modelDensity I i ≤ 1 := by classical apply (div_le_one₀ (by exact_mod_cast hn : (0 : ℝ) < n i)).mpr exact_mod_cast (show (modelFiber I i).card ≤ n i from (Finset.card_filter_le _ _).trans_eq (Fintype.card_fin (n i))) noncomputable def modelColorClass {n : Fin C → ℕ} {k : ℕ} (c : ModelVertex n → Fin k) (a : Fin k) : Finset (ModelVertex n) := by classical exact @Finset.filter _ (fun v => c v = a) (fun _ => Classical.propDecidable _) Finset.univ theorem mem_modelColorClass {n : Fin C → ℕ} {k : ℕ} (c : ModelVertex n → Fin k) (a : Fin k) (v : ModelVertex n) : v ∈ modelColorClass c a ↔ c v = a := by classical exact (@Finset.mem_filter (ModelVertex n) (fun v => c v = a) (fun _ => Classical.propDecidable _) Finset.univ v).trans (and_iff_right (Finset.mem_univ _)) /-- The weights of all color classes sum to the number of parts. -/ theorem modelWeight_color_sum {n : Fin C → ℕ} {k : ℕ} (hn : ∀ i, 0 < n i) (c : ModelVertex n → Fin k) : (∑ a : Fin k, modelWeight (modelColorClass c a)) = C := by classical unfold modelWeight modelDensity rw [Finset.sum_comm] calc _ = ∑ _i : Fin C, (1 : ℝ) := by apply Finset.sum_congr rfl intro i hi have hcount : (∑ a : Fin k, (modelFiber (modelColorClass c a) i).card) = n i := by have hfiber : ∀ a : Fin k, modelFiber (modelColorClass c a) i = Finset.univ.filter (fun x : Fin (n i) => c (⟨i, x⟩ : ModelVertex n) = a) := by intro a ext x simp only [modelFiber, Finset.mem_filter, Finset.mem_univ, true_and] exact mem_modelColorClass c a (⟨i, x⟩ : ModelVertex n) simp_rw [hfiber] simpa using (Finset.sum_card_fiberwise_eq_card_filter (Finset.univ : Finset (Fin (n i))) (Finset.univ : Finset (Fin k)) (fun x => c (⟨i, x⟩ : ModelVertex n))) rw [← Finset.sum_div] have hcountR : (∑ a : Fin k, ((modelFiber (modelColorClass c a) i).card : ℝ)) = n i := by exact_mod_cast hcount rw [hcountR] exact div_self (by exact_mod_cast Nat.ne_of_gt (hn i)) _ = _ := by simp /-- Small independent-set weights force a large chromatic number. -/ theorem model_not_colorable_of_independent_weights {n : Fin C → ℕ} {k : ℕ} (hn : ∀ i, 0 < n i) (hk : 0 < k) (ω : ModelSample n) (hsmall : ∀ I : Finset (ModelVertex n), (∀ v ∈ I, ∀ w ∈ I, ¬ (modelGraph ω).Adj v w) → modelWeight I < (C : ℝ) / k) : ¬ (modelGraph ω).Colorable k := by classical let : Nonempty (Fin k) := ⟨⟨0, hk⟩⟩ rintro ⟨c⟩ have hclasses : ∀ a : Fin k, modelWeight (modelColorClass c a) < (C : ℝ) / k := by intro a apply hsmall intro v hv w hw hvw exact c.valid hvw (((mem_modelColorClass c a v).mp hv).trans ((mem_modelColorClass c a w).mp hw).symm) have hsum : (∑ a : Fin k, modelWeight (modelColorClass c a)) < ∑ _a : Fin k, (C : ℝ) / k := Finset.sum_lt_sum_of_nonempty Finset.univ_nonempty (fun a _ => hclasses a) rw [modelWeight_color_sum hn c] at hsum have heq : (∑ _a : Fin k, (C : ℝ) / k) = C := by simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] field_simp linarith /-- Counting a fiber as vertices or as coordinates gives the same cardinality. -/ theorem modelFiber_card {n : Fin C → ℕ} (I : Finset (ModelVertex n)) (i : Fin C) : (modelFiber I i).card = (I.filter (fun v => v.1 = i)).card := by classical apply Finset.card_bij (fun x _ => (⟨i, x⟩ : ModelVertex n)) · intro x hx exact Finset.mem_filter.mpr ⟨(Finset.mem_filter.mp hx).2, rfl⟩ · intro x hx y hy heq cases heq rfl · intro v hv obtain ⟨j, x⟩ := v obtain ⟨hvI, hji⟩ := Finset.mem_filter.mp hv dsimp at hji subst j exact ⟨x, Finset.mem_filter.mpr ⟨Finset.mem_univ _, hvI⟩, rfl⟩ noncomputable def modelLaterWeight {n : Fin C → ℕ} (I : Finset (ModelVertex n)) (i : Fin C) : ℝ := ∑ j : Fin C, if i < j then modelDensity I j else 0 theorem modelLaterWeight_nonneg {n : Fin C → ℕ} (I : Finset (ModelVertex n)) (i : Fin C) : 0 ≤ modelLaterWeight I i := by apply Finset.sum_nonneg intro j hj split_ifs <;> first | exact modelDensity_nonneg _ _ | rfl /-- Choices from one fiber already give an exponential bound for independence. -/ theorem model_independent_probability_le {n : Fin C → ℕ} (hn : ∀ j, 0 < n j) (I : Finset (ModelVertex n)) (i : Fin C) : finiteProb {ω : ModelSample n | ∀ v ∈ I, ∀ w ∈ I, ¬ (modelGraph ω).Adj v w} ≤ Real.exp (-((modelFiber I i).card : ℝ) * modelLaterWeight I i) := by classical let S := I.filter (fun v => v.1 = i) let A : ∀ k : ModelVertex n × Fin C, Set (Fin (n k.2)) := fun k => if k.1 ∈ S ∧ i < k.2 then (↑(modelFiber I k.2) : Set (Fin (n k.2)))ᶜ else Set.univ let e : ModelVertex n × Fin C → ℝ := fun k => if k.1 ∈ S then if i < k.2 then -modelDensity I k.2 else 0 else 0 have hsub : {ω : ModelSample n | ∀ v ∈ I, ∀ w ∈ I, ¬ (modelGraph ω).Adj v w} ⊆ {ω | ∀ k, ω k ∈ A k} := by intro ω hω k by_cases hk : k.1 ∈ S ∧ i < k.2 · simp only [A, if_pos hk, Set.mem_compl_iff, Finset.mem_coe] intro hx have hsource := Finset.mem_filter.mp hk.1 have htarget : (⟨k.2, ω k⟩ : ModelVertex n) ∈ I := (Finset.mem_filter.mp hx).2 apply hω k.1 hsource.1 (⟨k.2, ω k⟩ : ModelVertex n) htarget apply Or.inl exact ⟨by simpa only [hsource.2] using hk.2, rfl⟩ · simp only [A, if_neg hk, Set.mem_univ] have hfactor : ∀ k : ModelVertex n × Fin C, ((A k).ncard : ℝ) / Fintype.card (Fin (n k.2)) ≤ Real.exp (e k) := by intro k have hnR : (0 : ℝ) < n k.2 := by exact_mod_cast hn k.2 by_cases hs : k.1 ∈ S · by_cases hj : i < k.2 · have hc : (modelFiber I k.2).card ≤ n k.2 := (Finset.card_filter_le _ _).trans_eq (Fintype.card_fin _) have heq : ((A k).ncard : ℝ) / Fintype.card (Fin (n k.2)) = 1 - modelDensity I k.2 := by simp only [A, if_pos (And.intro hs hj)] rw [Set.ncard_compl (↑(modelFiber I k.2) : Set (Fin (n k.2)))] simp only [Nat.card_eq_fintype_card, Fintype.card_fin, Set.ncard_coe_finset, Nat.cast_sub hc, modelDensity] field_simp rw [heq] have hb := Real.add_one_le_exp (-modelDensity I k.2) simpa only [e, if_pos hs, if_pos hj, sub_eq_add_neg, add_comm] using hb · simp [A, e, hs, hj, Set.ncard_univ, Nat.card_eq_fintype_card, hnR.ne'] · simp [A, e, hs, Set.ncard_univ, Nat.card_eq_fintype_card, hnR.ne'] have hexponent : (∑ k, e k) = -((modelFiber I i).card : ℝ) * modelLaterWeight I i := by rw [Fintype.sum_prod_type] calc _ = ∑ v : ModelVertex n, if v ∈ S then -modelLaterWeight I i else 0 := by apply Finset.sum_congr rfl intro v hv by_cases hs : v ∈ S · simp only [e, if_pos hs, modelLaterWeight, ← Finset.sum_neg_distrib] apply Finset.sum_congr rfl intro j hj split_ifs <;> simp · simp only [e, if_neg hs, Finset.sum_const_zero] _ = (S.card : ℝ) * (-modelLaterWeight I i) := by rw [Fintype.sum_ite_mem] simp _ = _ := by rw [modelFiber_card]; ring calc _ ≤ finiteProb {ω : ModelSample n | ∀ k, ω k ∈ A k} := finiteProb_mono hsub _ = ∏ k, ((A k).ncard : ℝ) / Fintype.card (Fin (n k.2)) := finiteProb_box A _ ≤ ∏ k, Real.exp (e k) := Finset.prod_le_prod (fun _ _ => by positivity) (fun k _ => hfactor k) _ = Real.exp (∑ k, e k) := (Real.exp_sum _ _).symm _ = _ := by rw [hexponent] end MultipartiteModel /-- The first substantial coordinate leaves a substantial sum to its right. -/ theorem exists_heavy_coordinate {C : ℕ} (hC : 0 < C) (p : Fin C → ℝ) {θ : ℝ} (hθ : 0 < θ) (hp : ∀ i, p i ≤ 1) (hsum : 2 * C * θ ≤ ∑ i, p i) : ∃ i : Fin C, θ ≤ p i ∧ (C : ℝ) * θ - 1 ≤ ∑ j : Fin C, if i < j then p j else 0 := by classical have hCR : (0 : ℝ) < C := by exact_mod_cast hC have hex : ∃ i : Fin C, θ ≤ p i := by by_contra! h have hb : (∑ i, p i) ≤ ∑ _i : Fin C, θ := Finset.sum_le_sum (fun i _ => (h i).le) simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] at hb nlinarith [mul_pos hCR hθ] let S := Finset.univ.filter (fun i : Fin C => θ ≤ p i) have hS : S.Nonempty := by obtain ⟨i, hi⟩ := hex exact ⟨i, Finset.mem_filter.mpr ⟨Finset.mem_univ _, hi⟩⟩ let i := S.min' hS have hi : θ ≤ p i := (Finset.mem_filter.mp (Finset.min'_mem S hS)).2 refine ⟨i, hi, ?_⟩ have hpoint : ∀ j : Fin C, p j ≤ θ + (if j = i then 1 else 0) + (if i < j then p j else 0) := by intro j rcases lt_trichotomy j i with hj | rfl | hj · have hjp : p j < θ := by by_contra! hbad have hji : i ≤ j := Finset.min'_le S j (Finset.mem_filter.mpr ⟨Finset.mem_univ _, hbad⟩) exact (not_lt_of_ge hji) hj simp only [if_neg hj.ne, if_neg hj.not_gt, add_zero] exact hjp.le · simp only [eq_self, if_true, lt_self_iff_false, if_false, add_zero] linarith [hp i] · simp only [if_neg hj.ne.symm, if_pos hj, add_zero] linarith have hb := Finset.sum_le_sum (fun j (_hj : j ∈ (Finset.univ : Finset (Fin C))) => hpoint j) simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, Finset.sum_ite_eq', Finset.mem_univ, if_true] at hb linarith /-- A large independent-set weight has a fiber witnessing both required lower bounds. -/ theorem model_weight_heavy_part {q C : ℕ} (hq : 1 ≤ q) (hC : C = 64 * q ^ 2) {n : Fin C → ℕ} (hn : ∀ j, 0 < n j) (I : Finset (ModelVertex n)) (hweight : (C : ℝ) / (2 * q) ≤ modelWeight I) : ∃ i : Fin C, 1 / (4 * (q : ℝ)) ≤ modelDensity I i ∧ 15 * (q : ℝ) ≤ modelLaterWeight I i := by have hqR : (0 : ℝ) < q := by exact_mod_cast (show 0 < q by omega) have hCpos : 0 < C := by rw [hC]; positivity have hsum : 2 * (C : ℝ) * (1 / (4 * q)) ≤ ∑ i, modelDensity I i := by have heq : 2 * (C : ℝ) * (1 / (4 * q)) = (C : ℝ) / (2 * q) := by ring rw [heq] exact hweight obtain ⟨i, hi, hright⟩ := exists_heavy_coordinate hCpos (modelDensity I) (by positivity) (fun j => modelDensity_le_one I j (hn j)) hsum refine ⟨i, hi, le_trans ?_ hright⟩ have hq1R : (1 : ℝ) ≤ q := by exact_mod_cast hq have hCR : (C : ℝ) = 64 * (q : ℝ) ^ 2 := by exact_mod_cast hC rw [hCR] have heq : 64 * (q : ℝ) ^ 2 * (1 / (4 * q)) = 16 * q := by field_simp; ring rw [heq] linarith noncomputable def modelSuffix {C : ℕ} (n : Fin C → ℕ) (i : Fin C) : Finset (ModelVertex n) := by classical exact Finset.univ.filter fun v => i ≤ v.1 noncomputable def modelRestrict {C : ℕ} {n : Fin C → ℕ} (I : Finset (ModelVertex n)) (i : Fin C) : Finset (ModelVertex n) := by classical exact I.filter fun v => i ≤ v.1 theorem mem_modelRestrict {C : ℕ} {n : Fin C → ℕ} (I : Finset (ModelVertex n)) (i : Fin C) (v : ModelVertex n) : v ∈ modelRestrict I i ↔ v ∈ I ∧ i ≤ v.1 := by classical exact Finset.mem_filter theorem modelFiber_restrict {C : ℕ} {n : Fin C → ℕ} (I : Finset (ModelVertex n)) (i j : Fin C) (hij : i ≤ j) : modelFiber (modelRestrict I i) j = modelFiber I j := by classical ext x simp only [modelFiber, Finset.mem_filter, Finset.mem_univ, true_and] exact (mem_modelRestrict I i (⟨j, x⟩ : ModelVertex n)).trans (and_iff_left hij) theorem modelLaterWeight_restrict {C : ℕ} {n : Fin C → ℕ} (I : Finset (ModelVertex n)) (i : Fin C) : modelLaterWeight (modelRestrict I i) i = modelLaterWeight I i := by unfold modelLaterWeight apply Finset.sum_congr rfl intro j hj split_ifs with hij · simp only [modelDensity, modelFiber_restrict I i j hij.le] · rfl /-- The exceptional independent sets can be searched for within a suffix. -/ def modelBadColor {C : ℕ} (n : Fin C → ℕ) (q : ℕ) : Set (ModelSample n) := {ω | ∃ i : Fin C, ∃ I : Finset (ModelVertex n), I ⊆ modelSuffix n i ∧ 1 / (4 * (q : ℝ)) ≤ modelDensity I i ∧ 15 * (q : ℝ) ≤ modelLaterWeight I i ∧ ∀ v ∈ I, ∀ w ∈ I, ¬ (modelGraph ω).Adj v w} theorem model_small_weights_of_not_bad {q C : ℕ} (hq : 1 ≤ q) (hC : C = 64 * q ^ 2) {n : Fin C → ℕ} (hn : ∀ j, 0 < n j) (ω : ModelSample n) (hω : ω ∉ modelBadColor n q) (I : Finset (ModelVertex n)) (hI : ∀ v ∈ I, ∀ w ∈ I, ¬ (modelGraph ω).Adj v w) : modelWeight I < (C : ℝ) / (2 * q) := by classical by_contra! hlarge obtain ⟨i, hi, hright⟩ := model_weight_heavy_part hq hC hn I hlarge apply hω refine ⟨i, modelRestrict I i, ?_, ?_, ?_, ?_⟩ · intro v hv exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, ((mem_modelRestrict I i v).mp hv).2⟩ · simpa only [modelDensity, modelFiber_restrict I i i le_rfl] using hi · simpa only [modelLaterWeight_restrict] using hright · intro v hv w hw exact hI v ((mem_modelRestrict I i v).mp hv).1 w ((mem_modelRestrict I i w).mp hw).1 theorem model_heavy_independent_probability_le {q C : ℕ} (hq : 0 < q) {n : Fin C → ℕ} (hn : ∀ j, 0 < n j) (I : Finset (ModelVertex n)) (i : Fin C) (hi : 1 / (4 * (q : ℝ)) ≤ modelDensity I i) (hright : 15 * (q : ℝ) ≤ modelLaterWeight I i) : finiteProb {ω : ModelSample n | ∀ v ∈ I, ∀ w ∈ I, ¬ (modelGraph ω).Adj v w} ≤ Real.exp (-3 * (n i : ℝ)) := by have hqR : (0 : ℝ) < q := by exact_mod_cast hq have hnR : (0 : ℝ) < n i := by exact_mod_cast hn i have ht : (n i : ℝ) ≤ ((modelFiber I i).card : ℝ) * (4 * q) := by have hb := (div_le_div_iff₀ (show (0 : ℝ) < 4 * q by positivity) hnR).mp hi simpa only [one_mul] using hb have hprod := mul_le_mul_of_nonneg_left hright (show (0 : ℝ) ≤ (modelFiber I i).card by positivity) apply (model_independent_probability_le hn I i).trans apply Real.exp_le_exp.mpr nlinarith /-- A union bound over all suffix sets and all possible first heavy parts. -/ theorem model_badColor_probability_le {q C : ℕ} (hq : 0 < q) (hC : 0 < C) {n : Fin C → ℕ} (hn : ∀ j, 0 < n j) (hsuffix : ∀ i, (modelSuffix n i).card ≤ 2 * n i) (hlarge : ∀ i, 8 * C ≤ n i) : finiteProb (modelBadColor n q) ≤ (1 : ℝ) / 8 := by classical let A : Fin C → Finset (ModelVertex n) → Set (ModelSample n) := fun i I => {ω | 1 / (4 * (q : ℝ)) ≤ modelDensity I i ∧ 15 * (q : ℝ) ≤ modelLaterWeight I i ∧ ∀ v ∈ I, ∀ w ∈ I, ¬ (modelGraph ω).Adj v w} have hfixed : ∀ i I, finiteProb (A i I) ≤ Real.exp (-3 * (n i : ℝ)) := by intro i I by_cases hi : 1 / (4 * (q : ℝ)) ≤ modelDensity I i · by_cases hr : 15 * (q : ℝ) ≤ modelLaterWeight I i · exact (finiteProb_mono (fun _ h => h.2.2)).trans (model_heavy_independent_probability_le hq hn I i hi hr) · have heq : A i I = ∅ := by ext ω; simp [A, hr] rw [heq, finiteProb_empty] exact Real.exp_nonneg _ · have heq : A i I = ∅ := by ext ω exact ⟨fun h => (hi h.1).elim, fun h => h.elim⟩ rw [heq, finiteProb_empty] exact Real.exp_nonneg _ have hpart : ∀ i, finiteProb {ω | ∃ I ∈ (modelSuffix n i).powerset, ω ∈ A i I} ≤ 1 / (8 * (C : ℝ)) := by intro i have hnR : (0 : ℝ) < n i := by exact_mod_cast hn i have hCR : (0 : ℝ) < C := by exact_mod_cast hC calc _ ≤ ∑ I ∈ (modelSuffix n i).powerset, finiteProb (A i I) := finiteProb_biUnion_le _ _ _ ≤ ∑ _I ∈ (modelSuffix n i).powerset, Real.exp (-3 * (n i : ℝ)) := Finset.sum_le_sum (fun I _ => hfixed i I) _ = (2 : ℝ) ^ (modelSuffix n i).card * Real.exp (-3 * (n i : ℝ)) := by simp _ ≤ (2 : ℝ) ^ (2 * n i) * Real.exp (-3 * (n i : ℝ)) := by gcongr · norm_num · exact hsuffix i _ ≤ Real.exp (2 * (n i : ℝ)) * Real.exp (-3 * (n i : ℝ)) := by apply mul_le_mul_of_nonneg_right _ (Real.exp_nonneg _) calc _ ≤ Real.exp 1 ^ (2 * n i) := pow_le_pow_left₀ (by norm_num) (by linarith [Real.add_one_le_exp (1 : ℝ)]) _ _ = _ := by rw [← Real.exp_nat_mul]; norm_cast; simp _ = Real.exp (-(n i : ℝ)) := by rw [← Real.exp_add]; congr 1; ring _ ≤ 1 / (8 * (C : ℝ)) := by rw [Real.exp_neg, one_div] apply (inv_le_inv₀ (Real.exp_pos _) (by positivity)).mpr have hlargeR : 8 * (C : ℝ) ≤ n i := by exact_mod_cast hlarge i linarith [Real.add_one_le_exp (n i : ℝ)] have heq : modelBadColor n q = {ω | ∃ i ∈ (Finset.univ : Finset (Fin C)), ∃ I ∈ (modelSuffix n i).powerset, ω ∈ A i I} := by ext ω simp only [modelBadColor, A, Set.mem_ofPred_eq, Finset.mem_univ, true_and, Finset.mem_powerset] calc _ = finiteProb {ω | ∃ i ∈ (Finset.univ : Finset (Fin C)), ∃ I ∈ (modelSuffix n i).powerset, ω ∈ A i I} := congrArg finiteProb heq _ ≤ ∑ i : Fin C, finiteProb {ω | ∃ I ∈ (modelSuffix n i).powerset, ω ∈ A i I} := finiteProb_biUnion_le _ _ _ ≤ ∑ _i : Fin C, 1 / (8 * (C : ℝ)) := Finset.sum_le_sum (fun i _ => hpart i) _ = 1 / 8 := by simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] field_simp /-- A convenient binomial estimate avoiding logarithms in the probability bounds. -/ theorem choose_le_three_mul_div_pow (N k : ℕ) (hk : 0 < k) : (N.choose k : ℝ) ≤ (3 * N / k) ^ k := by have hkR : (0 : ℝ) < k := by exact_mod_cast hk have hfact : (k : ℝ) ^ k / k.factorial ≤ (3 : ℝ) ^ k := by calc _ ≤ Real.exp k := Real.pow_div_factorial_le_exp (k : ℝ) (by positivity) k _ = Real.exp 1 ^ k := by simp [Real.exp_nat_mul] _ ≤ _ := pow_le_pow_left₀ (Real.exp_nonneg _) Real.exp_one_lt_three.le _ have hchoose := (Nat.choose_le_pow_div k N : (N.choose k : ℝ) ≤ (N : ℝ) ^ k / k.factorial) have hm := mul_le_mul_of_nonneg_left hfact (show 0 ≤ (N : ℝ) ^ k by positivity) have heq : (3 * (N : ℝ) / k) ^ k = (3 : ℝ) ^ k * (N : ℝ) ^ k / (k : ℝ) ^ k := by rw [div_pow, mul_pow] rw [heq] apply (le_div_iff₀ (pow_pos hkR _)).mpr have hc := mul_le_mul_of_nonneg_right hchoose (le_of_lt (pow_pos hkR k)) have he : (N : ℝ) ^ k / k.factorial * (k : ℝ) ^ k = (N : ℝ) ^ k * ((k : ℝ) ^ k / k.factorial) := by ring rw [he] at hc exact hc.trans (by simpa only [mul_comm] using hm) /-- Taking an integer power avoids fractional exponents in the sparse-set estimate. -/ theorem sparse_product_power_bound {a b δ : ℝ} {D x m : ℕ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hb1 : b ≤ 1) (hδ : 0 ≤ δ) (hD : 0 < D) (hm : (D + 1) * x ≤ m * D) (hcoef : a ^ D * b ^ (D + 1) ≤ δ ^ D) : a ^ x * b ^ m ≤ δ ^ x := by apply le_of_pow_le_pow_left₀ (Nat.ne_of_gt hD) (pow_nonneg hδ x) calc (a ^ x * b ^ m) ^ D = (a ^ D) ^ x * b ^ (m * D) := by simp only [mul_pow, ← pow_mul, Nat.mul_comm] _ ≤ (a ^ D) ^ x * b ^ ((D + 1) * x) := mul_le_mul_of_nonneg_left (pow_le_pow_of_le_one hb hb1 hm) (by positivity) _ = (a ^ D * b ^ (D + 1)) ^ x := by simp only [mul_pow, pow_mul] _ ≤ (δ ^ D) ^ x := pow_le_pow_left₀ (by positivity) hcoef x _ = (δ ^ x) ^ D := by simp only [← pow_mul, Nat.mul_comm] theorem sparse_binomial_bound {N L x m D : ℕ} {δ : ℝ} (hx : 0 < x) (hxm : x ≤ m) (hD : 0 < D) (hm : (D + 1) * x ≤ m * D) (hL : 3 * x ≤ L) (hδ : 0 ≤ δ) (hcoef : (3 : ℝ) ^ (2 * D + 1) * (N : ℝ) ^ D * x / (L : ℝ) ^ (D + 1) ≤ δ ^ D) : (N.choose x : ℝ) * ((x ^ 2).choose m : ℝ) * (1 / (L : ℝ)) ^ m ≤ δ ^ x := by have hxR : (0 : ℝ) < x := by exact_mod_cast hx have hmR : (0 : ℝ) < m := by exact_mod_cast lt_of_lt_of_le hx hxm have hLR : (0 : ℝ) < L := by exact_mod_cast (show 0 < L by omega) have hxmR : (x : ℝ) ≤ m := by exact_mod_cast hxm have hLR' : 3 * (x : ℝ) ≤ L := by exact_mod_cast hL let a : ℝ := 3 * N / x let b : ℝ := 3 * x / L have hchoose₁ : (N.choose x : ℝ) ≤ a ^ x := choose_le_three_mul_div_pow N x hx have hchoose₂ : ((x ^ 2).choose m : ℝ) ≤ (3 * (x : ℝ)) ^ m := by apply (choose_le_three_mul_div_pow (x ^ 2) m (by omega)).trans apply pow_le_pow_left₀ (by positivity) apply (div_le_iff₀ hmR).mpr push_cast nlinarith have hpow : a ^ D * b ^ (D + 1) ≤ δ ^ D := by have heq : a ^ D * b ^ (D + 1) = (3 : ℝ) ^ (2 * D + 1) * (N : ℝ) ^ D * x / (L : ℝ) ^ (D + 1) := by dsimp [a, b] rw [show 2 * D + 1 = D + (D + 1) by omega, pow_add] simp only [div_pow, mul_pow, pow_succ] field_simp ring rw [heq] exact hcoef calc _ ≤ a ^ x * (3 * (x : ℝ)) ^ m * (1 / (L : ℝ)) ^ m := by gcongr _ = a ^ x * b ^ m := by rw [mul_assoc, ← mul_pow] congr 1 dsimp [b] congr 1 ring _ ≤ _ := sparse_product_power_bound (by dsimp [a]; positivity) (by dsimp [b]; positivity) ((div_le_one₀ hLR).mpr hLR') hδ hD hm hpow /-- A union bound over all vertex sets of one specified size. -/ theorem model_fixed_size_density_probability_le {C : ℕ} {n : Fin C → ℕ} (P : Finset (ModelVertex n)) {x D L N : ℕ} {δ : ℝ} (hx : 0 < x) (hD : 0 < D) (hL : 3 * x ≤ L) (hδ : 0 ≤ δ) (hP : P.card ≤ N) (hsize : ∀ v ∈ P, L ≤ n v.1) (hcoef : (3 : ℝ) ^ (2 * D + 1) * (N : ℝ) ^ D * x / (L : ℝ) ^ (D + 1) ≤ δ ^ D) : finiteProb {ω : ModelSample n | ∃ X : Finset (ModelVertex n), X ⊆ P ∧ X.card = x ∧ (D + 1) * x ≤ (modelEdges ω X).card * D} ≤ δ ^ x := by classical have hmex : ∃ m : ℕ, (D + 1) * x ≤ m * D := ⟨(D + 1) * x, Nat.le_mul_of_pos_right _ hD⟩ let m := Nat.find hmex have hm : (D + 1) * x ≤ m * D := Nat.find_spec hmex have hxm : x ≤ m := by nlinarith have hLpos : 0 < L := by omega have hsub : {ω : ModelSample n | ∃ X : Finset (ModelVertex n), X ⊆ P ∧ X.card = x ∧ (D + 1) * x ≤ (modelEdges ω X).card * D} ⊆ {ω | ∃ X ∈ P.powersetCard x, m ≤ (modelEdges ω X).card} := by intro ω hω obtain ⟨X, hXP, hXx, hX⟩ := hω exact ⟨X, Finset.mem_powersetCard.mpr ⟨hXP, hXx⟩, Nat.find_min' hmex hX⟩ have hb : ∀ X ∈ P.powersetCard x, finiteProb {ω : ModelSample n | m ≤ (modelEdges ω X).card} ≤ ((x ^ 2).choose m : ℝ) * (1 / (L : ℝ)) ^ m := by intro X hX obtain ⟨hXP, hXx⟩ := Finset.mem_powersetCard.mp hX simpa only [hXx] using model_many_edges_probability_le X m hLpos (fun v hv => hsize v (hXP hv)) calc _ ≤ finiteProb {ω : ModelSample n | ∃ X ∈ P.powersetCard x, m ≤ (modelEdges ω X).card} := finiteProb_mono hsub _ ≤ ∑ X ∈ P.powersetCard x, finiteProb {ω : ModelSample n | m ≤ (modelEdges ω X).card} := finiteProb_biUnion_le _ _ _ ≤ ∑ _X ∈ P.powersetCard x, ((x ^ 2).choose m : ℝ) * (1 / (L : ℝ)) ^ m := Finset.sum_le_sum hb _ = (P.card.choose x : ℝ) * ((x ^ 2).choose m : ℝ) * (1 / (L : ℝ)) ^ m := by simp [mul_assoc] _ ≤ (N.choose x : ℝ) * ((x ^ 2).choose m : ℝ) * (1 / (L : ℝ)) ^ m := by gcongr _ ≤ _ := sparse_binomial_bound hx hxm hD hm hL hδ hcoef noncomputable def modelBefore {C : ℕ} (n : Fin C → ℕ) (i : Fin C) : Finset (ModelVertex n) := by classical exact Finset.univ.filter fun v => v.1 < i def modelBadSparse {C : ℕ} (n : Fin C → ℕ) (A D : ℕ) : Set (ModelSample n) := {ω | ∃ i : Fin C, ∃ X : Finset (ModelVertex n), X ⊆ modelBefore n i ∧ X.Nonempty ∧ X.card ≤ A * n i ∧ (D + 1) * X.card ≤ (modelEdges ω X).card * D} /-- Summing the dense-set estimate over sizes and parts. -/ theorem model_badSparse_probability_le {C A D : ℕ} (hC : 0 < C) (hD : 0 < D) {n : Fin C → ℕ} (hbounds : ∀ i : Fin C, 0 < i.val → ∀ x : ℕ, 0 < x → x ≤ A * n i → ∃ L N : ℕ, 3 * x ≤ L ∧ (modelBefore n i).card ≤ N ∧ (∀ v ∈ modelBefore n i, L ≤ n v.1) ∧ (3 : ℝ) ^ (2 * D + 1) * (N : ℝ) ^ D * x / (L : ℝ) ^ (D + 1) ≤ (1 / (16 * (C : ℝ))) ^ D) : finiteProb (modelBadSparse n A D) ≤ (1 : ℝ) / 8 := by classical let δ : ℝ := 1 / (16 * (C : ℝ)) have hCR : (0 : ℝ) < C := by exact_mod_cast hC have hδ : 0 ≤ δ := by dsimp [δ]; positivity have hδhalf : δ ≤ 1 / 2 := by dsimp [δ] apply one_div_le_one_div_of_le (by norm_num) have : (1 : ℝ) ≤ C := by exact_mod_cast hC linarith let E : Fin C → Set (ModelSample n) := fun i => {ω | ∃ X : Finset (ModelVertex n), X ⊆ modelBefore n i ∧ X.Nonempty ∧ X.card ≤ A * n i ∧ (D + 1) * X.card ≤ (modelEdges ω X).card * D} have hpart : ∀ i, finiteProb (E i) ≤ 1 / (8 * (C : ℝ)) := by intro i by_cases hiz : i.val = 0 · have heq : E i = ∅ := by ext ω constructor · rintro ⟨X, hX, hnonempty, _⟩ obtain ⟨v, hv⟩ := hnonempty have hvi : v.1 < i := (Finset.mem_filter.mp (hX hv)).2 have : v.1.val < i.val := hvi omega · exact fun h => h.elim rw [heq, finiteProb_empty] positivity · let B : ℕ → Set (ModelSample n) := fun k => {ω | ∃ X : Finset (ModelVertex n), X ⊆ modelBefore n i ∧ X.card = k + 1 ∧ (D + 1) * (k + 1) ≤ (modelEdges ω X).card * D} have hsub : E i ⊆ {ω | ∃ k ∈ Finset.range (A * n i), ω ∈ B k} := by rintro ω ⟨X, hX, hnonempty, hsize, hdense⟩ have hx : 0 < X.card := hnonempty.card_pos refine ⟨X.card - 1, Finset.mem_range.mpr (by omega), X, hX, by omega, ?_⟩ simpa only [Nat.sub_add_cancel (show 1 ≤ X.card by omega)] using hdense have hfixed : ∀ k ∈ Finset.range (A * n i), finiteProb (B k) ≤ δ ^ (k + 1) := by intro k hk have hk' : k + 1 ≤ A * n i := by have := Finset.mem_range.mp hk; omega obtain ⟨L, N, hL, hP, hsize, hcoef⟩ := hbounds i (by omega) (k + 1) (by omega) hk' exact model_fixed_size_density_probability_le (modelBefore n i) (by omega) hD hL hδ hP hsize hcoef calc _ ≤ finiteProb {ω | ∃ k ∈ Finset.range (A * n i), ω ∈ B k} := finiteProb_mono hsub _ ≤ ∑ k ∈ Finset.range (A * n i), finiteProb (B k) := finiteProb_biUnion_le _ _ _ ≤ ∑ k ∈ Finset.range (A * n i), δ ^ (k + 1) := Finset.sum_le_sum hfixed _ ≤ ∑ k ∈ Finset.range (A * n i), δ * ((1 : ℝ) / 2) ^ k := by apply Finset.sum_le_sum intro k hk rw [pow_succ'] exact mul_le_mul_of_nonneg_left (pow_le_pow_left₀ hδ hδhalf k) hδ _ = δ * (∑ k ∈ Finset.range (A * n i), ((1 : ℝ) / 2) ^ k) := (Finset.mul_sum _ _ _).symm _ ≤ δ * 2 := mul_le_mul_of_nonneg_left (sum_geometric_two_le _) hδ _ = 1 / (8 * (C : ℝ)) := by dsimp [δ]; ring have heq : modelBadSparse n A D = {ω | ∃ i ∈ (Finset.univ : Finset (Fin C)), ω ∈ E i} := by ext ω simp only [modelBadSparse, E, Set.mem_ofPred_eq, Finset.mem_univ, true_and] calc _ = finiteProb {ω | ∃ i ∈ (Finset.univ : Finset (Fin C)), ω ∈ E i} := congrArg finiteProb heq _ ≤ ∑ i : Fin C, finiteProb (E i) := finiteProb_biUnion_le _ _ _ ≤ ∑ _i : Fin C, 1 / (8 * (C : ℝ)) := Finset.sum_le_sum (fun i _ => hpart i) _ = 1 / 8 := by simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] field_simp theorem model_sparse_of_not_bad {C A D : ℕ} (hD : 0 < D) {n : Fin C → ℕ} (ω : ModelSample n) (hω : ω ∉ modelBadSparse n A D) (i : Fin C) (X : Finset (ModelVertex n)) (hX : ∀ v ∈ X, v.1 < i) (hsize : X.card ≤ A * n i) : internalCount (modelGraph ω) X ≤ (1 + 1 / (D : ℝ)) * X.card := by classical by_cases hx : X.Nonempty · have hbad : ¬ (D + 1) * X.card ≤ (modelEdges ω X).card * D := by intro h apply hω exact ⟨i, X, fun v hv => Finset.mem_filter.mpr ⟨Finset.mem_univ _, hX v hv⟩, hx, hsize, h⟩ have hlt : ((modelEdges ω X).card : ℝ) * D < ((D : ℝ) + 1) * X.card := by exact_mod_cast lt_of_not_ge hbad rw [internalCount_modelGraph] have hDR : (0 : ℝ) < D := by exact_mod_cast hD have heq : (1 + 1 / (D : ℝ)) * X.card = ((D + 1) * X.card) / (D : ℝ) := by field_simp rw [heq] exact (le_div_iff₀ hDR).mpr hlt.le · have heq : X = ∅ := Finset.not_nonempty_iff_eq_empty.mp hx subst X simp [internalCount, crossingCount] theorem model_card {C : ℕ} (n : Fin C → ℕ) : Fintype.card (ModelVertex n) = ∑ i, n i := by change Fintype.card (Σ i : Fin C, Fin (n i)) = _ simp only [Fintype.card_sigma, Fintype.card_fin] theorem model_count_parts {C : ℕ} (n : Fin C → ℕ) (P : Fin C → Prop) [DecidablePred P] : ((Finset.univ : Finset (ModelVertex n)).filter (fun v => P v.1)).card = ∑ i : Fin C, if P i then n i else 0 := by classical rw [Finset.card_eq_sum_ones, Finset.sum_filter] change (∑ v : Σ i : Fin C, Fin (n i), if P v.1 then (1 : ℕ) else 0) = _ rw [Fintype.sum_sigma] apply Finset.sum_congr rfl intro i hi by_cases hp : P i <;> simp only [hp, if_true, if_false, Finset.sum_const, Finset.card_univ, Fintype.card_fin, smul_eq_mul, mul_one, mul_zero] theorem model_filter_card_le {C : ℕ} {n : Fin C → ℕ} (S : Finset (ModelVertex n)) (P : Fin C → Prop) [DecidablePred P] : (S.filter (fun v => P v.1)).card ≤ ∑ i : Fin C, if P i then n i else 0 := by rw [← model_count_parts n P] exact Finset.card_le_card (Finset.filter_subset_filter _ (Finset.subset_univ _)) theorem model_suffix_card_le {C : ℕ} (hC : 0 < C) {n : Fin C → ℕ} (hsep : ∀ i j : Fin C, i < j → C * n j ≤ n i) (i : Fin C) : (modelSuffix n i).card ≤ 2 * n i := by classical let t : ℕ := ∑ j : Fin C, if i < j then n j else 0 have hmul : C * t ≤ C * n i := by dsimp [t] rw [Finset.mul_sum] calc _ ≤ ∑ _j : Fin C, n i := by apply Finset.sum_le_sum intro j hj by_cases hij : i < j · simpa only [if_pos hij] using hsep i j hij · simp only [if_neg hij, mul_zero, Nat.zero_le] _ = _ := by simp have ht : t ≤ n i := Nat.le_of_mul_le_mul_left hmul hC have hcard : (modelSuffix n i).card = n i + t := by rw [modelSuffix, model_count_parts] calc _ = ∑ j : Fin C, ((if j = i then n i else 0) + (if i < j then n j else 0)) := by apply Finset.sum_congr rfl intro j hj rcases lt_trichotomy i j with hij | rfl | hij · simp only [if_pos hij.le, if_neg hij.ne.symm, if_pos hij, zero_add] · simp · simp only [if_neg hij.not_ge, if_neg hij.ne, if_neg hij.not_gt, add_zero] _ = _ := by simp only [Finset.sum_add_distrib, Finset.sum_ite_eq', Finset.mem_univ, if_true, t] omega /-- The last part large enough for a set provides the deterministic sparse cut. -/ theorem model_size_cut {C K A : ℕ} (hC : 0 < C) (hK : 4 ≤ K) (hA : A = 16 * C * K * (K + 1)) {n : Fin C → ℕ} (hmono : Antitone n) (S : Finset (ModelVertex n)) (hS : S.Nonempty) : ∃ i : Fin C, S.card ≤ A * n i ∧ ((S.filter (fun v => i < v.1)).card : ℝ) < 2 * S.card / (16 * K * (K + 1)) := by classical let z : Fin C := ⟨0, hC⟩ have hCA : C ≤ A := by rw [hA] have hmul : 1 ≤ 16 * K * (K + 1) := by nlinarith nlinarith have htotal : Fintype.card (ModelVertex n) ≤ C * n z := by rw [model_card] calc _ ≤ ∑ _i : Fin C, n z := Finset.sum_le_sum (fun j _ => hmono (by exact Nat.zero_le _)) _ = _ := by simp have hz : S.card ≤ A * n z := (Finset.card_le_univ S).trans (htotal.trans (Nat.mul_le_mul_right _ hCA)) let Q := Finset.univ.filter (fun i : Fin C => S.card ≤ A * n i) have hQ : Q.Nonempty := ⟨z, Finset.mem_filter.mpr ⟨Finset.mem_univ _, hz⟩⟩ let i := Q.max' hQ refine ⟨i, (Finset.mem_filter.mp (Finset.max'_mem Q hQ)).2, ?_⟩ have hKR : (0 : ℝ) < 16 * K * (K + 1) := by positivity have hSR : (0 : ℝ) < S.card := by exact_mod_cast hS.card_pos by_cases hnext : i.val + 1 < C · let j : Fin C := ⟨i.val + 1, hnext⟩ have hij : i < j := by change i.val < i.val + 1; omega have hjbig : A * n j < S.card := by by_contra! hbad have hji : j ≤ i := Finset.le_max' Q j (Finset.mem_filter.mpr ⟨Finset.mem_univ _, hbad⟩) exact (not_lt_of_ge hji) hij have htail : (S.filter (fun v => i < v.1)).card ≤ C * n j := by apply (model_filter_card_le S (fun k => i < k)).trans calc _ ≤ ∑ _k : Fin C, n j := by apply Finset.sum_le_sum intro k hk by_cases hik : i < k · simp only [if_pos hik] exact hmono (show j ≤ k by change i.val + 1 ≤ k.val; exact hik) · simp only [if_neg hik, Nat.zero_le] _ = _ := by simp have htailR : ((S.filter (fun v => i < v.1)).card : ℝ) ≤ C * n j := by exact_mod_cast htail have hjR : (16 * (C : ℝ) * K * (K + 1)) * n j < S.card := by rw [hA] at hjbig exact_mod_cast hjbig apply (lt_div_iff₀ hKR).mpr have hm := mul_le_mul_of_nonneg_right htailR hKR.le nlinarith · have hempty : S.filter (fun v => i < v.1) = ∅ := by apply Finset.eq_empty_iff_forall_notMem.mpr intro v hv have hvi : i.val < v.1.val := (Finset.mem_filter.mp hv).2 have hvC := v.1.isLt omega rw [hempty, Finset.card_empty, Nat.cast_zero] positivity /-- Explicit, widely separated part sizes satisfying both probability estimates. -/ theorem model_sizes_exist {C A D : ℕ} (hC : 0 < C) (hD : 0 < D) : ∃ n : Fin C → ℕ, (∀ i, 0 < n i) ∧ Antitone n ∧ (∀ i j : Fin C, i < j → C * n j ≤ n i) ∧ (∀ i, 8 * C ≤ n i) ∧ ∀ i : Fin C, 0 < i.val → ∀ x : ℕ, 0 < x → x ≤ A * n i → ∃ L N : ℕ, 3 * x ≤ L ∧ (modelBefore n i).card ≤ N ∧ (∀ v ∈ modelBefore n i, L ≤ n v.1) ∧ (3 : ℝ) ^ (2 * D + 1) * (N : ℝ) ^ D * x / (L : ℝ) ^ (D + 1) ≤ (1 / (16 * (C : ℝ))) ^ D := by classical let R := (16 * C) ^ D * 3 ^ (2 * D + 1) * A + 3 * A + 8 * C + 2 let b := D + 2 let B := b ^ (C + 1) let n : Fin C → ℕ := fun i => R ^ (B - b ^ (i.val + 1)) have hR : 2 ≤ R := by dsimp [R]; omega have hRC : C ≤ R := by dsimp [R]; omega have hRlarge : 8 * C ≤ R := by dsimp [R]; omega have hRA : 3 * A ≤ R := by dsimp [R]; omega have hRcoef : (16 * C) ^ D * 3 ^ (2 * D + 1) * A ≤ R := by dsimp [R]; omega have hb : 1 < b := by dsimp [b]; omega have hB : 0 < B := by dsimp [B]; positivity have hpowlt : ∀ i : Fin C, b ^ (i.val + 1) < B := by intro i exact pow_lt_pow_right₀ hb (by have := i.isLt; omega) have hnR : ∀ i, R ≤ n i := by intro i calc R = R ^ 1 := by simp _ ≤ _ := pow_le_pow_right₀ (by omega) (by have := hpowlt i; omega) have hn : ∀ i, 0 < n i := fun i => lt_of_lt_of_le (by omega) (hnR i) have hmono : Antitone n := by intro i j hij apply pow_le_pow_right₀ (by omega) have hp : b ^ (i.val + 1) ≤ b ^ (j.val + 1) := pow_le_pow_right₀ hb.le (by exact Nat.add_le_add_right hij 1) exact Nat.sub_le_sub_left hp B have hgap : ∀ i j : Fin C, i < j → R * n j ≤ n i := by intro i j hij change R * R ^ (B - b ^ (j.val + 1)) ≤ R ^ (B - b ^ (i.val + 1)) rw [← pow_succ'] apply pow_le_pow_right₀ (by omega) have hp : b ^ (i.val + 1) < b ^ (j.val + 1) := pow_lt_pow_right₀ hb (by exact Nat.add_lt_add_right hij 1) have := hpowlt j omega have hsep : ∀ i j : Fin C, i < j → C * n j ≤ n i := fun i j hij => (Nat.mul_le_mul_right _ hRC).trans (hgap i j hij) have htotal : Fintype.card (ModelVertex n) ≤ R ^ B := by rw [model_card] have hsmall : ∀ i : Fin C, n i ≤ R ^ (B - 1) := by intro i apply pow_le_pow_right₀ (by omega) apply Nat.sub_le_sub_left exact Nat.one_le_pow _ _ (by omega) calc _ ≤ ∑ _i : Fin C, R ^ (B - 1) := Finset.sum_le_sum (fun i _ => hsmall i) _ = C * R ^ (B - 1) := by simp _ ≤ R * R ^ (B - 1) := Nat.mul_le_mul_right _ hRC _ = R ^ B := by rw [← pow_succ', Nat.sub_add_cancel hB] refine ⟨n, hn, hmono, hsep, fun i => hRlarge.trans (hnR i), ?_⟩ intro i hi x hx hxi let p : Fin C := ⟨i.val - 1, by have := i.isLt; omega⟩ let L := n p let N := R ^ B have hpi : p < i := by change i.val - 1 < i.val; omega have hL : L = R ^ (B - b ^ i.val) := by dsimp [L, n, p] rw [Nat.sub_add_cancel hi] have hLR : 0 < L := hn p have hthree : 3 * x ≤ L := calc 3 * x ≤ 3 * (A * n i) := Nat.mul_le_mul_left _ hxi _ = (3 * A) * n i := by ring _ ≤ R * n i := Nat.mul_le_mul_right _ hRA _ ≤ L := hgap p i hpi have hP : (modelBefore n i).card ≤ N := (Finset.card_filter_le _ _).trans htotal have hmin : ∀ v ∈ modelBefore n i, L ≤ n v.1 := by intro v hv apply hmono have hvi : v.1.val < i.val := (Finset.mem_filter.mp hv).2 change v.1.val ≤ i.val - 1 omega have hden : R * N ^ D * n i ≤ L ^ (D + 1) := by rw [hL] change R * (R ^ B) ^ D * R ^ (B - b ^ (i.val + 1)) ≤ (R ^ (B - b ^ i.val)) ^ (D + 1) rw [← pow_mul, ← pow_succ', ← pow_add, ← pow_mul] apply pow_le_pow_right₀ (by omega) have ht : 1 ≤ b ^ i.val := Nat.one_le_pow _ _ (by omega) have hbig : b ^ (i.val + 1) ≤ B := (hpowlt i).le have hsmall : b ^ i.val ≤ B := (pow_le_pow_right₀ hb.le (by omega : i.val ≤ i.val + 1)).trans hbig have he₁ := Nat.sub_add_cancel hsmall have he₂ := Nat.sub_add_cancel hbig rw [pow_succ] at he₂ ⊢ dsimp [b] at ht he₁ he₂ ⊢ nlinarith have hnat : 3 ^ (2 * D + 1) * N ^ D * x * (16 * C) ^ D ≤ L ^ (D + 1) := calc _ ≤ 3 ^ (2 * D + 1) * N ^ D * (A * n i) * (16 * C) ^ D := Nat.mul_le_mul_right _ (Nat.mul_le_mul_left _ hxi) _ = ((16 * C) ^ D * 3 ^ (2 * D + 1) * A) * (N ^ D * n i) := by ring _ ≤ R * (N ^ D * n i) := Nat.mul_le_mul_right _ hRcoef _ ≤ L ^ (D + 1) := by simpa only [mul_assoc] using hden refine ⟨L, N, hthree, hP, hmin, ?_⟩ rw [div_pow, one_pow] apply (div_le_div_iff₀ (by exact_mod_cast pow_pos hLR (D + 1)) (by positivity : (0 : ℝ) < (16 * C) ^ D)).mpr simpa only [one_mul] using (show (3 : ℝ) ^ (2 * D + 1) * (N : ℝ) ^ D * x * (16 * (C : ℝ)) ^ D ≤ (L : ℝ) ^ (D + 1) by exact_mod_cast hnat) /-- The probabilistic base graph: large chromatic number and sparse bounded-degree subgraphs. -/ theorem model_base_exists {q K : ℕ} (hq : 1 ≤ q) (hK : 4 ≤ K) : ∃ n : Fin (64 * q ^ 2) → ℕ, ∃ ω : ModelSample n, ¬ (modelGraph ω).Colorable (2 * q) ∧ ∀ J : SimpleGraph (ModelVertex n), J ≤ modelGraph ω → (∀ v, Nat.card (J.neighborSet v) ≤ K) → J.Colorable 4 := by classical let C := 64 * q ^ 2 let A := 16 * C * K * (K + 1) let D := 2 * (K + 1) have hqpos : 0 < q := by omega have hC : 0 < C := by dsimp [C]; positivity have hD : 0 < D := by dsimp [D]; positivity obtain ⟨n, hn, hmono, hsep, hlarge, hbounds⟩ := model_sizes_exist (A := A) hC hD let : Nonempty (ModelSample n) := ⟨fun k => ⟨0, hn k.2⟩⟩ have hcolor := model_badColor_probability_le hqpos hC hn (model_suffix_card_le hC hsep) hlarge have hsparse := model_badSparse_probability_le hC hD hbounds obtain ⟨ω, hωcolor, hωsparse⟩ := exists_avoiding_of_finiteProb_lt_one (modelBadColor n q) (modelBadSparse n A D) (by linarith) refine ⟨n, ω, ?_, ?_⟩ · apply model_not_colorable_of_independent_weights hn (by omega) ω intro I hI simpa only [C, Nat.cast_mul, Nat.cast_ofNat] using model_small_weights_of_not_bad hq rfl hn ω hωcolor I hI · have hcuts : SparseCutProperty (modelGraph ω) K := by apply sparse_cuts_of_parts (A := A) (fun v : ModelVertex n => v.1) n (modelGraph_same_part ω) (modelGraph_one_neighbor ω) · exact model_size_cut hC hK rfl hmono · intro i X hX hsize simpa only [D, Nat.cast_mul, Nat.cast_add, Nat.cast_one, Nat.cast_ofNat] using model_sparse_of_not_bad hD ω hωsparse i X hX hsize intro J hJ hdeg exact colorable_four_of_sparse_cuts hK hcuts hJ hdeg /-- Arc graphs have arbitrarily large chromatic number while their four-cycle-free subgraphs are six-colorable. -/ theorem arc_counterexample_family (M : ℕ) : ∃ (V : Type) (G : SimpleGraph V), Nonempty V ∧ M ≤ G.chromaticNumber ∧ ∀ J : SimpleGraph V, J ≤ G → FourCycleFree J → J.Colorable 6 := by classical let q : ℕ := 2 ^ M + 2 let d := 64 * q ^ 2 - 1 let K := d + d.choose 2 have hq : 1 ≤ q := Nat.succ_le_succ (Nat.zero_le (2 ^ M + 1)) have hd : 4 ≤ d := by have hbig : 64 ≤ 64 * q ^ 2 := by nlinarith dsimp [d] omega have hK : 4 ≤ K := by dsimp [K]; omega obtain ⟨n, ω, hnot, hbase⟩ := model_base_exists hq hK let F := modelGraph ω have hnotArc : ¬ (arcGraph F).Colorable M := by intro hc apply hnot exact (base_colorable_of_arc_colorable hc).mono (by dsimp [q]; omega) have hV : Nonempty (Arc F) := by by_contra hempty let : IsEmpty (Arc F) := not_nonempty_iff.mp hempty exact hnotArc (SimpleGraph.Colorable.of_isEmpty M) have hchi : (M : ℕ∞) ≤ (arcGraph F).chromaticNumber := by apply le_of_lt apply lt_of_not_ge intro h exact hnotArc (SimpleGraph.chromaticNumber_le_iff_colorable.mp h) refine ⟨Arc F, arcGraph F, hV, hchi, ?_⟩ intro J hJ h4 exact arc_colorable_bound (d := d) (a := 4) (model_outgoing_card_le ω) hbase hJ h4 /-- The counterexample is available in every universe occurring in the conjecture. -/ theorem counterexample_family (M : ℕ) : ∃ (V : Type u) (G : SimpleGraph V), Nonempty V ∧ M ≤ G.chromaticNumber ∧ ∀ H : G.Subgraph, 5 ≤ H.coe.girth → H.coe.Colorable 6 := by classical obtain ⟨V, G, hV, hchi, hcolor⟩ := arc_counterexample_family M let W := ULift.{u} V let G' : SimpleGraph W := G.comap ULift.down let e : G' ≃g G := SimpleGraph.Iso.comap Equiv.ulift G have hW : Nonempty W := hV.map ULift.up refine ⟨W, G', hW, ?_, ?_⟩ · simpa only [SimpleGraph.chromaticNumber_congr e] using hchi · intro H hg have h4 : FourCycleFree H.spanningCoe := (fourCycleFree_of_girth_ge_five hg).spanningCoe let J : SimpleGraph V := H.spanningCoe.comap ULift.up have hJG : J ≤ G := by intro a b hab exact H.adj_sub hab have hJ4 : FourCycleFree J := by intro a b x y hab hxy hax hay hbx hby exact h4 (ULift.up a) (ULift.up b) (ULift.up x) (ULift.up y) (fun h => hab (congrArg ULift.down h)) (fun h => hxy (congrArg ULift.down h)) hax hay hbx hby have hc : J.Colorable 6 := hcolor J hJG hJ4 let f : H.coe →g J := { toFun := fun v => v.val.down map_rel' := by intro v w hvw change H.Adj v.val w.val at hvw change H.Adj (ULift.up v.val.down) (ULift.up w.val.down) simpa only [ULift.up_down] using hvw } exact hc.of_hom f /-- The final logical reduction at girth five and chromatic number seven. -/ theorem counterexample_of_family (hfamily : ∀ M : ℕ, ∃ (V : Type u) (G : SimpleGraph V), Nonempty V ∧ M ≤ G.chromaticNumber ∧ ∀ H : G.Subgraph, 5 ≤ H.coe.girth → H.coe.Colorable 6) : ¬ (fcTypeOfName% "Erdos108.erdos_108") := by intro h obtain ⟨f, hf⟩ := h.mp trivial 5 (by decide) 7 (by decide) obtain ⟨V, G, hV, hchi, hG⟩ := hfamily f obtain ⟨H, hgirth, hseven⟩ := hf V G hV hchi have hsix := (hG H hgirth).chromaticNumber_le have hbad : (7 : ℕ∞) ≤ 6 := hseven.trans hsix norm_num at hbad theorem target : ¬ (fcTypeOfName% "Erdos108.erdos_108") := by exact counterexample_of_family counterexample_family