awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
refine :
  IsBigO (E := ℝ) (F := ℂ) atTop (fun (x : ℝ) ↦ dist ((↑x : ℂ) * g x) ((↑x : ℂ) * log (1 + g x))) fun (x : ℝ) ↦
    (↑x⁻¹ : ℂ)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ dist ((↑x : ℂ) * g x) ((↑x : ℂ) * log (1 + g x))) atTop (𝓝 0)

Tactic:
refine IsBigO.trans_tendsto ?_ tendsto_inv_atTop_zero.ofReal

Premises used: tendsto_inv_atTop_zero, Filter.Tendsto.ofReal, Asymptotics.IsBigO.trans_tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
simp_rw : IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * (log (1 + g x) - g x)) fun (x : ℝ) ↦ (↑x⁻¹ : ℂ)
⊢ IsBigO (E := ℝ) (F := ℂ) atTop (fun (x : ℝ) ↦ dist ((↑x : ℂ) * g x) ((↑x : ℂ) * log (1 + g x))) fun (x : ℝ) ↦
    (↑x⁻¹ : ℂ)

Tactic:
simp_rw [dist_comm (_ * g _), dist_eq, ← mul_sub, isBigO_norm_left]

Premises used: HMul.hMul, mul_sub, dist_comm, Complex.dist_eq, Asymptotics.isBigO_norm_left
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
⊢ Tendsto g atTop (𝓝 0)

Tactic:
have hg0 := tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hg.norm.isBoundedUnder_le
        (RCLike.tendsto_ofReal_atTop_cobounded ℂ)
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
hg0 : Tendsto g atTop (𝓝 0)
⊢ IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * (log (1 + g x) - g x)) fun (x : ℝ) ↦
    (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2

Tactic:
(isBigO_refl _ _).mul (log_sub_self_isBigO.comp_tendsto hg0)

Premises used: Asymptotics.IsBigO.mul, Complex.log_sub_self_isBigO, Asymptotics.IsBigO.comp_tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
hg0 : Tendsto g atTop (𝓝 0)
⊢ IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * (log (1 + g x) - g x)) fun (x : ℝ) ↦
    (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2

Tactic:
exact (isBigO_refl _ _).mul (log_sub_self_isBigO.comp_tendsto hg0)

Premises used: Asymptotics.IsBigO.mul, Complex.log_sub_self_isBigO, Asymptotics.IsBigO.comp_tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
h : ∀ (x : ℝ) (hx0 : x ≠ 0), (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2 = HPow.hPow (β := ℕ) ((↑x : ℂ) * g x) 2 * (↑x⁻¹ : ℂ)
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2) fun (x : ℝ) ↦
    HPow.hPow (β := ℕ) ((↑x : ℂ) * g x) 2 * (↑x⁻¹ : ℂ)

Tactic:
filter_upwards [eventually_ne_atTop 0] with x hx0

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
x : ℝ
hx0 : x ≠ 0
h : (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2 * (↑x : ℂ) = HPow.hPow (β := ℕ) ((↑x : ℂ) * g x) 2
⊢ (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2 = HPow.hPow (β := ℕ) ((↑x : ℂ) * g x) 2 * (↑x⁻¹ : ℂ)

Tactic:
rw [ofReal_inv, eq_mul_inv_iff_mul_eq₀ (mod_cast hx0)]

Premises used: eq_mul_inv_iff_mul_eq₀, Complex.ofReal_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
x : ℝ
hx0 : x ≠ 0
⊢ (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2 * (↑x : ℂ) = HPow.hPow (β := ℕ) ((↑x : ℂ) * g x) 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
⊢ IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ((↑x : ℂ) * g x) 2 * (↑x⁻¹ : ℂ)) fun (x : ℝ) ↦
    (↑x⁻¹ : ℂ)

Tactic:
simpa using isBigO_const_of_tendsto hg (one_ne_zero (α := ℂ))
        |>.pow 2 |>.mul (isBigO_refl _ _)

Premises used: Asymptotics.IsBigO.mul, Asymptotics.isBigO_const_of_tendsto, Asymptotics.IsBigO.pow, one_ne_zero, OfNat.ofNat, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
_ :
  IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * (log (1 + g x) - g x)) fun (x : ℝ) ↦
    (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2
_₁ :
  EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2) fun (x : ℝ) ↦
    HPow.hPow (β := ℕ) ((↑x : ℂ) * g x) 2 * (↑x⁻¹ : ℂ)
_₂ :
  IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ((↑x : ℂ) * g x) 2 * (↑x⁻¹ : ℂ)) fun (x : ℝ) ↦
    (↑x⁻¹ : ℂ)
⊢ IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * (log (1 + g x) - g x)) fun (x : ℝ) ↦ (↑x⁻¹ : ℂ)

