t : ℝ
⊢ (exp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
t : ℝ
⊢ Tendsto (fun x => (1 + t / x) ^ x) atTop (𝓝 (exp t))
apply ((Real.continuous_exp.tendsto _).comp (tendsto_mul_log_one_plus_div_atTop t)).congr' _
t : ℝ
h₁ : 1 / 2 < 1
⊢ (exp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
t : ℝ
⊢ (exp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
have h₁ : (1 : ℝ) / 2 < 1 := by linarith
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
⊢ (exp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
t : ℝ
h₁ : 1 / 2 < 1
⊢ (exp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
have h₂ : Tendsto (fun x : ℝ => 1 + t / x) atTop (𝓝 1) := by
  simpa using (tendsto_inv_atTop_zero.const_mul t).const_add 1
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
⊢ (exp ∘ fun x => x * log (1 + t / x)) x = (fun x => (1 + t / x) ^ x) x
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
⊢ (exp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
refine' (eventually_ge_of_tendsto_gt h₁ h₂).mono fun x hx => _
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
hx' : 0 < 1 + t / x
⊢ (exp ∘ fun x => x * log (1 + t / x)) x = (fun x => (1 + t / x) ^ x) x
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
⊢ (exp ∘ fun x => x * log (1 + t / x)) x = (fun x => (1 + t / x) ^ x) x
have hx' : 0 < 1 + t / x := by linarith
no goals
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
hx' : 0 < 1 + t / x
⊢ (exp ∘ fun x => x * log (1 + t / x)) x = (fun x => (1 + t / x) ^ x) x
simp [mul_comm x, exp_mul, exp_log hx']
no goals
t : ℝ
⊢ 1 / 2 < 1
linarith
no goals
t : ℝ
h₁ : 1 / 2 < 1
⊢ Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
simpa using (tendsto_inv_atTop_zero.const_mul t).const_add 1
no goals
t : ℝ
h₁ : 1 / 2 < 1
h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)
x : ℝ
hx : 1 / 2 ≤ 1 + t / x
⊢ 0 < 1 + t / x
linarith