feat(analysis/special_functions/exp): add real.exp_half (#14729)

leanprover-community · Jun 14, 2022 · 1c8f995 · 1c8f995
1 parent da5a737
commit 1c8f995
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/analysis/special_functions/exp.lean b/src/analysis/special_functions/exp.lean
@@ -131,6 +131,9 @@ namespace real
 
 variables {x y z : ℝ}
 
+lemma exp_half (x : ℝ) : exp (x / 2) = sqrt (exp x) :=
+by rw [eq_comm, sqrt_eq_iff_sq_eq, sq, ← exp_add, add_halves]; exact (exp_pos _).le
+
 /-- The real exponential function tends to `+∞` at `+∞`. -/
 lemma tendsto_exp_at_top : tendsto exp at_top at_top :=
 begin