refactor(analysis/complex/exponential): split into three files in spe…

…cial_functions/ (leanprover-community#2565) The file `analysis/complex/exponential.lean` was growing out of control (2500 lines) and was dealing with complex and real exponentials, trigonometric functions, and power functions. I split it into three files corresponding to these three topics, and put them instead in `analysis/special_functions/`, as it was not specifically complex. This is purely a refactor, so absolutely no new material nor changed proof. Related Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.232565.20exponential.20split
cipher1024 · Mar 15, 2022 · b3f381a · b3f381a
1 parent a9aa583
commit b3f381a
Show file tree

Hide file tree

Showing 14 changed files with 1,050 additions and 989 deletions.
diff --git a/src/analysis/ODE/gronwall.lean b/src/analysis/ODE/gronwall.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import analysis.calculus.mean_value
-import analysis.complex.exponential
+import analysis.special_functions.exp_log
 
 /-!
 # Grönwall's inequality
@@ -56,8 +56,8 @@ begin
     convert ((has_deriv_at_id x).const_mul ε).const_add δ,
     rw [mul_one] },
   { simp only [gronwall_bound_of_K_ne_0 hK],
-    convert (((has_deriv_at_id x).const_mul K).rexp.const_mul δ).add
-      ((((has_deriv_at_id x).const_mul K).rexp.sub_const 1).const_mul (ε / K)) using 1,
+    convert (((has_deriv_at_id x).const_mul K).exp.const_mul δ).add
+      ((((has_deriv_at_id x).const_mul K).exp.sub_const 1).const_mul (ε / K)) using 1,
     simp only [id, mul_add, (mul_assoc _ _ _).symm, mul_comm _ K, mul_div_cancel' _ hK],
     ring }
 end

diff --git a/src/analysis/analytic/basic.lean b/src/analysis/analytic/basic.lean
@@ -5,7 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import analysis.calculus.times_cont_diff
 import tactic.omega
-import analysis.complex.exponential
+import analysis.special_functions.pow
 
 /-!
 # Analytic functions

diff --git a/src/analysis/calculus/fderiv.lean b/src/analysis/calculus/fderiv.lean
@@ -66,7 +66,7 @@ example (x : ℝ) (h : 1 + sin x ≠ 0) : differentiable_at ℝ (λ x, exp x / (
 by simp [h]
 ```
 Of course, these examples only work once `exp`, `cos` and `sin` have been shown to be
-differentiable, in `analysis.complex.exponential`.
+differentiable, in `analysis.special_functions.trigonometric`.
 
 The simplifier is not set up to compute the Fréchet derivative of maps (as these are in general
 complicated multidimensional linear maps), but it will compute one-dimensional derivatives,

diff --git a/src/analysis/calculus/specific_functions.lean b/src/analysis/calculus/specific_functions.lean
@@ -5,7 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import analysis.calculus.extend_deriv
 import analysis.calculus.iterated_deriv
-import analysis.complex.exponential
+import analysis.special_functions.exp_log
 
 /-!
 # Smoothness of specific functions

diff --git a/src/analysis/complex/polynomial.lean b/src/analysis/complex/polynomial.lean
@@ -4,7 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import topology.algebra.polynomial
-import analysis.complex.exponential
+import analysis.special_functions.pow
+
+/-!
+# The fundamental theorem of algebra
+
+This file proves that every nonconstant complex polynomial has a root.
+-/
 
 open complex polynomial metric filter is_absolute_value set
 

diff --git a/src/analysis/convex/specific_functions.lean b/src/analysis/convex/specific_functions.lean
@@ -5,7 +5,7 @@ Authors: Yury Kudryashov
 -/
 import analysis.calculus.mean_value
 import data.nat.parity
-import analysis.complex.exponential
+import analysis.special_functions.exp_log
 
 /-!
 # Collection of convex functions

diff --git a/src/analysis/mean_inequalities.lean b/src/analysis/mean_inequalities.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import analysis.convex.specific_functions
+import analysis.special_functions.pow
 
 /-!
 # Mean value inequalities

diff --git a/src/analysis/normed_space/real_inner_product.lean b/src/analysis/normed_space/real_inner_product.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou
 -/
 import algebra.quadratic_discriminant
-import analysis.complex.exponential
+import analysis.special_functions.pow
 import tactic.monotonicity