Merge branch 'feat-clique-number' into feat-independence-set

Archive.lean

@@ -18,6 +18,7 @@ import Archive.Imo.Imo1972Q5
 import Archive.Imo.Imo1975Q1
 import Archive.Imo.Imo1977Q6
 import Archive.Imo.Imo1981Q3
+import Archive.Imo.Imo1982Q1
 import Archive.Imo.Imo1986Q5
 import Archive.Imo.Imo1987Q1
 import Archive.Imo.Imo1988Q6
@@ -62,6 +63,6 @@ import Archive.Wiedijk100Theorems.InverseTriangleSum
 import Archive.Wiedijk100Theorems.Konigsberg
 import Archive.Wiedijk100Theorems.Partition
 import Archive.Wiedijk100Theorems.PerfectNumbers
-import Archive.Wiedijk100Theorems.SolutionOfCubic
+import Archive.Wiedijk100Theorems.SolutionOfCubicQuartic
 import Archive.Wiedijk100Theorems.SumOfPrimeReciprocalsDiverges
 import Archive.ZagierTwoSquares

Archive/Imo/Imo1982Q1.lean

@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2024 Alex Brodbelt. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex Brodbelt, Violeta Hernández
+-/
+
+import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Linarith
+import Mathlib.Data.PNat.Basic
+
+/-!
+# IMO 1982 Q1
+
+The function `f` is defined for all positive integers `n` and takes on
+non-negative integer values. Also, for all `m`, `n`
+
+`f (m + n) - f(m) - f(n) = 0` or `1`
+`f 2 = 0`, `f 3 > 0`, and `f 9999 = 3333`.
+
+Determine `f 1982`.
+
+The solution is based on the one at the
+[Art of Problem Solving](https://artofproblemsolving.com/wiki/index.php/1982_IMO_Problems/Problem_1)
+website.
+
+We prove the helper lemmas:
+1. `f m + f n ≤ f(m + n)` `superadditive`.
+2. `n * f(m) ≤ f(m * n)` `superhomogeneous`.
+3. `a * f a  + c * f d ≤ f (a * b + c * d)` `superlinear`, (derived from 1. and 2.).
+
+So we can establish on the one hand that `f 1980 ≤ 660`,
+by observing that `660 * 1 = 660 * f3 ≤ f 1980 = f (660 * 3)`.
+
+On the other hand, we establish that `f 1980 ≥ 660`
+from `5 * f 1980 + 33 * f 3 ≤ f (5 * 1980 + 33 * 1) = f 9999 = 3333`.
+
+We then conclude `f 1980 = 660` and then eventually determine that either
+`f 1982 = 660` or `f 1982 = 661`.
+
+In the latter case we derive a contradiction, because if `f 1982 = 661` then
+`3334 = 5 * f 1982 + 29 * f(3) + f(2) ≤ f (5 * 1982 + 29 * 3 + 2) = f 9999 = 3333`.
+-/
+
+namespace Imo1982Q1
+
+structure IsGood (f : ℕ+ → ℕ) : Prop where
+  /-- The function satisfies the functional relation-/
+  rel: ∀ m n : ℕ+, f (m + n) = f m + f n ∨ f (m + n) = f m + f n + 1
+  f₂ : f 2 = 0
+  hf₃ : 0 < f 3
+  f_9999 : f 9999 = 3333
+
+namespace IsGood
+
+variable {f : ℕ+ → ℕ} (hf : IsGood f)
+include hf
+
+lemma f₁ : f 1 = 0 := by
+  have h : f 2 = 2 * f 1 ∨ f 2 = 2 * f 1 + 1 := by rw [two_mul]; exact hf.rel 1 1
+  obtain h₁ | h₂ := hf.f₂ ▸ h
+  · rw [eq_comm, mul_eq_zero] at h₁
+    apply h₁.resolve_left
+    norm_num
+  · cases Nat.succ_ne_zero _ h₂.symm
+
+lemma f₃ : f 3 = 1 := by
+    have h : f 3 = f 2 + f 1 ∨ f 3  = f 2 + f 1 + 1 := by apply hf.rel 2 1
+    rw [hf.f₁, hf.f₂, add_zero, zero_add] at h
+    have not_left : ¬ f 3 = 0 := by apply ne_of_gt hf.hf₃
+    rw [or_iff_right (not_left)] at h
+    exact h
+
+lemma superadditive {m n : ℕ+} : f m + f n ≤ f (m + n) := by
+  have h := hf.rel m n
+  rcases h with ( hl | hr )
+  · rw [hl]
+  · rw [hr]; nth_rewrite 1 [← add_zero (f n), ← add_assoc]; apply add_le_add_right (by norm_num)
+
+lemma superhomogeneous {m n : ℕ+} : ↑n * f m ≤ f (n * m) := by
+  induction n using PNat.recOn
+  case p1 => simp
+  case hp n' ih =>
+    calc
+    ↑(n' + 1) * f m = ↑n' * f m + f m := by rw [PNat.add_coe, add_mul, PNat.val_ofNat, one_mul]
+    _ ≤ f (n' * m) + f m := add_le_add_right ih (f m)
+    _ ≤ f (n' * m + m) := hf.superadditive
+    _ = f ((n' + 1) * m) := by congr; rw [add_mul, one_mul]
+
+lemma superlinear {a b c d : ℕ+} : a * f b + c * f d ≤ f (a * b + c * d) :=
+  (add_le_add hf.superhomogeneous hf.superhomogeneous).trans hf.superadditive
+
+lemma le_mul_three_apply (n : ℕ+) : n ≤ f (3 * n) := by
+  rw [← mul_one (n : ℕ), ← hf.f₃, mul_comm 3]
+  exact hf.superhomogeneous
+
+lemma part_1 : 660 ≤ f (1980) := by
+  exact hf.le_mul_three_apply 660
+
+lemma part_2 : f 1980 ≤ 660 := by
+  have h : 5 * f 1980 + 33 * f 3 ≤ 5 * 660 + 33 := by
+    calc (5 : ℕ+) * f 1980 + (33 : ℕ+) * f 3 ≤  f (5 * 1980 + 33 * 3) := by apply hf.superlinear
+    _ = f 9999 := by rfl
+    _ = 5 * 660 + 33 := by rw [hf.f_9999]
+  rw [hf.f₃, mul_one] at h
+  -- from 5 * f 1980 + 33 ≤ 5 * 660 + 33 we show f 1980 ≤ 660
+  linarith
+
+end IsGood
+
+end Imo1982Q1
+
+open Imo1982Q1
+
+lemma imo1982_q1 {f : ℕ+ → ℕ} (hf : IsGood f) : f 1982 = 660 := by
+  have f_1980 := hf.part_2.antisymm hf.part_1
+  have h : f 1982 = f 1980 + f 2 ∨ f 1982 = f 1980 + f 2 + 1 := hf.rel 1980 2
+  rw [f_1980, hf.f₂, add_zero] at h
+  apply h.resolve_right
+  intro hr
+  suffices h : 3334 ≤ 3333 by norm_num at h
+  calc
+    3334 = 5 * f 1982 + 29 * f 3 + f 2 := by rw [hf.f₃, hf.f₂, hr, add_zero, mul_one]
+    (5 : ℕ+) * f 1982 + (29 : ℕ+) * f 3 + f 2 ≤ f (5 * 1982 + 29 * 3) + f 2 :=
+      add_le_add_right hf.superlinear _
+    _ ≤ f (5 * 1982 + 29 * 3 + 2) := hf.superadditive
+    _ = 3333 := hf.f_9999

Archive/Imo/Imo2019Q4.lean

@@ -5,7 +5,7 @@ Authors: Floris van Doorn
 -/
 import Mathlib.Data.Nat.Factorial.BigOperators
 import Mathlib.Data.Nat.Multiplicity
-import Mathlib.Data.Nat.Prime.Basic
+import Mathlib.Data.Nat.Prime.Int
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.GCongr
 

Archive/Wiedijk100Theorems/BirthdayProblem.lean

@@ -76,12 +76,9 @@ theorem birthday_measure :
     · rw [Fintype.card_embedding_eq, Fintype.card_fin, Fintype.card_fin]
       rfl
   rw [this, ENNReal.lt_div_iff_mul_lt, mul_comm, mul_div, ENNReal.div_lt_iff]
-  rotate_left
-  iterate 2 right; norm_num
-  · decide
-  iterate 2 left; norm_num
-  simp only [Fintype.card_pi]
-  norm_num
+  all_goals
+    simp only [Fintype.card_pi, Fintype.card_fin, Finset.prod_const, Finset.card_univ]
+    norm_num
 
 end MeasureTheory
 

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Enrico Z. Borba
 -/
 
-import Mathlib.Probability.Density
-import Mathlib.Probability.Notation
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import Mathlib.Analysis.SpecialFunctions.Integrals
+import Mathlib.MeasureTheory.Integral.Prod
+import Mathlib.Probability.Density
 import Mathlib.Probability.Distributions.Uniform
+import Mathlib.Probability.Notation
 
 /-!
 

Archive/Wiedijk100Theorems/InverseTriangleSum.lean

@@ -27,8 +27,8 @@ open Finset
 /-- **Sum of the Reciprocals of the Triangular Numbers** -/
 theorem Theorems100.inverse_triangle_sum :
     ∀ n, ∑ k ∈ range n, (2 : ℚ) / (k * (k + 1)) = if n = 0 then 0 else 2 - (2 : ℚ) / n := by
-  refine sum_range_induction _ _ (if_pos rfl) ?_
-  rintro (_ | n)
-  · rw [if_neg, if_pos] <;> norm_num
+  refine sum_range_induction _ _ rfl ?_
+  rintro (_ | _)
+  · norm_num
   field_simp
   ring

Archive/Wiedijk100Theorems/PerfectNumbers.lean

@@ -17,10 +17,10 @@ This file proves Theorem 70 from the [100 Theorems List](https://www.cs.ru.nl/~f
 The theorem characterizes even perfect numbers.
 
 Euclid proved that if `2 ^ (k + 1) - 1` is prime (these primes are known as Mersenne primes),
-  then `2 ^ k * 2 ^ (k + 1) - 1` is perfect.
+  then `2 ^ k * (2 ^ (k + 1) - 1)` is perfect.
 
 Euler proved the converse, that if `n` is even and perfect, then there exists `k` such that
-  `n = 2 ^ k * 2 ^ (k + 1) - 1` and `2 ^ (k + 1) - 1` is prime.
+  `n = 2 ^ k * (2 ^ (k + 1) - 1)` and `2 ^ (k + 1) - 1` is prime.
 
 ## References
 https://en.wikipedia.org/wiki/Euclid%E2%80%93Euler_theorem

Archive/Wiedijk100Theorems/SolutionOfCubic.lean → Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.lean

@@ -1,32 +1,40 @@
 /-
 Copyright (c) 2022 Jeoff Lee. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeoff Lee
+Authors: Jeoff Lee, Thomas Zhu
 -/
 import Mathlib.Tactic.LinearCombination
 import Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
 
 /-!
-# The Solution of a Cubic
+# The roots of cubic polynomials
 
 This file proves Theorem 37 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/).
 
-In this file, we give the solutions to the cubic equation `a * x^3 + b * x^2 + c * x + d = 0`
-over a field `K` that has characteristic neither 2 nor 3, that has a third primitive root of
-unity, and in which certain other quantities admit square and cube roots.
-
-This is based on the [Cardano's Formula](https://en.wikipedia.org/wiki/Cubic_equation#Cardano's_formula).
+We give the solutions to the cubic equation `a * x^3 + b * x^2 + c * x + d = 0` over a field `K`
+that has characteristic neither 2 nor 3, that has a third primitive root of
+unity, and in which certain other quantities admit square and cube roots. This is based on the
+[Cardano's Formula](https://en.wikipedia.org/wiki/Cubic_equation#Cardano's_formula).
 
 ## Main statements
 
-- `cubic_eq_zero_iff` : gives the roots of the cubic equation
+- `cubic_eq_zero_iff`: gives the roots of the cubic equation
 where the discriminant `p = 3 * a * c - b^2` is nonzero.
-- `cubic_eq_zero_iff_of_p_eq_zero` : gives the roots of the cubic equation
+- `cubic_eq_zero_iff_of_p_eq_zero`: gives the roots of the cubic equation
 where the discriminant equals zero.
 
+## Proof outline
+
+1.  Given cubic $ax^3 + bx^2 + cx + d = 0$, we show it is equivalent to some "depressed cubic"
+    $y^3 + 3py - 2q = 0$ where $y = x + b / (3a)$, $p = (3ac - b^2) / (9a^2)$, and
+    $q = (9abc - 2b^3 - 27a^2d) / (54a^3)$ (`h₁` in `cubic_eq_zero_iff`).
+2.  When $p$ is zero, this is easily solved (`cubic_eq_zero_iff_of_p_eq_zero`).
+3.  Otherwise one can directly derive a factorization of the depressed cubic, in terms of some
+    primitive cube root of unity $\omega^3 = 1$ (`cubic_depressed_eq_zero_iff`).
+
 ## References
 
-Originally ported from Isabelle/HOL. The
+The cubic formula was originally ported from Isabelle/HOL. The
 [original file](https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Cubic_Quartic.html) was written by Amine Chaieb.
 
 ## Tags
@@ -41,13 +49,15 @@ section Field
 
 open Polynomial
 
-variable {K : Type*} [Field K] (a b c d : K) {ω p q r s t : K}
+variable {K : Type*} [Field K] (a b c d e : K) {ω p q r s t u v w x y : K}
+
+section Cubic
 
 theorem cube_root_of_unity_sum (hω : IsPrimitiveRoot ω 3) : 1 + ω + ω ^ 2 = 0 := by
   simpa [cyclotomic_prime, Finset.sum_range_succ] using hω.isRoot_cyclotomic (by decide)
 
-/-- The roots of a monic cubic whose quadratic term is zero and whose discriminant is nonzero. -/
-theorem cubic_basic_eq_zero_iff (hω : IsPrimitiveRoot ω 3) (hp_nonzero : p ≠ 0)
+/-- The roots of a monic cubic whose quadratic term is zero and whose linear term is nonzero. -/
+theorem cubic_depressed_eq_zero_iff (hω : IsPrimitiveRoot ω 3) (hp_nonzero : p ≠ 0)
     (hr : r ^ 2 = q ^ 2 + p ^ 3) (hs3 : s ^ 3 = q + r) (ht : t * s = p) (x : K) :
     x ^ 3 + 3 * p * x - 2 * q = 0 ↔ x = s - t ∨ x = s * ω - t * ω ^ 2 ∨ x = s * ω ^ 2 - t * ω := by
   have h₁ : ∀ x a₁ a₂ a₃ : K, x = a₁ ∨ x = a₂ ∨ x = a₃ ↔ (x - a₁) * (x - a₂) * (x - a₃) = 0 := by
@@ -66,23 +76,6 @@ theorem cubic_basic_eq_zero_iff (hω : IsPrimitiveRoot ω 3) (hp_nonzero : p ≠
 
 variable [Invertible (2 : K)] [Invertible (3 : K)]
 
-/-- Roots of a monic cubic whose discriminant is nonzero. -/
-theorem cubic_monic_eq_zero_iff (hω : IsPrimitiveRoot ω 3) (hp : p = (3 * c - b ^ 2) / 9)
-    (hp_nonzero : p ≠ 0) (hq : q = (9 * b * c - 2 * b ^ 3 - 27 * d) / 54)
-    (hr : r ^ 2 = q ^ 2 + p ^ 3) (hs3 : s ^ 3 = q + r) (ht : t * s = p) (x : K) :
-    x ^ 3 + b * x ^ 2 + c * x + d = 0 ↔
-      x = s - t - b / 3 ∨ x = s * ω - t * ω ^ 2 - b / 3 ∨ x = s * ω ^ 2 - t * ω - b / 3 := by
-  let y := x + b / 3
-  have hi2 : (2 : K) ≠ 0 := Invertible.ne_zero _
-  have hi3 : (3 : K) ≠ 0 := Invertible.ne_zero _
-  have h9 : (9 : K) = 3 ^ 2 := by norm_num
-  have h54 : (54 : K) = 2 * 3 ^ 3 := by norm_num
-  have h₁ : x ^ 3 + b * x ^ 2 + c * x + d = y ^ 3 + 3 * p * y - 2 * q := by
-    rw [hp, hq]
-    field_simp [y, h9, h54]; ring
-  rw [h₁, cubic_basic_eq_zero_iff hω hp_nonzero hr hs3 ht y]
-  simp_rw [eq_sub_iff_add_eq]
-
 /-- **The Solution of Cubic**.
   The roots of a cubic polynomial whose discriminant is nonzero. -/
 theorem cubic_eq_zero_iff (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3)
@@ -92,25 +85,17 @@ theorem cubic_eq_zero_iff (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3)
     a * x ^ 3 + b * x ^ 2 + c * x + d = 0 ↔
       x = s - t - b / (3 * a) ∨
         x = s * ω - t * ω ^ 2 - b / (3 * a) ∨ x = s * ω ^ 2 - t * ω - b / (3 * a) := by
-  have hi3 : (3 : K) ≠ 0 := Invertible.ne_zero _
+  let y := x + b / (3 * a)
   have h9 : (9 : K) = 3 ^ 2 := by norm_num
   have h54 : (54 : K) = 2 * 3 ^ 3 := by norm_num
-  have h₁ : a * x ^ 3 + b * x ^ 2 + c * x + d
-    = a * (x ^ 3 + b / a * x ^ 2 + c / a * x + d / a) := by field_simp; ring
+  have h₁ : a * x ^ 3 + b * x ^ 2 + c * x + d = a * (y ^ 3 + 3 * p * y - 2 * q) := by
+    rw [hp, hq]
+    simp [field_simps, y, ha, h9, h54]; ring
   have h₂ : ∀ x, a * x = 0 ↔ x = 0 := by intro x; simp [ha]
-  have hp' : p = (3 * (c / a) - (b / a) ^ 2) / 9 := by field_simp [hp, h9]; ring_nf
-  have hq' : q = (9 * (b / a) * (c / a) - 2 * (b / a) ^ 3 - 27 * (d / a)) / 54 := by
-    rw [hq, h54]
-    simp [field_simps, ha]
-    ring_nf
-  rw [h₁, h₂, cubic_monic_eq_zero_iff (b / a) (c / a) (d / a) hω hp' hp_nonzero hq' hr hs3 ht x]
-  have h₄ :=
-    calc
-      b / a / 3 = b / (a * 3) := by field_simp [ha]
-      _ = b / (3 * a) := by rw [mul_comm]
-  rw [h₄]
+  rw [h₁, h₂, cubic_depressed_eq_zero_iff hω hp_nonzero hr hs3 ht]
+  simp_rw [eq_sub_iff_add_eq]
 
-/-- the solution of the cubic equation when p equals zero. -/
+/-- The solution of the cubic equation when p equals zero. -/
 theorem cubic_eq_zero_iff_of_p_eq_zero (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3)
     (hpz : 3 * a * c - b ^ 2 = 0)
     (hq : q = (9 * a * b * c - 2 * b ^ 3 - 27 * a ^ 2 * d) / (54 * a ^ 3)) (hs3 : s ^ 3 = 2 * q)
@@ -144,6 +129,8 @@ theorem cubic_eq_zero_iff_of_p_eq_zero (ha : a ≠ 0) (hω : IsPrimitiveRoot ω
   rw [h₁, h₂, h₃, h₄ (x + b / (3 * a))]
   ring_nf
 
+end Cubic
+
 end Field
 
 end Theorems100

Counterexamples/CharPZeroNeCharZero.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa, Eric Wieser
 -/
-import Mathlib.Algebra.CharP.Basic
+import Mathlib.Algebra.CharP.Lemmas
 import Mathlib.Algebra.PUnitInstances.Algebra
 
 /-! # `CharP R 0` and `CharZero R` need not coincide for semirings

Counterexamples/Phillips.lean

@@ -385,7 +385,7 @@ section
 
 
 theorem norm_indicator_le_one (s : Set α) (x : α) : ‖(indicator s (1 : α → ℝ)) x‖ ≤ 1 := by
-  simp only [indicator, Pi.one_apply]; split_ifs <;> norm_num
+  simp only [Set.indicator, Pi.one_apply]; split_ifs <;> norm_num
 
 /-- A functional in the dual space of bounded functions gives rise to a bounded additive measure,
 by applying the functional to the indicator functions. -/