chore(analysis/complex/upper_half_plane,number_theory/modular_forms): reduce dependency on manifolds (#19212)

urkud · urkud · commit 57f9349f2fe1 · 2023-06-22T23:00:27.000Z
Move some lemmas that use `mfderiv` or `mdifferentiable` to new files.
diff --git a/src/analysis/complex/upper_half_plane/manifold.lean b/src/analysis/complex/upper_half_plane/manifold.lean
@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2022 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+import analysis.complex.upper_half_plane.topology
+import geometry.manifold.cont_mdiff_mfderiv
+/-!
+# Manifold structure on the upper half plane.
+
+In this file we define the complex manifold structure on the upper half-plane.
+-/
+
+open_locale upper_half_plane manifold
+
+namespace upper_half_plane
+
+noncomputable instance : charted_space ℂ ℍ :=
+upper_half_plane.open_embedding_coe.singleton_charted_space
+
+instance : smooth_manifold_with_corners 𝓘(ℂ) ℍ :=
+upper_half_plane.open_embedding_coe.singleton_smooth_manifold_with_corners 𝓘(ℂ)
+
+/-- The inclusion map `ℍ → ℂ` is a smooth map of manifolds. -/
+lemma smooth_coe : smooth 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) :=
+λ x, cont_mdiff_at_ext_chart_at
+
+/-- The inclusion map `ℍ → ℂ` is a differentiable map of manifolds. -/
+lemma mdifferentiable_coe : mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) :=
+smooth_coe.mdifferentiable
+
+end upper_half_plane
diff --git a/src/analysis/complex/upper_half_plane/topology.lean b/src/analysis/complex/upper_half_plane/topology.lean
@@ -9,7 +9,6 @@ import analysis.convex.normed
 import analysis.convex.complex
 import analysis.complex.re_im_topology
 import topology.homotopy.contractible
-import geometry.manifold.cont_mdiff_mfderiv
 
 /-!
 # Topology on the upper half plane
@@ -20,7 +19,7 @@ various instances.
 
 noncomputable theory
 open set filter function topological_space complex
-open_locale filter topology upper_half_plane manifold
+open_locale filter topology upper_half_plane
 
 namespace upper_half_plane
 
@@ -58,18 +57,4 @@ end
 
 instance : locally_compact_space ℍ := open_embedding_coe.locally_compact_space
 
-instance upper_half_plane.charted_space : charted_space ℂ ℍ :=
-upper_half_plane.open_embedding_coe.singleton_charted_space
-
-instance upper_half_plane.smooth_manifold_with_corners : smooth_manifold_with_corners 𝓘(ℂ) ℍ :=
-upper_half_plane.open_embedding_coe.singleton_smooth_manifold_with_corners 𝓘(ℂ)
-
-/-- The inclusion map `ℍ → ℂ` is a smooth map of manifolds. -/
-lemma smooth_coe : smooth 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) :=
-λ x, cont_mdiff_at_ext_chart_at
-
-/-- The inclusion map `ℍ → ℂ` is a differentiable map of manifolds. -/
-lemma mdifferentiable_coe : mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (coe : ℍ → ℂ) :=
-smooth_coe.mdifferentiable
-
 end upper_half_plane
diff --git a/src/number_theory/modular_forms/basic.lean b/src/number_theory/modular_forms/basic.lean
@@ -3,9 +3,8 @@ Copyright (c) 2022 Chris Birkbeck. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Birkbeck
 -/
-
 import analysis.complex.upper_half_plane.functions_bounded_at_infty
-import analysis.complex.upper_half_plane.topology
+import analysis.complex.upper_half_plane.manifold
 import number_theory.modular_forms.slash_invariant_forms
 /-!
 # Modular forms
diff --git a/src/number_theory/modular_forms/jacobi_theta/basic.lean b/src/number_theory/modular_forms/jacobi_theta/basic.lean
@@ -19,9 +19,8 @@ and proves the modular transformation properties `θ (τ + 2) = θ τ` and
 show that `θ` is differentiable on `ℍ`, and `θ(τ) - 1` has exponential decay as `im τ → ∞`.
 -/
 
-open complex real asymptotics
-
-open_locale real big_operators upper_half_plane manifold
+open complex real asymptotics filter
+open_locale real big_operators upper_half_plane
 
 /-- Jacobi's theta function `∑' (n : ℤ), exp (π * I * n ^ 2 * τ)`. -/
 noncomputable def jacobi_theta (z : ℂ) : ℂ := ∑' (n : ℤ), cexp (π * I * n ^ 2 * z)
@@ -151,7 +150,7 @@ end
 
 /-- The norm of `jacobi_theta τ - 1` decays exponentially as `im τ → ∞`. -/
 lemma is_O_at_im_infty_jacobi_theta_sub_one :
-  is_O (filter.comap im filter.at_top) (λ τ, jacobi_theta τ - 1) (λ τ, rexp (-π * τ.im)) :=
+  (λ τ, jacobi_theta τ - 1) =O[comap im at_top] (λ τ, rexp (-π * τ.im)) :=
 begin
   simp_rw [is_O, is_O_with, filter.eventually_comap, filter.eventually_at_top],
   refine ⟨2 / (1 - rexp (-π)), 1, λ y hy z hz, (norm_jacobi_theta_sub_one_le
@@ -181,8 +180,5 @@ begin
   exact differentiable_on_tsum_of_summable_norm bd_s h1 h2 (λ i w hw, le_bd (le_of_lt hw) i),
 end
 
-lemma mdifferentiable_jacobi_theta : mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (jacobi_theta ∘ coe : ℍ → ℂ) :=
-λ τ, (differentiable_at_jacobi_theta τ.2).mdifferentiable_at.comp τ τ.mdifferentiable_coe
-
 lemma continuous_at_jacobi_theta {z : ℂ} (hz : 0 < im z) :
   continuous_at jacobi_theta z := (differentiable_at_jacobi_theta hz).continuous_at
diff --git a/src/number_theory/modular_forms/jacobi_theta/manifold.lean b/src/number_theory/modular_forms/jacobi_theta/manifold.lean
@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2023 David Loeffler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Loeffler
+-/
+import number_theory.modular_forms.jacobi_theta.basic
+import analysis.complex.upper_half_plane.manifold
+
+/-!
+# Manifold differentiability of the Jacobi's theta function
+
+In this file we reformulate differentiability of the Jacobi's theta function in terms of manifold
+differentiability.
+
+## TODO
+
+Prove smoothness (in terms of `smooth`).
+-/
+
+open_locale upper_half_plane manifold
+
+lemma mdifferentiable_jacobi_theta : mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (jacobi_theta ∘ coe : ℍ → ℂ) :=
+λ τ, (differentiable_at_jacobi_theta τ.2).mdifferentiable_at.comp τ τ.mdifferentiable_coe
diff --git a/src/number_theory/zeta_function.lean b/src/number_theory/zeta_function.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 -/
 import analysis.special_functions.gamma.beta
-import number_theory.modular_forms.jacobi_theta
+import number_theory.modular_forms.jacobi_theta.basic
 import number_theory.zeta_values
 
 /-!