Tactic:
calc
    _ =O[atTop] fun x ↦ x * g x ^ 2 := by
      have hg0 := tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hg.norm.isBoundedUnder_le
        (RCLike.tendsto_ofReal_atTop_cobounded ℂ)
      exact (isBigO_refl _ _).mul (log_sub_self_isBigO.comp_tendsto hg0)
    _ =ᶠ[atTop] fun x ↦ (x * g x) ^ 2 * x⁻¹ := by
      filter_upwards [eventually_ne_atTop 0] with x hx0
      rw [ofReal_inv, eq_mul_inv_iff_mul_eq₀ (mod_cast hx0)]
      ring
    _ =O[atTop] _ := by
      simpa using isBigO_const_of_tendsto hg (one_ne_zero (α := ℂ))
        |>.pow 2 |>.mul (isBigO_refl _ _)

Premises used: HMul.hMul, Complex.ofReal, Filter.atTop, Inv.inv, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
apply : (cexp ∘ fun (x : ℝ) ↦ (↑x : ℂ) * log (1 + g x)) =ᶠ[atTop] fun (x : ℝ) ↦ (1 + g x) ^ (↑x : ℂ)
⊢ Tendsto (fun (x : ℝ) ↦ (1 + g x) ^ (↑x : ℂ)) atTop (𝓝 (cexp t))

Tactic:
apply ((continuous_exp.tendsto _).comp (tendsto_mul_log_one_add_of_tendsto hg)).congr'

Premises used: Complex.tendsto_mul_log_one_add_of_tendsto, Complex.continuous_exp, Continuous.tendsto, Filter.Tendsto.comp, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
⊢ Tendsto g atTop (𝓝 0)

Tactic:
have hg0 := tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded
    hg.norm.isBoundedUnder_le (RCLike.tendsto_ofReal_atTop_cobounded ℂ)
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
hg0 : Tendsto g atTop (𝓝 0)
⊢ Ne (α := ℂ) 0 (-1)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
hg0 : Tendsto g atTop (𝓝 0)
h : ∀ (x : ℝ) (hg1 : g x ≠ -1), (cexp ∘ fun (x : ℝ) ↦ (↑x : ℂ) * log (1 + g x)) x = (1 + g x) ^ (↑x : ℂ)
⊢ (cexp ∘ fun (x : ℝ) ↦ (↑x : ℂ) * log (1 + g x)) =ᶠ[atTop] fun (x : ℝ) ↦ (1 + g x) ^ (↑x : ℂ)

Tactic:
filter_upwards [hg0.eventually_ne (show 0 ≠ -1 by simp)] with x hg1

Premises used: Filter.Tendsto.eventually_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
hg0 : Tendsto g atTop (𝓝 0)
x : ℝ
hg1 : g x ≠ -1
h : 1 + g x ≠ 0
⊢ cexp ((↑x : ℂ) * log (1 + g x)) = (1 + g x) ^ (↑x : ℂ)

Tactic:
rw [cpow_def_of_ne_zero, mul_comm]

Premises used: mul_comm, Complex.cpow_def_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
hg0_1 : Tendsto g atTop (𝓝 0)
x : ℝ
hg1 : g x ≠ -1
hg0 : 1 + g x = 0
⊢ Ne (α := ℂ) (-1) (-1)

Tactic:
rw [← add_eq_zero_iff_neg_eq.mp hg0] at hg1

Premises used: add_eq_zero_iff_neg_eq, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
hg0_1 : Tendsto g atTop (𝓝 0)
x : ℝ
hg1 : g x ≠ -1
hg0 : 1 + g x = 0
hg1₁ : Ne (α := ℂ) (-1) (-1)
⊢ 1 + g x = 0

