feat: port Analysis.SpecialFunctions.Log.Basic (#4019)

Includes some additional declarations and golfs from #4017.

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: Parcly-Taxel

Mathlib.lean

@@ -424,6 +424,7 @@ import Mathlib.Analysis.NormedSpace.Star.Basic
 import Mathlib.Analysis.NormedSpace.Units
 import Mathlib.Analysis.Seminorm
 import Mathlib.Analysis.SpecialFunctions.Exp
+import Mathlib.Analysis.SpecialFunctions.Log.Basic
 import Mathlib.Analysis.SpecialFunctions.Polynomials
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev
 import Mathlib.Analysis.SpecificLimits.Basic

Mathlib/Analysis/SpecialFunctions/Exp.lean

@@ -348,6 +348,18 @@ theorem tendsto_exp_comp_nhds_zero {f : α → ℝ} :
   simp_rw [←comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero]
 #align real.tendsto_exp_comp_nhds_zero Real.tendsto_exp_comp_nhds_zero
 
+-- Porting note: new lemma
+theorem openEmbedding_exp : OpenEmbedding exp :=
+  isOpen_Ioi.openEmbedding_subtype_val.comp expOrderIso.toHomeomorph.openEmbedding
+
+-- Porting note: new lemma; TODO: backport & make `@[simp]`
+theorem map_exp_nhds (x : ℝ) : map exp (𝓝 x) = 𝓝 (exp x) :=
+  openEmbedding_exp.map_nhds_eq x
+
+-- Porting note: new lemma; TODO: backport & make `@[simp]`
+theorem comap_exp_nhds_exp (x : ℝ) : comap exp (𝓝 (exp x)) = 𝓝 x :=
+  (openEmbedding_exp.nhds_eq_comap x).symm
+
 theorem isLittleO_pow_exp_atTop {n : ℕ} : (fun x : ℝ => x ^ n) =o[atTop] Real.exp := by
   simpa [isLittleO_iff_tendsto fun x hx => ((exp_pos x).ne' hx).elim] using
     tendsto_div_pow_mul_exp_add_atTop 1 0 n zero_ne_one