feat(analysis/special_functions/exp_log): continuous_on_exp/pow (#…

…7243)

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

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) :=

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