Tactic:
rw [← add_eq_zero_iff_neg_eq.mp hg0] at hg1

Premises used: add_eq_zero_iff_neg_eq, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
hg0_1 : Tendsto g atTop (𝓝 0)
x : ℝ
hg1 : Ne (α := ℂ) (-1) (-1)
hg0 : 1 + g x = 0
⊢ False

Tactic:
norm_num at hg1
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (t / (↑x : ℂ))) atTop (𝓝 t)
⊢ Tendsto (fun (x : ℝ) ↦ (1 + t / (↑x : ℂ)) ^ (↑x : ℂ)) atTop (𝓝 (cexp t))

Tactic:
apply tendsto_one_add_cpow_exp_of_tendsto

Premises used: Complex.tendsto_one_add_cpow_exp_of_tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℂ
hg : ∀ᶠ (x' : ℝ) in atTop, (↑x' : ℂ) * (t / (↑x' : ℂ)) = t
⊢ Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (t / (↑x : ℂ))) atTop (𝓝 t)

Tactic:
apply tendsto_nhds_of_eventually_eq

Premises used: tendsto_nhds_of_eventually_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℂ
h : ∀ (x : ℝ) (hx0 : x ≠ 0), (↑x : ℂ) * (t / (↑x : ℂ)) = t
⊢ ∀ᶠ (x' : ℝ) in atTop, (↑x' : ℂ) * (t / (↑x' : ℂ)) = t

Tactic:
filter_upwards [eventually_ne_atTop 0] with x hx0

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℂ
x : ℝ
hx0 : x ≠ 0
⊢ (↑x : ℂ) * (t / (↑x : ℂ)) = t

Tactic:
mul_div_cancel₀ t (mod_cast hx0)

Premises used: congrArg, cast, Ne, Complex.ofReal, mul_div_cancel₀, Nat.cast_zero, Eq.symm, Eq, Not, Complex.ofReal_inj._simp_1, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℂ
x : ℝ
hx0 : x ≠ 0
⊢ (↑x : ℂ) * (t / (↑x : ℂ)) = t

Tactic:
exact mul_div_cancel₀ t (mod_cast hx0)

Premises used: mul_div_cancel₀
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℕ → ℂ
t : ℂ
hg : Tendsto (fun (n : ℕ) ↦ (↑n : ℂ) * g n) atTop (𝓝 t)
⊢ ∀ (x : ℕ), ((fun (x : ℝ) ↦ (↑x : ℂ) * log (1 + g ⌊x⌋₊)) ∘ Nat.cast) x = (↑x : ℂ) * log (1 + g x)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℕ → ℂ
t : ℂ
hg : Tendsto (fun (n : ℕ) ↦ (↑n : ℂ) * g n) atTop (𝓝 t)
⊢ ∀ (x : ℕ), ((fun (x : ℝ) ↦ (1 + g ⌊x⌋₊) ^ (↑x : ℂ)) ∘ Nat.cast) x = (1 + g x) ^ x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℂ
⊢ ∀ (x : ℕ), ((fun (x : ℝ) ↦ (1 + t / (↑x : ℂ)) ^ (↑x : ℂ)) ∘ Nat.cast) x = (1 + t / (↑x : ℂ)) ^ x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
h : ∀ (x : ℕ), f x ^ x = (1 + (f x - 1)) ^ x
⊢ Eq (α := (n : ℕ) → ℂ) (fun (n : ℕ) ↦ f n ^ n) fun (n : ℕ) ↦ (1 + (f n - 1)) ^ n

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
x : ℕ
⊢ f x ^ x = (1 + (f x - 1)) ^ x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
rw : Tendsto (fun (n : ℕ) ↦ (1 + (f n - 1)) ^ n) atTop (𝓝 (cexp t))
⊢ Tendsto (fun (n : ℕ) ↦ f n ^ n) atTop (𝓝 (cexp t))

Tactic:
rw [show (fun n ↦ f n ^ n) = (fun n ↦ (1 + (f n - 1)) ^ n) by ext; simp]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
⊢ Tendsto (fun (n : ℕ) ↦ (1 + (f n - 1)) ^ n) atTop (𝓝 (cexp t))

Tactic:
tendsto_one_add_pow_exp_of_tendsto (tendsto_sub_nhds_zero_iff.1 ?_)

Premises used: Iff.mp, Complex.tendsto_one_add_pow_exp_of_tendsto, tendsto_sub_nhds_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
refine : Tendsto (β := ℂ) (fun (x : ℕ) ↦ (↑x : ℂ) * (f x - 1) - t) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ (1 + (f n - 1)) ^ n) atTop (𝓝 (cexp t))

Tactic:
refine tendsto_one_add_pow_exp_of_tendsto (tendsto_sub_nhds_zero_iff.1 ?_)

Premises used: Iff.mp, Complex.tendsto_one_add_pow_exp_of_tendsto, tendsto_sub_nhds_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
⊢ Tendsto (β := ℂ) (fun (x : ℕ) ↦ (↑x : ℂ) * (f x - 1) - t) atTop (𝓝 0)

Tactic:
hf.tendsto_inv_smul_nhds_zero.congr' ?_

Premises used: Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
convert_2 :
  EventuallyEq (β := ℂ) atTop (fun (x : ℕ) ↦ (HDiv.hDiv (α := ℂ) 1 (↑x : ℂ))⁻¹ • (f x - (1 + t / (↑x : ℂ))))
    fun (x : ℕ) ↦ (↑x : ℂ) * (f x - 1) - t
⊢ Tendsto (β := ℂ) (fun (x : ℕ) ↦ (↑x : ℂ) * (f x - 1) - t) atTop (𝓝 0)

Tactic:
convert! hf.tendsto_inv_smul_nhds_zero.congr' ?_

Premises used: Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
h : ∀ (n : ℕ) (h0 : n ≠ 0), (HDiv.hDiv (α := ℂ) 1 (↑n : ℂ))⁻¹ • (f n - (1 + t / (↑n : ℂ))) = (↑n : ℂ) * (f n - 1) - t
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℕ) ↦ (HDiv.hDiv (α := ℂ) 1 (↑x : ℂ))⁻¹ • (f x - (1 + t / (↑x : ℂ))))
    fun (x : ℕ) ↦ (↑x : ℂ) * (f x - 1) - t

