feat(analysis/special_functions): real.log is infinitely smooth awa…

…y from zero (#5116)

Also redefine it using `order_iso.to_homeomorph` and prove more lemmas about limits of `exp`/`log`.

src/analysis/calculus/times_cont_diff.lean

@@ -2429,6 +2429,9 @@ lemma times_cont_diff_at_inv {x : 𝕜'} (hx : x ≠ 0) {n} :
   times_cont_diff_at 𝕜 n has_inv.inv x :=
 by simpa only [inverse_eq_has_inv] using times_cont_diff_at_ring_inverse 𝕜 (units.mk0 x hx)
 
+lemma times_cont_diff_on_inv {n} : times_cont_diff_on 𝕜 n (has_inv.inv : 𝕜' → 𝕜') {0}ᶜ :=
+λ x hx, (times_cont_diff_at_inv 𝕜 hx).times_cont_diff_within_at
+
 variable {𝕜}
 
 -- TODO: the next few lemmas don't need `𝕜` or `𝕜'` to be complete
@@ -2683,7 +2686,6 @@ begin
     exact with_top.coe_le_coe.2 (nat.le_succ n) }
 end
 
-
 /-- A function is `C^∞` on an open domain if and only if it is differentiable
 there, and its derivative (formulated with `deriv`) is `C^∞`. -/
 theorem times_cont_diff_on_top_iff_deriv_of_open (hs : is_open s₂) :