e as limit of (1+1/n)^n

Stream: Is there code for X?

[Bhavik Mehta]

Does mathlib have a statement like this?

import analysis.specific_limits
import analysis.calculus.deriv
import analysis.special_functions.exp_log
import analysis.special_functions.pow

open_locale big_operators filter topological_space

example (t : ℝ) : filter.tendsto (λ (x : ℝ), (1 + t/x)^x) filter.at_top (𝓝 (real.exp t)) :=
begin

end

[Adam Topaz]

I don't know the answer, but it would be nice to have the more general form $\exp(t) = \lim_x (1+t/x)^x$.

[Bhavik Mehta]

Good point - I've amended the original post

[Anatole Dedecker]

I haven't done an extensive check but I would be surprised if those existed, since I've spent quite a lot of times using files where it could have been and have never seen it

[Bhavik Mehta]

I've got a roughly 50 line proof but I'm sure someone else will find a much nicer one!

[Eric Rodriguez]

Something similar is proved here: https://github.com/leanprover-community/mathlib/blob/700c4cb6f6d85b589d76f7e88fa9e26c74689149/src/data/equiv/derangements/exponential.lean (this is part of the derangements PR, fwiw)

The issue is that exp is defined using cau_seq, so it needs converting

[Mario Carneiro]

You shouldn't need to inspect the definition of exp here. real.pow is defined using exp, so you only need something like the derivative of log at 1

[Sebastien Gouezel]

Yes, we have everything we need on the exponential now, so its definition through cau_seq should never ever be used anymore.

[Bhavik Mehta]

Yup, Mario's suggestion is almost exactly what I did:

lemma one_plus_div_pow_tendsto_exp (t : ℝ) :
  tendsto (λ (x : ℝ), (1 + t/x)^x) at_top (𝓝 (real.exp t)) :=
begin
  rcases eq_or_ne with (rfl : t = 0) | ht,
  { simp only [add_zero, real.exp_zero, zero_div, real.one_rpow],
    exact tendsto_const_nhds },
  suffices h : tendsto (λ x, x * real.log (1 + t/x)) at_top (𝓝 t),
  { apply ((real.continuous_exp.tendsto _).comp h).congr' _,
    refine eventually_at_top.2 _,
    refine ⟨max 1 (1 - t), λ x hx, _⟩,
    have : 0 < x := zero_lt_one.trans_le ((le_max_left _ _).trans hx),
    have : x ≠ 0 := ‹0 < x›.ne',
    have : 0 < 1 + t / x,
    { rw [add_div' _ _ _ ‹x ≠ 0›, one_mul],
      apply div_pos _ ‹0 < x›,
      linarith [(le_max_right _ _).trans hx]},
    dsimp only [function.comp_apply],
    rw [←real.log_rpow ‹0 < 1 + t / x›, real.exp_log],
    apply real.rpow_pos_of_pos ‹0 < 1 + t / x›},
  suffices h : tendsto (λ x, real.log (1 + t * x) / x) (𝓝[{0}ᶜ] 0) (𝓝 t),
  { apply (h.comp (tendsto_inv_at_top_zero'.mono_right _)).congr' _,
    { refine eventually_at_top.2 ⟨1, λ x hx, _⟩,
      dsimp,
      have : x ≠ 0 := ne_of_gt (lt_of_lt_of_le zero_lt_one hx),
      rw [←div_eq_mul_inv, div_eq_mul_inv, inv_inv', mul_comm] },
    refine inf_le_inf_left _ _,
    rw principal_mono,
    intros x,
    apply ne_of_gt },
  suffices h : tendsto (λ x, real.log (1 + x) / x) (𝓝[{0}ᶜ] 0) (𝓝 1),
  { have : tendsto (λ (x : ℝ), real.log (1 + t * x) / (t * x)) (𝓝[{0}ᶜ] 0) (𝓝 1),
    { apply h.comp (tendsto.inf (by simpa using (continuous_mul_left t).tendsto 0) _),
      simp [ht, not_or_distrib] },
    replace := tendsto.mul_const t this,
    simp_rw [one_mul, div_mul_eq_mul_div, mul_comm _ t, mul_div_mul_left _ _ ht] at this,
    exact this },
  suffices h : tendsto (λ x, (real.log (1 + x) - x) / x) (𝓝[{0}ᶜ] 0) (𝓝 0),
  { simp_rw [sub_div] at h,
    have : tendsto (λ (x : ℝ), real.log (1 + x) / x - 1) (𝓝[{0}ᶜ] 0) (𝓝 0),
    { apply h.congr' (eventually_inf_principal.2 _),
      rw eventually_nhds_iff,
      exact ⟨set.univ, λ x _ (hx : x ≠ 0), by simp [div_self hx], is_open_univ, ⟨⟩⟩ },
    simpa using this.add_const 1 },
  apply asymptotics.is_o.tendsto_0,
  have : has_deriv_at real.log 1 1,
    by simpa using real.has_deriv_at_log (show (1 : ℝ) ≠ 0, by norm_num),
  rw has_deriv_at_iff_is_o_nhds_zero at this,
  simp only [mul_one, algebra.id.smul_eq_mul, real.log_one, sub_zero] at this,
  apply this.mono inf_le_left,
end

[Bhavik Mehta]

PR'd as #8243

[Yaël Dillies]

"The Fact"