linter

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 :=

src/combinatorics/simple_graph/exponential_ramsey/main_results.lean

@@ -18,27 +18,38 @@ 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.
 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

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)