Merge remote-tracking branch 'origin/master' into kneser

leanprover-community · Oct 31, 2023 · c2a7197 · c2a7197
2 parents 3dd0117 + 65a1391
commit c2a7197
Show file tree

Hide file tree

Showing 39 changed files with 1,551 additions and 205 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/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean
@@ -106,6 +106,9 @@ variables {s s₁ s₂ : finset α} {a : α} {f g : α → β}
 @[to_additive] lemma prod_eq_multiset_prod [comm_monoid β] (s : finset α) (f : α → β) :
   ∏ x in s, f x = (s.1.map f).prod := rfl
 
+@[simp, to_additive] lemma prod_map_val [comm_monoid β] (s : finset α) (f : α → β) :
+  (s.1.map f).prod = ∏ a in s, f a := rfl
+
 @[to_additive]
 theorem prod_eq_fold [comm_monoid β] (s : finset α) (f : α → β) :
   ∏ x in s, f x = s.fold (*) 1 f :=
@@ -1418,16 +1421,19 @@ begin
   apply sum_congr rfl h₁
 end
 
+lemma nat_cast_card_filter [add_comm_monoid_with_one β] (p) [decidable_pred p] (s : finset α) :
+  ((filter p s).card : β) = ∑ a in s, if p a then 1 else 0 :=
+by simp only [add_zero, sum_const, nsmul_eq_mul, eq_self_iff_true, sum_const_zero, sum_ite,
+  nsmul_one]
+
+lemma card_filter (p) [decidable_pred p] (s : finset α) :
+  (filter p s).card = ∑ a in s, ite (p a) 1 0 :=
+nat_cast_card_filter _ _
+
 @[simp]
-lemma sum_boole {s : finset α} {p : α → Prop} [non_assoc_semiring β] {hp : decidable_pred p} :
-  (∑ x in s, if p x then (1 : β) else (0 : β)) = (s.filter p).card :=
-by simp only [add_zero,
- mul_one,
- finset.sum_const,
- nsmul_eq_mul,
- eq_self_iff_true,
- finset.sum_const_zero,
- finset.sum_ite]
+lemma sum_boole {s : finset α} {p : α → Prop} [add_comm_monoid_with_one β] {hp : decidable_pred p} :
+  (∑ x in s, if p x then 1 else 0 : β) = (s.filter p).card :=
+(nat_cast_card_filter _ _).symm
 
 lemma _root_.commute.sum_right [non_unital_non_assoc_semiring β] (s : finset α)
   (f : α → β) (b : β) (h : ∀ i ∈ s, commute b (f i)) :

diff --git a/src/algebra/big_operators/order.lean b/src/algebra/big_operators/order.lean
@@ -174,7 +174,7 @@ lemma prod_le_pow_card (s : finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s,
 begin
   refine (multiset.prod_le_pow_card (s.val.map f) n _).trans _,
   { simpa using h },
-  { simpa }
+  { simp }
 end
 
 @[to_additive card_nsmul_le_sum]

diff --git a/src/analysis/normed/group/pointwise.lean b/src/analysis/normed/group/pointwise.lean
@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel, Yaël Dillies
 -/
 import analysis.normed.group.basic
 import topology.metric_space.hausdorff_distance
+import topology.metric_space.isometric_smul
 
 /-!
 # Properties of pointwise addition of sets in normed groups
@@ -24,6 +25,7 @@ variables {E : Type*}
 section seminormed_group
 variables [seminormed_group E] {ε δ : ℝ} {s t : set E} {x y : E}
 
+-- note: we can't use `lipschitz_on_with.bounded_image2` here without adding `[isometric_smul E E]`
 @[to_additive] lemma metric.bounded.mul (hs : bounded s) (ht : bounded t) : bounded (s * t) :=
 begin
   obtain ⟨Rs, hRs⟩ : ∃ R, ∀ x ∈ s, ‖x‖ ≤ R := hs.exists_norm_le',
@@ -33,6 +35,10 @@ begin
   exact norm_mul_le_of_le (hRs x hx) (hRt y hy),
 end
 
+@[to_additive] lemma metric.bounded.of_mul (hst : bounded (s * t)) :
+  bounded s ∨ bounded t :=
+antilipschitz_with.bounded_of_image2_left _ (λ x, (isometry_mul_right x).antilipschitz) hst
+
 @[to_additive] lemma metric.bounded.inv : bounded s → bounded s⁻¹ :=
 by { simp_rw [bounded_iff_forall_norm_le', ←image_inv, ball_image_iff, norm_inv'], exact id }
 
@@ -55,6 +61,13 @@ eq_of_forall_le_iff $ λ r, by simp_rw [le_inf_edist, ←image_inv, ball_image_i
 lemma inf_edist_inv_inv (x : E) (s : set E) : inf_edist x⁻¹ s⁻¹ = inf_edist x s :=
 by rw [inf_edist_inv, inv_inv]
 
+@[to_additive] lemma ediam_mul_le (x y : set E) :
+  emetric.diam (x * y) ≤ emetric.diam x + emetric.diam y :=
+(lipschitz_on_with.ediam_image2_le (*) _ _
+    (λ _ _, (isometry_mul_right _).lipschitz.lipschitz_on_with _)
+    (λ _ _, (isometry_mul_left _).lipschitz.lipschitz_on_with _)).trans_eq $
+  by simp only [ennreal.coe_one, one_mul]
+
 end emetric
 
 variables (ε δ s t x y)