Merge branch 'master' into YK-cont-alternating

leanprover-community · Nov 28, 2023 · 2851eea · 2851eea
2 parents 991d1b5 + 65a1391
commit 2851eea
Show file tree

Hide file tree

Showing 329 changed files with 7,430 additions and 1,566 deletions.
diff --git a/OLD_README.md b/OLD_README.md
@@ -0,0 +1,115 @@
+# Lean 3's mathlib
+
+> [!WARNING]  
+> Lean 3 and Mathlib 3 are no longer actively maintained.
+> It is strongly recommended that you use [mathlib4](https://github.com/leanprover-community/mathlib4) for Lean 4 instead.
+
+![](https://github.com/leanprover-community/mathlib/workflows/continuous%20integration/badge.svg?branch=master)
+[![Bors enabled](https://bors.tech/images/badge_small.svg)](https://app.bors.tech/repositories/24316)
+[![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://leanprover.zulipchat.com)
+[![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/leanprover-community/mathlib)
+
+[Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean 3 theorem prover](https://github.com/leanprover-community/lean).
+It contains both programming infrastructure and mathematics,
+as well as tactics that use the former and allow to develop the latter.
+
+## Installation
+
+You can find detailed instructions to install Lean 3, mathlib 3, and supporting tools on [our website](https://leanprover-community.github.io/lean3/get_started.html).
+
+## Experimenting
+
+Got everything installed? Why not start with the [tutorial project](https://leanprover-community.github.io/lean3/install/project.html)?
+
+For more pointers, see [Learning Lean](https://leanprover-community.github.io/lean3/learn.html).
+
+## Documentation
+
+Besides the installation guides above and [Lean's general
+documentation](https://leanprover.github.io/lean3/documentation/), the documentation
+of mathlib consists of:
+
+- [The mathlib docs](https://leanprover-community.github.io/mathlib_docs): documentation [generated
+  automatically](https://github.com/leanprover-community/doc-gen) from the source `.lean` files.
+  In addition to the pages generated for each file in the library, the docs also include pages on:
+  - [tactics](https://leanprover-community.github.io/mathlib_docs/tactics.html),
+  - [commands](https://leanprover-community.github.io/mathlib_docs/commands.html),
+  - [hole commands](https://leanprover-community.github.io/mathlib_docs/hole_commands.html), and
+  - [attributes](https://leanprover-community.github.io/mathlib_docs/attributes.html).
+- A description of [currently covered theories](https://leanprover-community.github.io/theories.html),
+  as well as an [overview](https://leanprover-community.github.io/lean3/mathlib-overview.html) for mathematicians.
+- A couple of [tutorial Lean files](docs/tutorial/)
+- Some [extra Lean documentation](https://leanprover-community.github.io/lean3/learn.html) not specific to mathlib (see "Miscellaneous topics")
+- Documentation for people who would like to [contribute to mathlib3](https://leanprover-community.github.io/lean3/contribute/index.html)
+
+Much of the discussion surrounding mathlib occurs in a
+[Zulip chat room](https://leanprover.zulipchat.com/). Since this
+chatroom is only visible to registered users, we provide an
+[openly accessible archive](https://leanprover-community.github.io/archive/)
+of the public discussions. This is useful for quick reference; for a
+better browsing interface, and to participate in the discussions, we strongly
+suggest joining the chat. Questions from users at all levels of expertise are
+welcomed.
+
+## Contributing
+
+> [!WARNING]  
+> Contributions are no longer accepted to mathlib 3; contribute to mathlib 4 instead!
+
+The complete documentation for contributing to ``mathlib`` is located
+[on the community guide contribute to mathlib](https://leanprover-community.github.io/lean3/contribute/index.html)
+
+The process is different from other projects where one should not fork the repository.
+Instead write permission for non-master branches should be requested on [Zulip](https://leanprover.zulipchat.com)
+by introducing yourself, providing your GitHub handle and what contribution you are planning on doing.
+
+### Guidelines
+
+Mathlib has the following guidelines and conventions that must be followed
+
+ - The [style guide](https://leanprover-community.github.io/lean3/contribute/style.html)
+ - A guide on the [naming convention](https://leanprover-community.github.io/lean3/contribute/naming.html)
+ - The [documentation style](https://leanprover-community.github.io/lean3/contribute/doc.html)
+ - The [commit naming conventions](https://github.com/leanprover-community/lean/blob/master/doc/commit_convention.md)
+
+Note: the title of a PR should follow the commit naming convention.
+
+### Using ``leanproject`` to contribute
+
+Running the ``leanproject get -b mathlib:shiny_lemma`` command will create a new worktree ``mathlib_shiny_lemma``
+with a local branch called ``shiny_lemma`` which has a copy of mathlib to work on.
+
+``leanproject build`` will check that nothing broke.
+Be warned that this will take some time if a fundamental file was changed.
+
+## Maintainers:
+
+* Anne Baanen (@Vierkantor): algebra, number theory, tactics
+* Reid Barton (@rwbarton): category theory, topology
+* Riccardo Brasca (@riccardobrasca): algebra, number theory, algebraic geometry, category theory
+* Mario Carneiro (@digama0): lean formalization, tactics, type theory, proof engineering
+* Bryan Gin-ge Chen (@bryangingechen): documentation, infrastructure
+* Johan Commelin (@jcommelin): algebra, number theory, category theory, algebraic geometry
+* Rémy Degenne (@RemyDegenne): probability, measure theory, analysis
+* Floris van Doorn (@fpvandoorn): measure theory, model theory, tactics
+* Frédéric Dupuis (@dupuisf): linear algebra, functional analysis
+* Gabriel Ebner (@gebner): tactics, infrastructure, core, formal languages
+* Sébastien Gouëzel (@sgouezel): topology, calculus, geometry, analysis, measure theory
+* Markus Himmel (@TwoFX): category theory
+* Chris Hughes (@ChrisHughes24): algebra
+* Yury G. Kudryashov (@urkud): analysis, topology, measure theory
+* Robert Y. Lewis (@robertylewis): tactics, documentation
+* Heather Macbeth (@hrmacbeth): geometry, analysis
+* Patrick Massot (@patrickmassot): documentation, topology, geometry
+* Bhavik Mehta (@b-mehta): category theory, combinatorics
+* Kyle Miller (@kmill): combinatorics, documentation
+* Scott Morrison (@semorrison): category theory, tactics
+* Oliver Nash (@ocfnash): algebra, geometry, topology
+* Adam Topaz (@adamtopaz): algebra, category theory, algebraic geometry
+* Eric Wieser (@eric-wieser): algebra, infrastructure
+
+## Emeritus maintainers:
+
+* Jeremy Avigad (@avigad): analysis
+* Johannes Hölzl (@johoelzl): measure theory, topology
+* Simon Hudon (@cipher1024): tactics
diff --git a/README.md b/README.md
@@ -1,108 +1,7 @@
-# Lean mathlib
+# Lean 3's mathlib
 
-![](https://github.com/leanprover-community/mathlib/workflows/continuous%20integration/badge.svg?branch=master)
-[![Bors enabled](https://bors.tech/images/badge_small.svg)](https://app.bors.tech/repositories/24316)
-[![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://leanprover.zulipchat.com)
-[![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/leanprover-community/mathlib)
+> [!WARNING]  
+> Lean 3 and Mathlib 3 are no longer actively maintained.
+> It is strongly recommended that you use [mathlib4](https://github.com/leanprover-community/mathlib4) for Lean 4 instead.
 
-[Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean theorem prover](https://leanprover.github.io).
-It contains both programming infrastructure and mathematics,
-as well as tactics that use the former and allow to develop the latter.
-
-## Installation
-
-You can find detailed instructions to install Lean, mathlib, and supporting tools on [our website](https://leanprover-community.github.io/get_started.html).
-
-## Experimenting
-
-Got everything installed? Why not start with the [tutorial project](https://leanprover-community.github.io/install/project.html)?
-
-For more pointers, see [Learning Lean](https://leanprover-community.github.io/learn.html).
-
-## Documentation
-
-Besides the installation guides above and [Lean's general
-documentation](https://leanprover.github.io/documentation/), the documentation
-of mathlib consists of:
-
-- [The mathlib docs](https://leanprover-community.github.io/mathlib_docs): documentation [generated
-  automatically](https://github.com/leanprover-community/doc-gen) from the source `.lean` files.
-  In addition to the pages generated for each file in the library, the docs also include pages on:
-  - [tactics](https://leanprover-community.github.io/mathlib_docs/tactics.html),
-  - [commands](https://leanprover-community.github.io/mathlib_docs/commands.html),
-  - [hole commands](https://leanprover-community.github.io/mathlib_docs/hole_commands.html), and
-  - [attributes](https://leanprover-community.github.io/mathlib_docs/attributes.html).
-- A description of [currently covered theories](https://leanprover-community.github.io/theories.html),
-  as well as an [overview](https://leanprover-community.github.io/mathlib-overview.html) for mathematicians.
-- A couple of [tutorial Lean files](docs/tutorial/)
-- Some [extra Lean documentation](https://leanprover-community.github.io/learn.html) not specific to mathlib (see "Miscellaneous topics")
-- Documentation for people who would like to [contribute to mathlib](https://leanprover-community.github.io/contribute/index.html)
-
-Much of the discussion surrounding mathlib occurs in a
-[Zulip chat room](https://leanprover.zulipchat.com/). Since this
-chatroom is only visible to registered users, we provide an
-[openly accessible archive](https://leanprover-community.github.io/archive/)
-of the public discussions. This is useful for quick reference; for a
-better browsing interface, and to participate in the discussions, we strongly
-suggest joining the chat. Questions from users at all levels of expertise are
-welcomed.
-
-## Contributing
-
-The complete documentation for contributing to ``mathlib`` is located
-[on the community guide contribute to mathlib](https://leanprover-community.github.io/contribute/index.html)
-
-The process is different from other projects where one should not fork the repository.
-Instead write permission for non-master branches should be requested on [Zulip](https://leanprover.zulipchat.com)
-by introducing yourself, providing your GitHub handle and what contribution you are planning on doing.
-
-### Guidelines
-
-Mathlib has the following guidelines and conventions that must be followed
-
- - The [style guide](https://leanprover-community.github.io/contribute/style.html)
- - A guide on the [naming convention](https://leanprover-community.github.io/contribute/naming.html)
- - The [documentation style](https://leanprover-community.github.io/contribute/doc.html)
- - The [commit naming conventions](https://github.com/leanprover-community/lean/blob/master/doc/commit_convention.md)
-
-Note: the title of a PR should follow the commit naming convention.
-
-### Using ``leanproject`` to contribute
-
-Running the ``leanproject get -b mathlib:shiny_lemma`` command will create a new worktree ``mathlib_shiny_lemma``
-with a local branch called ``shiny_lemma`` which has a copy of mathlib to work on.
-
-``leanproject build`` will check that nothing broke.
-Be warned that this will take some time if a fundamental file was changed.
-
-## Maintainers:
-
-* Anne Baanen (@Vierkantor): algebra, number theory, tactics
-* Reid Barton (@rwbarton): category theory, topology
-* Riccardo Brasca (@riccardobrasca): algebra, number theory, algebraic geometry, category theory
-* Mario Carneiro (@digama0): lean formalization, tactics, type theory, proof engineering
-* Bryan Gin-ge Chen (@bryangingechen): documentation, infrastructure
-* Johan Commelin (@jcommelin): algebra, number theory, category theory, algebraic geometry
-* Rémy Degenne (@RemyDegenne): probability, measure theory, analysis
-* Floris van Doorn (@fpvandoorn): measure theory, model theory, tactics
-* Frédéric Dupuis (@dupuisf): linear algebra, functional analysis
-* Gabriel Ebner (@gebner): tactics, infrastructure, core, formal languages
-* Sébastien Gouëzel (@sgouezel): topology, calculus, geometry, analysis, measure theory
-* Markus Himmel (@TwoFX): category theory
-* Chris Hughes (@ChrisHughes24): algebra
-* Yury G. Kudryashov (@urkud): analysis, topology, measure theory
-* Robert Y. Lewis (@robertylewis): tactics, documentation
-* Heather Macbeth (@hrmacbeth): geometry, analysis
-* Patrick Massot (@patrickmassot): documentation, topology, geometry
-* Bhavik Mehta (@b-mehta): category theory, combinatorics
-* Kyle Miller (@kmill): combinatorics, documentation
-* Scott Morrison (@semorrison): category theory, tactics
-* Oliver Nash (@ocfnash): algebra, geometry, topology
-* Adam Topaz (@adamtopaz): algebra, category theory, algebraic geometry
-* Eric Wieser (@eric-wieser): algebra, infrastructure
-
-## Emeritus maintainers:
-
-* Jeremy Avigad (@avigad): analysis
-* Johannes Hölzl (@johoelzl): measure theory, topology
-* Simon Hudon (@cipher1024): tactics
+(If you need to read the old `README.md`, please see `OLD_README.md`.)
diff --git a/archive/arithcc.lean b/archive/arithcc.lean
@@ -9,6 +9,9 @@ import tactic.basic
 /-!
 # A compiler for arithmetic expressions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A formalization of the correctness of a compiler from arithmetic expressions to machine language
 described by McCarthy and Painter, which is considered the first proof of compiler correctness.
 

diff --git a/archive/examples/mersenne_primes.lean b/archive/examples/mersenne_primes.lean
@@ -8,6 +8,9 @@ import number_theory.lucas_lehmer
 /-!
 # Explicit Mersenne primes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We run some Lucas-Lehmer tests to prove some Mersenne primes are prime.
 
 See the discussion at the end of [src/number_theory/lucas_lehmer.lean]

diff --git a/archive/examples/prop_encodable.lean b/archive/examples/prop_encodable.lean
@@ -9,6 +9,9 @@ import data.W.basic
 /-!
 # W types
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The file `data/W.lean` shows that if `α` is an an encodable fintype and for every `a : α`,
 `β a` is encodable, then `W β` is encodable.
 

diff --git a/archive/imo/imo1959_q1.lean b/archive/imo/imo1959_q1.lean
@@ -10,6 +10,9 @@ import data.nat.prime
 /-!
 # IMO 1959 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Prove that the fraction `(21n+4)/(14n+3)` is irreducible for every natural number `n`.
 
 Since Lean doesn't have a concept of "irreducible fractions" per se, we just formalize this

diff --git a/archive/imo/imo1960_q1.lean b/archive/imo/imo1960_q1.lean
@@ -9,6 +9,9 @@ import data.nat.digits
 /-!
 # IMO 1960 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Determine all three-digit numbers $N$ having the property that $N$ is divisible by 11, and
 $\dfrac{N}{11}$ is equal to the sum of the squares of the digits of $N$.
 

diff --git a/archive/imo/imo1962_q1.lean b/archive/imo/imo1962_q1.lean
@@ -9,6 +9,9 @@ import data.nat.digits
 /-!
 # IMO 1962 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Find the smallest natural number $n$ which has the following properties:
 
 (a) Its decimal representation has 6 as the last digit.

diff --git a/archive/imo/imo1962_q4.lean b/archive/imo/imo1962_q4.lean
@@ -9,6 +9,9 @@ import analysis.special_functions.trigonometric.complex
 /-!
 # IMO 1962 Q4
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Solve the equation `cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 = 1`.
 
 Since Lean does not have a concept of "simplest form", we just express what is

diff --git a/archive/imo/imo1964_q1.lean b/archive/imo/imo1964_q1.lean
@@ -10,6 +10,9 @@ import data.nat.modeq
 /-!
 # IMO 1964 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 (a) Find all positive integers $n$ for which $2^n-1$ is divisible by $7$.
 
 (b) Prove that there is no positive integer $n$ for which $2^n+1$ is divisible by $7$.

diff --git a/archive/imo/imo1969_q1.lean b/archive/imo/imo1969_q1.lean
@@ -11,6 +11,9 @@ import data.set.finite
 /-!
 # IMO 1969 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Prove that there are infinitely many natural numbers $a$ with the following property:
 the number $z = n^4 + a$ is not prime for any natural number $n$.
 -/

diff --git a/archive/imo/imo1972_q5.lean b/archive/imo/imo1972_q5.lean
@@ -10,6 +10,9 @@ import analysis.normed_space.basic
 /-!
 # IMO 1972 Q5
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Problem: `f` and `g` are real-valued functions defined on the real line. For all `x` and `y`,
 `f(x + y) + f(x - y) = 2f(x)g(y)`. `f` is not identically zero and `|f(x)| ≤ 1` for all `x`.
 Prove that `|g(x)| ≤ 1` for all `x`.

diff --git a/archive/imo/imo1975_q1.lean b/archive/imo/imo1975_q1.lean
@@ -11,6 +11,9 @@ import algebra.big_operators.ring
 /-!
 # IMO 1975 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `x₁, x₂, ... , xₙ` and `y₁, y₂, ... , yₙ` be two sequences of real numbers, such that
 `x₁ ≥ x₂ ≥ ... ≥ xₙ` and `y₁ ≥ y₂ ≥ ... ≥ yₙ`. Prove that if `z₁, z₂, ... , zₙ` is any permutation
 of `y₁, y₂, ... , yₙ`, then `∑ (xᵢ - yᵢ)^2 ≤ ∑ (xᵢ - zᵢ)^2`

diff --git a/archive/imo/imo1977_q6.lean b/archive/imo/imo1977_q6.lean
@@ -8,6 +8,9 @@ import data.pnat.basic
 /-!
 # IMO 1977 Q6
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Suppose `f : ℕ+ → ℕ+` satisfies `f(f(n)) < f(n + 1)` for all `n`.
 Prove that `f(n) = n` for all `n`.
 

diff --git a/archive/imo/imo1981_q3.lean b/archive/imo/imo1981_q3.lean
@@ -10,6 +10,9 @@ import tactic.linarith
 /-!
 # IMO 1981 Q3
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Determine the maximum value of `m ^ 2 + n ^ 2`, where `m` and `n` are integers in
 `{1, 2, ..., 1981}` and `(n ^ 2 - m * n - m ^ 2) ^ 2 = 1`.
 

diff --git a/archive/imo/imo1987_q1.lean b/archive/imo/imo1987_q1.lean
@@ -11,6 +11,9 @@ import dynamics.fixed_points.basic
 /-!
 # Formalization of IMO 1987, Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let $p_{n, k}$ be the number of permutations of a set of cardinality `n ≥ 1` that fix exactly `k`
 elements. Prove that $∑_{k=0}^n k p_{n,k}=n!$.
 

diff --git a/archive/imo/imo1988_q6.lean b/archive/imo/imo1988_q6.lean
@@ -13,6 +13,9 @@ import tactic.wlog
 /-!
 # IMO 1988 Q6 and constant descent Vieta jumping
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Question 6 of IMO1988 is somewhat (in)famous. Several expert problem solvers
 could not tackle the question within the given time limit.
 The problem lead to the introduction of a new proof technique,

diff --git a/archive/imo/imo1994_q1.lean b/archive/imo/imo1994_q1.lean
@@ -14,6 +14,9 @@ import tactic.by_contra
 /-!
 # IMO 1994 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `m` and `n` be two positive integers.
 Let `a₁, a₂, ..., aₘ` be `m` different numbers from the set `{1, 2, ..., n}`
 such that for any two indices `i` and `j` with `1 ≤ i ≤ j ≤ m` and `aᵢ + aⱼ ≤ n`,

diff --git a/archive/imo/imo1998_q2.lean b/archive/imo/imo1998_q2.lean
@@ -11,6 +11,9 @@ import tactic.noncomm_ring
 
 /-!
 # IMO 1998 Q2
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 In a competition, there are `a` contestants and `b` judges, where `b ≥ 3` is an odd integer. Each
 judge rates each contestant as either "pass" or "fail". Suppose `k` is a number such that, for any
 two judges, their ratings coincide for at most `k` contestants. Prove that `k / a ≥ (b - 1) / (2b)`.