bump to nightly-2023-06-24-03

mathlib commit leanprover-community/mathlib@93f8809

Mathbin/AlgebraicGeometry/GammaSpecAdjunction.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Junyan Xu
 
 ! This file was ported from Lean 3 source module algebraic_geometry.Gamma_Spec_adjunction
-! leanprover-community/mathlib commit d39590fc8728fbf6743249802486f8c91ffe07bc
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.CategoryTheory.Adjunction.Reflective
 /-!
 # Adjunction between `Γ` and `Spec`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the adjunction `Γ_Spec.adjunction : Γ ⊣ Spec` by defining the unit (`to_Γ_Spec`,
 in multiple steps in this file) and counit (done in Spec.lean) and checking that they satisfy
 the left and right triangle identities. The constructions and proofs make use of

Mathbin/AlgebraicGeometry/OpenImmersion/Scheme.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module algebraic_geometry.open_immersion.Scheme
-! leanprover-community/mathlib commit 533f62f4dd62a5aad24a04326e6e787c8f7e98b1
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.CategoryTheory.Limits.Shapes.CommSq
 /-!
 # Open immersions of schemes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 -/
 
 

Mathbin/All.lean

@@ -585,6 +585,7 @@ import Mathbin.Analysis.Complex.Schwarz
 import Mathbin.Analysis.Complex.UnitDisc.Basic
 import Mathbin.Analysis.Complex.UpperHalfPlane.Basic
 import Mathbin.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
+import Mathbin.Analysis.Complex.UpperHalfPlane.Manifold
 import Mathbin.Analysis.Complex.UpperHalfPlane.Metric
 import Mathbin.Analysis.Complex.UpperHalfPlane.Topology
 import Mathbin.Analysis.ConstantSpeed
@@ -2338,7 +2339,8 @@ import Mathbin.NumberTheory.LucasLehmer
 import Mathbin.NumberTheory.LucasPrimality
 import Mathbin.NumberTheory.ModularForms.Basic
 import Mathbin.NumberTheory.ModularForms.CongruenceSubgroups
-import Mathbin.NumberTheory.ModularForms.JacobiTheta
+import Mathbin.NumberTheory.ModularForms.JacobiTheta.Basic
+import Mathbin.NumberTheory.ModularForms.JacobiTheta.Manifold
 import Mathbin.NumberTheory.ModularForms.SlashActions
 import Mathbin.NumberTheory.ModularForms.SlashInvariantForms
 import Mathbin.NumberTheory.Modular
@@ -3106,6 +3108,7 @@ import Mathbin.Topology.MetricSpace.CauSeqFilter
 import Mathbin.Topology.MetricSpace.Closeds
 import Mathbin.Topology.MetricSpace.Completion
 import Mathbin.Topology.MetricSpace.Contracting
+import Mathbin.Topology.MetricSpace.Dilation
 import Mathbin.Topology.MetricSpace.EmetricParacompact
 import Mathbin.Topology.MetricSpace.EmetricSpace
 import Mathbin.Topology.MetricSpace.Equicontinuity

Mathbin/Analysis/Calculus/Implicit.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.calculus.implicit
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! 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.NormedSpace.Complemented
 /-!
 # Implicit function theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We prove three versions of the implicit function theorem. First we define a structure
 `implicit_function_data` that holds arguments for the most general version of the implicit function
 theorem, see `implicit_function_data.implicit_function`

