Skip to content

Commit

Permalink
Merge branch 'master' into MR-import-header-linter
Browse files Browse the repository at this point in the history
  • Loading branch information
grunweg committed Oct 31, 2024
2 parents 133955c + 348232e commit 737eda7
Show file tree
Hide file tree
Showing 929 changed files with 22,293 additions and 8,900 deletions.
3 changes: 2 additions & 1 deletion Archive.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
126 changes: 126 additions & 0 deletions Archive/Imo/Imo1982Q1.lean
Original file line number Diff line number Diff line change
@@ -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 1980660 := by
have h : 5 * f 1980 + 33 * f 35 * 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 : 33343333 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
2 changes: 1 addition & 1 deletion Archive/Imo/Imo2019Q4.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
9 changes: 3 additions & 6 deletions Archive/Wiedijk100Theorems/BirthdayProblem.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
6 changes: 3 additions & 3 deletions Archive/Wiedijk100Theorems/BuffonsNeedle.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

/-!
Expand Down
4 changes: 2 additions & 2 deletions Archive/Wiedijk100Theorems/PerfectNumbers.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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
Expand All @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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
2 changes: 1 addition & 1 deletion Counterexamples/Phillips.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/
Expand Down
8 changes: 3 additions & 5 deletions LongestPole/Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -122,9 +122,8 @@ open System in
def countLOC (modules : List Name) : IO (NameMap Float) := do
let mut r := {}
for m in modules do
let fp := FilePath.mk ((← findOLean m).toString.replace ".lake/build/lib/" "")
|>.withExtension "lean"
if ← fp.pathExists then
if let .some fp ← Lean.SearchPath.findModuleWithExt [s!".{FilePath.pathSeparator}"] "lean" m
then
let src ← IO.FS.readFile fp
r := r.insert m (src.toList.count '\n').toFloat
return r
Expand Down Expand Up @@ -154,8 +153,7 @@ def longestPoleCLI (args : Cli.Parsed) : IO UInt32 := do
let c := cumulative.find! n'
let t := total.find! n'
let r := (t / c).toStringDecimals 2
table := table.push
#[n.get!.toString, toString (i |>.toUInt64), toString (c |>.toUInt64), r]
table := table.push #[n.get!.toString, toString i.toUInt64, toString c.toUInt64, r]
n := slowest.find? n'
let instructionsHeader := if args.hasFlag "loc" then "LoC" else "instructions"
IO.println (formatTable
Expand Down
Loading

0 comments on commit 737eda7

Please sign in to comment.