From 56bedb400b37797e5f701726a38ec060aa65465f Mon Sep 17 00:00:00 2001
From: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
Date: Thu, 22 Apr 2021 14:56:25 +0000
Subject: [PATCH] feat(analysis/special_functions/exp_log):
 `continuous_on_exp`/`pow` (#7243)

---
 src/analysis/special_functions/exp_log.lean   | 6 ++++++
 src/analysis/special_functions/integrals.lean | 4 ++--
 src/topology/algebra/monoid.lean              | 5 ++++-
 3 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/analysis/special_functions/exp_log.lean b/src/analysis/special_functions/exp_log.lean
index d7a6b16bae828..d3ad45f54fa10 100644
--- a/src/analysis/special_functions/exp_log.lean
+++ b/src/analysis/special_functions/exp_log.lean
@@ -73,6 +73,9 @@ funext $ λ x, (has_deriv_at_exp x).deriv
 @[continuity] lemma continuous_exp : continuous exp :=
 differentiable_exp.continuous
 
+lemma continuous_on_exp {s : set ℂ} : continuous_on exp s :=
+continuous_exp.continuous_on
+
 lemma times_cont_diff_exp : ∀ {n}, times_cont_diff ℂ n exp :=
 begin
   refine times_cont_diff_all_iff_nat.2 (λ n, _),
@@ -203,6 +206,9 @@ funext $ λ x, (has_deriv_at_exp x).deriv
 @[continuity] lemma continuous_exp : continuous exp :=
 differentiable_exp.continuous
 
+lemma continuous_on_exp {s : set ℝ} : continuous_on exp s :=
+continuous_exp.continuous_on
+
 lemma measurable_exp : measurable exp := continuous_exp.measurable
 
 end real
diff --git a/src/analysis/special_functions/integrals.lean b/src/analysis/special_functions/integrals.lean
index 3dd5192155d14..c47085f8a8ca5 100644
--- a/src/analysis/special_functions/integrals.lean
+++ b/src/analysis/special_functions/integrals.lean
@@ -159,7 +159,7 @@ begin
     ext,
     simp [mul_div_assoc, mul_div_cancel' _ hne] },
   rw integral_deriv_eq_sub' _ hderiv;
-  norm_num [div_sub_div_same, (continuous_pow n).continuous_on],
+  norm_num [div_sub_div_same, continuous_on_pow],
 end
 
 @[simp]
@@ -172,7 +172,7 @@ by simp
 
 @[simp]
 lemma integral_exp : ∫ x in a..b, exp x = exp b - exp a :=
-by rw integral_deriv_eq_sub'; norm_num [continuous_exp.continuous_on]
+by rw integral_deriv_eq_sub'; norm_num [continuous_on_exp]
 
 @[simp]
 lemma integral_inv (h : (0:ℝ) ∉ interval a b) : ∫ x in a..b, x⁻¹ = log (b / a) :=
diff --git a/src/topology/algebra/monoid.lean b/src/topology/algebra/monoid.lean
index dcd64d557806b..39640700e999b 100644
--- a/src/topology/algebra/monoid.lean
+++ b/src/topology/algebra/monoid.lean
@@ -269,7 +269,10 @@ lemma continuous_pow : ∀ n : ℕ, continuous (λ a : M, a ^ n)
 @[continuity]
 lemma continuous.pow {f : X → M} (h : continuous f) (n : ℕ) :
   continuous (λ b, (f b) ^ n) :=
-continuous.comp (continuous_pow n) h
+(continuous_pow n).comp h
+
+lemma continuous_on_pow {s : set M} (n : ℕ) : continuous_on (λ x, x ^ n) s :=
+(continuous_pow n).continuous_on
 
 end has_continuous_mul