Mathbin/Analysis/Complex/UpperHalfPlane/Manifold.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2022 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+
+! This file was ported from Lean 3 source module analysis.complex.upper_half_plane.manifold
+! leanprover-community/mathlib commit 57f9349f2fe19d2de7207e99b0341808d977cdcf
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathbin.Analysis.Complex.UpperHalfPlane.Topology
+import Mathbin.Geometry.Manifold.ContMdiffMfderiv
+
+/-!
+# Manifold structure on the upper half plane.
+
+In this file we define the complex manifold structure on the upper half-plane.
+-/
+
+
+open scoped UpperHalfPlane Manifold
+
+namespace UpperHalfPlane
+
+noncomputable instance : ChartedSpace ℂ ℍ :=
+  UpperHalfPlane.openEmbedding_coe.singletonChartedSpace
+
+instance : SmoothManifoldWithCorners 𝓘(ℂ) ℍ :=
+  UpperHalfPlane.openEmbedding_coe.singleton_smoothManifoldWithCorners 𝓘(ℂ)
+
+/-- The inclusion map `ℍ → ℂ` is a smooth map of manifolds. -/
+theorem smooth_coe : Smooth 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) := fun x => contMdiffAt_extChartAt
+#align upper_half_plane.smooth_coe UpperHalfPlane.smooth_coe
+
+/-- The inclusion map `ℍ → ℂ` is a differentiable map of manifolds. -/
+theorem mdifferentiable_coe : Mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) :=
+  smooth_coe.Mdifferentiable
+#align upper_half_plane.mdifferentiable_coe UpperHalfPlane.mdifferentiable_coe
+
+end UpperHalfPlane
+

Mathbin/Analysis/Complex/UpperHalfPlane/Topology.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.upper_half_plane.topology
-! leanprover-community/mathlib commit f0c8bf9245297a541f468be517f1bde6195105e9
+! leanprover-community/mathlib commit 57f9349f2fe19d2de7207e99b0341808d977cdcf
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,7 +14,6 @@ import Mathbin.Analysis.Convex.Normed
 import Mathbin.Analysis.Convex.Complex
 import Mathbin.Analysis.Complex.ReImTopology
 import Mathbin.Topology.Homotopy.Contractible
-import Mathbin.Geometry.Manifold.ContMdiffMfderiv
 
 /-!
 # Topology on the upper half plane
@@ -28,7 +27,7 @@ noncomputable section
 
 open Set Filter Function TopologicalSpace Complex
 
-open scoped Filter Topology UpperHalfPlane Manifold
+open scoped Filter Topology UpperHalfPlane
 
 namespace UpperHalfPlane
 
@@ -80,22 +79,5 @@ instance : NoncompactSpace ℍ := by
 instance : LocallyCompactSpace ℍ :=
   openEmbedding_coe.LocallyCompactSpace
 
-instance UpperHalfPlane.chartedSpace : ChartedSpace ℂ ℍ :=
-  UpperHalfPlane.openEmbedding_coe.singletonChartedSpace
-#align upper_half_plane.upper_half_plane.charted_space UpperHalfPlane.UpperHalfPlane.chartedSpace
-
-instance UpperHalfPlane.smoothManifoldWithCorners : SmoothManifoldWithCorners 𝓘(ℂ) ℍ :=
-  UpperHalfPlane.openEmbedding_coe.singleton_smoothManifoldWithCorners 𝓘(ℂ)
-#align upper_half_plane.upper_half_plane.smooth_manifold_with_corners UpperHalfPlane.UpperHalfPlane.smoothManifoldWithCorners
-
-/-- The inclusion map `ℍ → ℂ` is a smooth map of manifolds. -/
-theorem smooth_coe : Smooth 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) := fun x => contMdiffAt_extChartAt
-#align upper_half_plane.smooth_coe UpperHalfPlane.smooth_coe
-
-/-- The inclusion map `ℍ → ℂ` is a differentiable map of manifolds. -/
-theorem mdifferentiable_coe : Mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) :=
-  smooth_coe.Mdifferentiable
-#align upper_half_plane.mdifferentiable_coe UpperHalfPlane.mdifferentiable_coe
-
 end UpperHalfPlane
 

Mathbin/Analysis/Matrix.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth, Eric Wieser
 
 ! This file was ported from Lean 3 source module analysis.matrix
-! leanprover-community/mathlib commit 46b633fd842bef9469441c0209906f6dddd2b4f5
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! 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.InnerProductSpace.PiL2
 /-!
 # Matrices as a normed space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we provide the following non-instances for norms on matrices:
 
 * The elementwise norm:

