bump to nightly-2023-06-11-03

mathlib commit leanprover-community/mathlib@c471da7
leanprover-community · Jun 11, 2023 · 6960a94 · 6960a94
1 parent dee7ec8
commit 6960a94
Show file tree

Hide file tree

Showing 48 changed files with 343 additions and 124 deletions.
diff --git a/Mathbin/Algebra/Lie/CartanSubalgebra.lean b/Mathbin/Algebra/Lie/CartanSubalgebra.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 
 ! This file was ported from Lean 3 source module algebra.lie.cartan_subalgebra
-! leanprover-community/mathlib commit 938fead7abdc0cbbca8eba7a1052865a169dc102
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Algebra.Lie.Normalizer
 /-!
 # Cartan subalgebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Cartan subalgebras are one of the most important concepts in Lie theory. We define them here.
 The standard example is the set of diagonal matrices in the Lie algebra of matrices.
 

diff --git a/Mathbin/Algebra/Lie/Nilpotent.lean b/Mathbin/Algebra/Lie/Nilpotent.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 
 ! This file was ported from Lean 3 source module algebra.lie.nilpotent
-! leanprover-community/mathlib commit 6b0169218d01f2837d79ea2784882009a0da1aa1
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -17,6 +17,9 @@ import Mathbin.RingTheory.Nilpotent
 /-!
 # Nilpotent Lie algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Like groups, Lie algebras admit a natural concept of nilpotency. More generally, any Lie module
 carries a natural concept of nilpotency. We define these here via the lower central series.
 

diff --git a/Mathbin/All.lean b/Mathbin/All.lean
@@ -2024,6 +2024,7 @@ import Mathbin.LinearAlgebra.FreeModule.Finite.Basic
 import Mathbin.LinearAlgebra.FreeModule.Finite.Matrix
 import Mathbin.LinearAlgebra.FreeModule.Finite.Rank
 import Mathbin.LinearAlgebra.FreeModule.IdealQuotient
+import Mathbin.LinearAlgebra.FreeModule.Norm
 import Mathbin.LinearAlgebra.FreeModule.Pid
 import Mathbin.LinearAlgebra.FreeModule.Rank
 import Mathbin.LinearAlgebra.FreeModule.StrongRankCondition

diff --git a/Mathbin/Analysis/Calculus/AffineMap.lean b/Mathbin/Analysis/Calculus/AffineMap.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 
 ! This file was ported from Lean 3 source module analysis.calculus.affine_map
-! leanprover-community/mathlib commit 839b92fedff9981cf3fe1c1f623e04b0d127f57c
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Analysis.Calculus.ContDiff
 /-!
 # Smooth affine maps
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains results about smoothness of affine maps.
 
 ## Main definitions:

diff --git a/Mathbin/Analysis/Complex/AbsMax.lean b/Mathbin/Analysis/Complex/AbsMax.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.complex.abs_max
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.Topology.Algebra.Order.ExtrClosure
 /-!
 # Maximum modulus principle
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove several versions of the maximum modulus principle. There are several
 statements that can be called "the maximum modulus principle" for maps between normed complex
 spaces. They differ by assumptions on the domain (any space, a nontrivial space, a finite

diff --git a/Mathbin/Analysis/Complex/CauchyIntegral.lean b/Mathbin/Analysis/Complex/CauchyIntegral.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.complex.cauchy_integral
-! leanprover-community/mathlib commit fd5edc43dc4f10b85abfe544b88f82cf13c5f844
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -20,6 +20,9 @@ import Mathbin.Data.Real.Cardinality
 /-!
 # Cauchy integral formula
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove the Cauchy-Goursat theorem and the Cauchy integral formula for integrals over
 circles. Most results are formulated for a function `f : ℂ → E` that takes values in a complex
 Banach space with second countable topology.

diff --git a/Mathbin/Analysis/Complex/Liouville.lean b/Mathbin/Analysis/Complex/Liouville.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.complex.liouville
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.Analysis.NormedSpace.Completion
 /-!
 # Liouville's theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove Liouville's theorem: if `f : E → F` is complex differentiable on the whole
 space and its range is bounded, then the function is a constant. Various versions of this theorem
 are formalized in `differentiable.apply_eq_apply_of_bounded`,

diff --git a/Mathbin/Analysis/Complex/LocallyUniformLimit.lean b/Mathbin/Analysis/Complex/LocallyUniformLimit.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Vincent Beffara
 
 ! This file was ported from Lean 3 source module analysis.complex.locally_uniform_limit
-! leanprover-community/mathlib commit fe44cd36149e675eb5dec87acc7e8f1d6568e081
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Analysis.Calculus.Series
 /-!
 # Locally uniform limits of holomorphic functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file gathers some results about locally uniform limits of holomorphic functions on an open
 subset of the complex plane.
 

diff --git a/Mathbin/Analysis/Complex/PhragmenLindelof.lean b/Mathbin/Analysis/Complex/PhragmenLindelof.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.complex.phragmen_lindelof
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Analysis.Asymptotics.SuperpolynomialDecay
 /-!
 # Phragmen-Lindelöf principle
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove several versions of the Phragmen-Lindelöf principle, a version of the maximum
 modulus principle for an unbounded domain.
 

diff --git a/Mathbin/Analysis/Complex/RemovableSingularity.lean b/Mathbin/Analysis/Complex/RemovableSingularity.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.complex.removable_singularity
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.Analysis.Complex.CauchyIntegral
 /-!
 # Removable singularity theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove Riemann's removable singularity theorem: if `f : ℂ → E` is complex
 differentiable in a punctured neighborhood of a point `c` and is bounded in a punctured neighborhood
 of `c` (or, more generally, $f(z) - f(c)=o((z-c)^{-1})$), then it has a limit at `c` and the

diff --git a/Mathbin/Analysis/Complex/Schwarz.lean b/Mathbin/Analysis/Complex/Schwarz.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.complex.schwarz
-! leanprover-community/mathlib commit 3f655f5297b030a87d641ad4e825af8d9679eb0b
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Analysis.Complex.RemovableSingularity
 /-!
 # Schwarz lemma
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove several versions of the Schwarz lemma.
 
 * `complex.norm_deriv_le_div_of_maps_to_ball`, `complex.abs_deriv_le_div_of_maps_to_ball`: if

diff --git a/Mathbin/Analysis/Convex/Measure.lean b/Mathbin/Analysis/Convex/Measure.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.convex.measure
-! leanprover-community/mathlib commit fd5edc43dc4f10b85abfe544b88f82cf13c5f844
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.MeasureTheory.Measure.Lebesgue.EqHaar
 /-!
 # Convex sets are null-measurable
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `E` be a finite dimensional real vector space, let `μ` be a Haar measure on `E`, let `s` be a
 convex set in `E`. Then the frontier of `s` has measure zero (see `convex.add_haar_frontier`), hence
 `s` is a `measure_theory.null_measurable_set` (see `convex.null_measurable_set`).

diff --git a/Mathbin/Analysis/Fourier/FourierTransform.lean b/Mathbin/Analysis/Fourier/FourierTransform.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 
 ! This file was ported from Lean 3 source module analysis.fourier.fourier_transform
-! leanprover-community/mathlib commit fd5edc43dc4f10b85abfe544b88f82cf13c5f844
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.MeasureTheory.Measure.Haar.OfBasis
 /-!
 # The Fourier transform
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We set up the Fourier transform for complex-valued functions on finite-dimensional spaces.
 
 ## Design choices

diff --git a/Mathbin/Analysis/NormedSpace/AddTorsorBases.lean b/Mathbin/Analysis/NormedSpace/AddTorsorBases.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 
 ! This file was ported from Lean 3 source module analysis.normed_space.add_torsor_bases
-! leanprover-community/mathlib commit 2f4cdce0c2f2f3b8cd58f05d556d03b468e1eb2e
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.LinearAlgebra.AffineSpace.FiniteDimensional
 /-!
 # Bases in normed affine spaces.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains results about bases in normed affine spaces.
 
 ## Main definitions:

diff --git a/Mathbin/Analysis/NormedSpace/ContinuousAffineMap.lean b/Mathbin/Analysis/NormedSpace/ContinuousAffineMap.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 
 ! This file was ported from Lean 3 source module analysis.normed_space.continuous_affine_map
-! leanprover-community/mathlib commit 17ef379e997badd73e5eabb4d38f11919ab3c4b3
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.Analysis.NormedSpace.OperatorNorm
 /-!
 # Continuous affine maps between normed spaces.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file develops the theory of continuous affine maps between affine spaces modelled on normed
 spaces.
 

diff --git a/Mathbin/Analysis/ODE/PicardLindelof.lean b/Mathbin/Analysis/ODE/PicardLindelof.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov, Winston Yin
 
 ! This file was ported from Lean 3 source module analysis.ODE.picard_lindelof
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Topology.MetricSpace.Contracting
 /-!
 # Picard-Lindelöf (Cauchy-Lipschitz) Theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove that an ordinary differential equation $\dot x=v(t, x)$ such that $v$ is
 Lipschitz continuous in $x$ and continuous in $t$ has a local solution, see
 `exists_forall_deriv_within_Icc_eq_of_is_picard_lindelof`.

diff --git a/Mathbin/Analysis/SpecialFunctions/ImproperIntegrals.lean b/Mathbin/Analysis/SpecialFunctions/ImproperIntegrals.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 
 ! This file was ported from Lean 3 source module analysis.special_functions.improper_integrals
-! leanprover-community/mathlib commit fd5edc43dc4f10b85abfe544b88f82cf13c5f844
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -17,6 +17,9 @@ import Mathbin.MeasureTheory.Measure.Lebesgue.Integral
 /-!
 # Evaluation of specific improper integrals
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains some integrability results, and evaluations of integrals, over `ℝ` or over
 half-infinite intervals in `ℝ`.
 

diff --git a/Mathbin/Analysis/SpecialFunctions/Stirling.lean b/Mathbin/Analysis/SpecialFunctions/Stirling.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Moritz Firsching, Fabian Kruse, Nikolas Kuhn
 
 ! This file was ported from Lean 3 source module analysis.special_functions.stirling
-! leanprover-community/mathlib commit 2c1d8ca2812b64f88992a5294ea3dba144755cd1
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Data.Real.Pi.Wallis
 /-!
 # Stirling's formula
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves Stirling's formula for the factorial.
 It states that $n!$ grows asymptotically like $\sqrt{2\pi n}(\frac{n}{e})^n$.
 

diff --git a/Mathbin/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean b/Mathbin/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 
 ! This file was ported from Lean 3 source module analysis.special_functions.trigonometric.euler_sine_prod
-! leanprover-community/mathlib commit 2c1d8ca2812b64f88992a5294ea3dba144755cd1
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.MeasureTheory.Integral.PeakFunction
 
 /-! # Euler's infinite product for the sine function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves the infinite product formula
 
 $$ \sin \pi z = \pi z \prod_{n = 1}^\infty \left(1 - \frac{z ^ 2}{n ^ 2}\right) $$

diff --git a/Mathbin/Analysis/SumIntegralComparisons.lean b/Mathbin/Analysis/SumIntegralComparisons.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin H. Wilson
 
 ! This file was ported from Lean 3 source module analysis.sum_integral_comparisons
-! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.Analysis.SpecialFunctions.Integrals
 /-!
 # Comparing sums and integrals
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Summary
 
 It is often the case that error terms in analysis can be computed by comparing

diff --git a/Mathbin/CategoryTheory/Closed/Cartesian.lean b/Mathbin/CategoryTheory/Closed/Cartesian.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Edward Ayers, Thomas Read
 
 ! This file was ported from Lean 3 source module category_theory.closed.cartesian
-! leanprover-community/mathlib commit 239d882c4fb58361ee8b3b39fb2091320edef10a
+! leanprover-community/mathlib commit fd4551cfe4b7484b81c2c9ba3405edae27659676
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -19,6 +19,9 @@ import Mathbin.CategoryTheory.Closed.Monoidal
 /-!
 # Cartesian closed categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a category with finite products, the cartesian monoidal structure is provided by the local
 instance `monoidal_of_has_finite_products`.