Tactic:
filter_upwards [eventually_ne_atTop 0] with n h0

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
n : ℕ
h0 : n ≠ 0
h : (↑n : ℂ) * (f n - (1 + t / (↑n : ℂ))) = (↑n : ℂ) * (f n - 1) - t
⊢ (HDiv.hDiv (α := ℂ) 1 (↑n : ℂ))⁻¹ • (f n - (1 + t / (↑n : ℂ))) = (↑n : ℂ) * (f n - 1) - t

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
n : ℕ
h0 : n ≠ 0
h : (↑n : ℂ) * f n - ((↑n : ℂ) + t) = (↑n : ℂ) * (f n - 1) - t
⊢ (↑n : ℂ) * (f n - (1 + t / (↑n : ℂ))) = (↑n : ℂ) * (f n - 1) - t

Tactic:
field_simp [n.cast_ne_zero.2 h0]

Premises used: Iff.mpr, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
n : ℕ
h0 : n ≠ 0
⊢ (↑n : ℂ) * f n - ((↑n : ℂ) + t) = (↑n : ℂ) * (f n - 1) - t

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun (x : ℝ) ↦ x * g x) atTop (𝓝 t)
⊢ atTop ≤ Bornology.cobounded ℝ

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun (x : ℝ) ↦ x * g x) atTop (𝓝 t)
⊢ Tendsto g atTop (𝓝 0)

Tactic:
have hg0 := tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded
    hg.norm.isBoundedUnder_le (tendsto_id'.mpr (by simp))
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun (x : ℝ) ↦ x * g x) atTop (𝓝 t)
hg0 : Tendsto g atTop (𝓝 0)
rw :
  ∀ (hg : Tendsto (fun (x : ℝ) ↦ (↑(x * g x) : ℂ)) atTop (𝓝 (↑t : ℂ))) (hg0 : Tendsto g atTop (𝓝 0)),
    Tendsto (fun (x : ℝ) ↦ (↑(x * log (1 + g x)) : ℂ)) atTop (𝓝 (↑t : ℂ))