Mathbin/Analysis/NormedSpace/MatrixExponential.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 
 ! This file was ported from Lean 3 source module analysis.normed_space.matrix_exponential
-! leanprover-community/mathlib commit 1e3201306d4d9eb1fd54c60d7c4510ad5126f6f9
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -18,6 +18,9 @@ import Mathbin.Topology.UniformSpace.Matrix
 /-!
 # Lemmas about the matrix exponential
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we provide results about `exp` on `matrix`s over a topological or normed algebra.
 Note that generic results over all topological spaces such as `exp_zero` can be used on matrices
 without issue, so are not repeated here. The topological results specific to matrices are:

Mathbin/Analysis/NormedSpace/Star/Matrix.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Hans Parshall
 
 ! This file was ported from Lean 3 source module analysis.normed_space.star.matrix
-! leanprover-community/mathlib commit 468b141b14016d54b479eb7a0fff1e360b7e3cf6
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! 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.UnitaryGroup
 /-!
 # Unitary matrices
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file collects facts about the unitary matrices over `𝕜` (either `ℝ` or `ℂ`).
 -/
 

Mathbin/Data/Matrix/Invertible.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 
 ! This file was ported from Lean 3 source module data.matrix.invertible
-! leanprover-community/mathlib commit 722b3b152ddd5e0cf21c0a29787c76596cb6b422
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.Data.Matrix.Basic
 
 /-! # Extra lemmas about invertible matrices
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Many of the `invertible` lemmas are about `*`; this restates them to be about `⬝`.
 
 For lemmas about the matrix inverse in terms of the determinant and adjugate, see `matrix.has_inv`

Mathbin/LinearAlgebra/CliffordAlgebra/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser, Utensil Song
 
 ! This file was ported from Lean 3 source module linear_algebra.clifford_algebra.basic
-! leanprover-community/mathlib commit d46774d43797f5d1f507a63a6e904f7a533ae74a
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.LinearAlgebra.QuadraticForm.Isometry
 /-!
 # Clifford Algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We construct the Clifford algebra of a module `M` over a commutative ring `R`, equipped with
 a quadratic_form `Q`.
 

Mathbin/LinearAlgebra/ExteriorAlgebra/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhangir Azerbayev, Adam Topaz, Eric Wieser
 
 ! This file was ported from Lean 3 source module linear_algebra.exterior_algebra.basic
-! leanprover-community/mathlib commit b8d2eaa69d69ce8f03179a5cda774fc0cde984e4
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.LinearAlgebra.Alternating
 /-!
 # Exterior Algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We construct the exterior algebra of a module `M` over a commutative semiring `R`.
 
 ## Notation

Mathbin/NumberTheory/Cyclotomic/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 
 ! This file was ported from Lean 3 source module number_theory.cyclotomic.basic
-! leanprover-community/mathlib commit 4b05d3f4f0601dca8abf99c4ec99187682ed0bba
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.FieldTheory.Galois
 /-!
 # Cyclotomic extensions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `A` and `B` be commutative rings with `algebra A B`. For `S : set ℕ+`, we define a class
 `is_cyclotomic_extension S A B` expressing the fact that `B` is obtained from `A` by adding `n`-th
 primitive roots of unity, for all `n ∈ S`.

Mathbin/NumberTheory/Cyclotomic/PrimitiveRoots.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex Best, Riccardo Brasca, Eric Rodriguez
 
 ! This file was ported from Lean 3 source module number_theory.cyclotomic.primitive_roots
