From ae455e738408cee6cf0414794475225da76cacae Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Sun, 22 Oct 2023 16:46:06 +0100 Subject: [PATCH] linter --- src/analysis/calculus/taylor_mathlib.lean | 1 + .../exponential_ramsey/main_results.lean | 41 ++++++++++++------- .../exponential_ramsey/section9.lean | 2 +- 3 files changed, 28 insertions(+), 16 deletions(-) diff --git a/src/analysis/calculus/taylor_mathlib.lean b/src/analysis/calculus/taylor_mathlib.lean index 061bf715f85b0..75ef2f2acf13e 100644 --- a/src/analysis/calculus/taylor_mathlib.lean +++ b/src/analysis/calculus/taylor_mathlib.lean @@ -19,6 +19,7 @@ section variables {α : Type*} [lattice α] +/-- The unordered open-open interval. -/ def uIoo (x y : α) : set α := Ioo (x ⊓ y) (x ⊔ y) lemma uIoo_of_le {x y : α} (h : x ≤ y) : uIoo x y = Ioo x y := diff --git a/src/combinatorics/simple_graph/exponential_ramsey/main_results.lean b/src/combinatorics/simple_graph/exponential_ramsey/main_results.lean index 36bf2c4c3bd72..909ba09e5dc63 100644 --- a/src/combinatorics/simple_graph/exponential_ramsey/main_results.lean +++ b/src/combinatorics/simple_graph/exponential_ramsey/main_results.lean @@ -18,17 +18,28 @@ namespace main_results open simple_graph open simple_graph.top_edge_labelling --- This lemma characterises our definition of Ramsey numbers. --- Since `fin k` denotes the numbers `{0, ..., k - 1}`, we can think of a function `fin k → ℕ` --- as being a vector in `ℕ^k`, ie `n = (n₀, n₁, ..., nₖ₋₁)`. Then our definition of `R(n)` satisfies --- `R(n) ≤ N` if and only if, for any labelling `C` of the edges of the complete graph on --- `{0, ..., N - 1}`, there is a finite subset `m` of this graph's vertices, and a label `i` such --- that `|m| ≥ nᵢ`, and all edges of `m` are labelled `i`. -lemma ramsey_number_le_iff {k N : ℕ} (n : fin k → ℕ) : - ramsey_number n ≤ N ↔ - ∀ (C : (complete_graph (fin N)).edge_set → fin k), - ∃ m : finset (fin N), ∃ i : fin k, monochromatic_of C m i ∧ n i ≤ m.card := -ramsey_number_le_iff_fin +/-- +Since `fin t` denotes the numbers `{0, ..., t - 1}`, we can think of a function `fin t → ℕ` +as being a vector in `ℕ^t`, ie `n = (n₀, n₁, ..., nₜ₋₁)`. +Then `is_ramsey_valid (fin N) n` means that for any labelling `C` of the edges of the complete graph +on `{0, ..., N - 1}`, there is a finite subset `m` of this graph's vertices, and a label `i` such +that `|m| ≥ nᵢ`, and all edges between vertices in `m` are labelled `i`. +In the two-colour case discussed in the blogpost, we would have `t = 2`, and `n = (k, l)`. +In Lean this is denoted by `![k, l]`, as in the examples below. +-/ +lemma ramsey_valid_iff {t N : ℕ} (n : fin t → ℕ) : + is_ramsey_valid (fin N) n = + ∀ (C : (complete_graph (fin N)).edge_set → fin t), + ∃ m : finset (fin N), ∃ i : fin t, monochromatic_of C m i ∧ n i ≤ m.card := +rfl + +/-- +The ramsey number of the vector `n` is then just the infimum of all `N` such that +`is_ramsey_valid (fin N) n`. +-/ +lemma ramsey_number_def {t : ℕ} (n : fin t → ℕ) : + ramsey_number n = Inf {N | is_ramsey_valid (fin N) n} := +(nat.find_eq_iff _).2 ⟨Inf_mem (ramsey_fin_exists n), λ m, nat.not_mem_of_lt_Inf⟩ -- We've got a definition of Ramsey numbers, let's first make sure it satisfies some of -- the obvious properties. @@ -36,9 +47,9 @@ example : ∀ k, ramsey_number ![2, k] = k := by simp example : ∀ k l, ramsey_number ![k, l] = ramsey_number ![l, k] := ramsey_number_pair_swap -- It also satisfies the inductive bound by Erdős-Szekeres -lemma ramsey_number_inductive_bound : ∀ k l, k ≥ 2 → l ≥ 2 → +lemma ramsey_number_inductive_bound : ∀ k ≥ 2, ∀ l ≥ 2, ramsey_number ![k, l] ≤ ramsey_number ![k - 1, l] + ramsey_number ![k, l - 1] := -λ _ _, ramsey_number_two_colour_bound_aux +λ _ h _, ramsey_number_two_colour_bound_aux h -- And we can use this bound to get the standard upper bound in terms of the binomial coefficient, -- which is written `n.choose k` in Lean. @@ -58,14 +69,14 @@ example : ramsey_number ![4, 4] = 18 := ramsey_number_four_four example : ramsey_number ![3, 3, 3] = 17 := ramsey_number_three_three_three -- We also have Erdős' lower bound on Ramsey numbers -lemma ramsey_number_lower_bound : ∀ k, 2 ≤ k → real.sqrt 2 ^ k ≤ ramsey_number ![k, k] := +lemma ramsey_number_lower_bound : ∀ k ≥ 2, real.sqrt 2 ^ k ≤ ramsey_number ![k, k] := λ _, diagonal_ramsey_lower_bound_simpler -- Everything up to this point has been known results, which were needed for the formalisation, -- served as a useful warm up to the main result, and hopefully demonstrate the correctness -- of the definition of Ramsey numbers. --- Finally, the titutar statement, giving an exponential improvement to the upper bound on Ramsey +-- Finally, the titular statement, giving an exponential improvement to the upper bound on Ramsey -- numbers. theorem exponential_ramsey_improvement : ∃ ε > 0, ∀ k, (ramsey_number ![k, k] : ℝ) ≤ (4 - ε) ^ k := global_bound diff --git a/src/combinatorics/simple_graph/exponential_ramsey/section9.lean b/src/combinatorics/simple_graph/exponential_ramsey/section9.lean index 1c2d34b48d6d8..51314a3212edb 100644 --- a/src/combinatorics/simple_graph/exponential_ramsey/section9.lean +++ b/src/combinatorics/simple_graph/exponential_ramsey/section9.lean @@ -1313,7 +1313,7 @@ end end /-- The density of a label in the edge labelling. -/ -def top_edge_labelling.density [fintype V] {K : Type*} [decidable_eq K] (χ : top_edge_labelling V K) +def top_edge_labelling.density [fintype V] {K : Type*} (χ : top_edge_labelling V K) (k : K) [fintype (χ.label_graph k).edge_set] : ℝ := density (χ.label_graph k)