⊢ Tendsto (fun (x : ℝ) ↦ x * log (1 + g x)) atTop (𝓝 t)

Tactic:
rw [← tendsto_ofReal_iff] at hg ⊢

Premises used: Filter.tendsto_ofReal_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun (x : ℝ) ↦ (↑(x * g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
hg0 : Tendsto g atTop (𝓝 0)
push_cast :
  ∀ (hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))),
    Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(log (1 + g x)) : ℂ)) atTop (𝓝 (↑t : ℂ))
⊢ Tendsto (fun (x : ℝ) ↦ (↑(x * log (1 + g x)) : ℂ)) atTop (𝓝 (↑t : ℂ))

Tactic:
push_cast at hg ⊢
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
apply :
  EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ))) fun (x : ℝ) ↦
    (↑x : ℂ) * (↑(log (1 + g x)) : ℂ)
⊢ Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(log (1 + g x)) : ℂ)) atTop (𝓝 (↑t : ℂ))

Tactic:
apply (Complex.tendsto_mul_log_one_add_of_tendsto hg).congr'

Premises used: Complex.tendsto_mul_log_one_add_of_tendsto, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
⊢ LT.lt (α := ℝ) (-1) 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
h : ∀ (x : ℝ) (hg1 : -1 ≤ g x), (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ)) = (↑x : ℂ) * (↑(log (1 + g x)) : ℂ)
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ))) fun (x : ℝ) ↦
    (↑x : ℂ) * (↑(log (1 + g x)) : ℂ)

Tactic:
filter_upwards [hg0.eventually_const_le (show (-1 : ℝ) < 0 by simp)] with x hg1

Premises used: Filter.Tendsto.eventually_const_le
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
x : ℝ
hg1 : -1 ≤ g x
linarith : 1 + g x < 0 → -1 - g x + (1 + g x - 0) = 0
⊢ 0 ≤ 1 + g x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
x : ℝ
hg1 : -1 ≤ g x
h : (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ)) = (↑x : ℂ) * Complex.log (↑(1 + g x) : ℂ)
h₁ : (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ)) = (↑x : ℂ) * Complex.log ((↑1 : ℂ) + (↑(g x) : ℂ))
h₂ h₃ : (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ)) = (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ))
⊢ (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ)) = (↑x : ℂ) * (↑(log (1 + g x)) : ℂ)

Tactic:
rw [Complex.ofReal_log (by linarith), Complex.ofReal_add, Complex.ofReal_one]

Premises used: Complex.ofReal_log, Complex.ofReal_add, Complex.ofReal_one
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
⊢ Tendsto (fun (x : ℝ) ↦ x * log (1 + t / x)) atTop (𝓝 t)

Tactic:
tendsto_mul_log_one_add_of_tendsto <|
    tendsto_const_nhds.congr' <|
      (EventuallyEq.div_mul_cancel_atTop tendsto_id).symm.trans <|
        .of_eq <| funext fun _ => mul_comm _ _

Premises used: Filter.EventuallyEq.trans, Real.tendsto_mul_log_one_add_of_tendsto, Filter.tendsto_id, tendsto_const_nhds, id, HDiv.hDiv, Filter.EventuallyEq.of_eq, funext, Filter.EventuallyEq.div_mul_cancel_atTop, mul_comm, Filter.Tendsto.congr', Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun (x : ℝ) ↦ x * g x) atTop (𝓝 t)
hg0 : Tendsto g atTop (𝓝 0)
rw :
  ∀ (hg : Tendsto (fun (x : ℝ) ↦ (↑(x * g x) : ℂ)) atTop (𝓝 (↑t : ℂ))) (hg0 : Tendsto g atTop (𝓝 0)),
    Tendsto (fun (x : ℝ) ↦ (↑((1 + g x) ^ x) : ℂ)) atTop (𝓝 (↑(rexp t) : ℂ))
⊢ Tendsto (fun (x : ℝ) ↦ (1 + g x) ^ x) atTop (𝓝 (rexp t))

Tactic:
rw [← tendsto_ofReal_iff] at hg ⊢

Premises used: Filter.tendsto_ofReal_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun (x : ℝ) ↦ (↑(x * g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
hg0 : Tendsto g atTop (𝓝 0)
push_cast :
  ∀ (hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))),
    Tendsto (fun (x : ℝ) ↦ (↑((1 + g x) ^ x) : ℂ)) atTop (𝓝 (Complex.exp (↑t : ℂ)))