-! leanprover-community/mathlib commit 5bfbcca0a7ffdd21cf1682e59106d6c942434a32
+! leanprover-community/mathlib commit 5d0c76894ada7940957143163d7b921345474cbc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -18,6 +18,9 @@ import Mathbin.RingTheory.Polynomial.Cyclotomic.Expand
 
 /-!
 # Primitive roots in cyclotomic fields
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 If `is_cyclotomic_extension {n} A B`, we define an element `zeta n A B : B` that is a primitive
 `n`th-root of unity in `B` and we study its properties. We also prove related theorems under the
 more general assumption of just being a primitive root, for reasons described in the implementation

Mathbin/NumberTheory/ModularForms/Basic.lean

@@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Birkbeck
 
 ! This file was ported from Lean 3 source module number_theory.modular_forms.basic
-! leanprover-community/mathlib commit 59150e4a8ab64a88e35d5cfa0a17b762a68acfe9
+! leanprover-community/mathlib commit 57f9349f2fe19d2de7207e99b0341808d977cdcf
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
-import Mathbin.Analysis.Complex.UpperHalfPlane.Topology
+import Mathbin.Analysis.Complex.UpperHalfPlane.Manifold
 import Mathbin.NumberTheory.ModularForms.SlashInvariantForms
 
 /-!

Mathbin/NumberTheory/ModularForms/JacobiTheta.lean → Mathbin/NumberTheory/ModularForms/JacobiTheta/Basic.lean

@@ -3,8 +3,8 @@ Copyright (c) 2023 David Loeffler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 
-! This file was ported from Lean 3 source module number_theory.modular_forms.jacobi_theta
-! leanprover-community/mathlib commit c720ca1664115159ac610a74e079287d052cf8d0
+! This file was ported from Lean 3 source module number_theory.modular_forms.jacobi_theta.basic
+! leanprover-community/mathlib commit 57f9349f2fe19d2de7207e99b0341808d977cdcf
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -25,9 +25,9 @@ show that `θ` is differentiable on `ℍ`, and `θ(τ) - 1` has exponential deca
 -/
 
 
-open Complex Real Asymptotics
+open Complex Real Asymptotics Filter
 
-open scoped Real BigOperators UpperHalfPlane Manifold
+open scoped Real BigOperators UpperHalfPlane
 
 /-- Jacobi's theta function `∑' (n : ℤ), exp (π * I * n ^ 2 * τ)`. -/
 noncomputable def jacobiTheta (z : ℂ) : ℂ :=
@@ -168,7 +168,7 @@ theorem norm_jacobiTheta_sub_one_le {z : ℂ} (hz : 0 < im z) :
 
 /-- The norm of `jacobi_theta τ - 1` decays exponentially as `im τ → ∞`. -/
 theorem isBigO_at_im_infty_jacobiTheta_sub_one :
-    IsBigO (Filter.comap im Filter.atTop) (fun τ => jacobiTheta τ - 1) fun τ => rexp (-π * τ.im) :=
+    (fun τ => jacobiTheta τ - 1) =O[comap im atTop] fun τ => rexp (-π * τ.im) :=
   by
   simp_rw [is_O, is_O_with, Filter.eventually_comap, Filter.eventually_atTop]
   refine'
@@ -202,10 +202,6 @@ theorem differentiableAt_jacobiTheta {z : ℂ} (hz : 0 < im z) : DifferentiableA
   exact differentiable_on_tsum_of_summable_norm bd_s h1 h2 fun i w hw => le_bd (le_of_lt hw) i
 #align differentiable_at_jacobi_theta differentiableAt_jacobiTheta
 
-theorem mdifferentiable_jacobiTheta : Mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (jacobiTheta ∘ coe : ℍ → ℂ) :=
-  fun τ => (differentiableAt_jacobiTheta τ.2).MdifferentiableAt.comp τ τ.mdifferentiable_coe
-#align mdifferentiable_jacobi_theta mdifferentiable_jacobiTheta
-
 theorem continuousAt_jacobiTheta {z : ℂ} (hz : 0 < im z) : ContinuousAt jacobiTheta z :=
   (differentiableAt_jacobiTheta hz).ContinuousAt
 #align continuous_at_jacobi_theta continuousAt_jacobiTheta