⊢ Tendsto (fun (x : ℝ) ↦ (↑((1 + g x) ^ x) : ℂ)) atTop (𝓝 (↑(rexp t) : ℂ))

Tactic:
push_cast at hg ⊢
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
apply : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ)) fun (x : ℝ) ↦ (↑((1 + g x) ^ x) : ℂ)
⊢ Tendsto (fun (x : ℝ) ↦ (↑((1 + g x) ^ x) : ℂ)) atTop (𝓝 (Complex.exp (↑t : ℂ)))

Tactic:
apply (Complex.tendsto_one_add_cpow_exp_of_tendsto hg).congr'

Premises used: Complex.tendsto_one_add_cpow_exp_of_tendsto, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
h : ∀ (x : ℝ) (hg1 : -1 ≤ g x), (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ) = (↑((1 + g x) ^ x) : ℂ)
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ)) fun (x : ℝ) ↦ (↑((1 + g x) ^ x) : ℂ)

Tactic:
filter_upwards [hg0.eventually_const_le (show (-1 : ℝ) < 0 by simp)] with x hg1

Premises used: Filter.Tendsto.eventually_const_le
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
x : ℝ
hg1 : -1 ≤ g x
h : (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ) = (↑(1 + g x) : ℂ) ^ (↑x : ℂ)
h₁ : (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ) = ((↑1 : ℂ) + (↑(g x) : ℂ)) ^ (↑x : ℂ)
h₂ h₃ : (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ) = (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ)
⊢ (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ) = (↑((1 + g x) ^ x) : ℂ)

Tactic:
rw [Complex.ofReal_cpow (by linarith), Complex.ofReal_add, Complex.ofReal_one]

Premises used: Complex.ofReal_cpow, Complex.ofReal_add, Complex.ofReal_one
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
hg : Tendsto (fun (x : ℝ) ↦ x * (t / x)) atTop (𝓝 t)
⊢ Tendsto (fun (x : ℝ) ↦ (1 + t / x) ^ x) atTop (𝓝 (rexp t))

Tactic:
apply tendsto_one_add_rpow_exp_of_tendsto

Premises used: Real.tendsto_one_add_rpow_exp_of_tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
hg : ∀ᶠ (x' : ℝ) in atTop, x' * (t / x') = t
⊢ Tendsto (fun (x : ℝ) ↦ x * (t / x)) atTop (𝓝 t)

Tactic:
apply tendsto_nhds_of_eventually_eq

Premises used: tendsto_nhds_of_eventually_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
h : ∀ (x : ℝ) (hx0 : x ≠ 0), x * (t / x) = t
⊢ ∀ᶠ (x' : ℝ) in atTop, x' * (t / x') = t

Tactic:
filter_upwards [eventually_ne_atTop 0] with x hx0

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t x : ℝ
hx0 : x ≠ 0
⊢ x * (t / x) = t

Tactic:
mul_div_cancel₀ t (mod_cast hx0)

Premises used: congrArg, cast, Ne, mul_div_cancel₀, Nat.cast_zero, Eq.symm, Eq, Not, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t x : ℝ
hx0 : x ≠ 0
⊢ x * (t / x) = t

Tactic:
exact mul_div_cancel₀ t (mod_cast hx0)

Premises used: mul_div_cancel₀
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℕ → ℝ
t : ℝ
hg : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * g n) atTop (𝓝 t)
⊢ ∀ (x : ℕ), ((fun (x : ℝ) ↦ x * log (1 + g ⌊x⌋₊)) ∘ Nat.cast) x = (↑x : ℝ) * log (1 + g x)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
g : ℕ → ℝ
t : ℝ
hg : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) * g n) atTop (𝓝 t)
⊢ ∀ (x : ℕ), ((fun (x : ℝ) ↦ (1 + g ⌊x⌋₊) ^ x) ∘ Nat.cast) x = (1 + g x) ^ x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
⊢ ∀ (x : ℕ), ((fun (x : ℝ) ↦ (1 + t / x) ^ x) ∘ Nat.cast) x = (1 + t / (↑x : ℝ)) ^ x

Tactic:
simp