-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
lemma tendsto_rpow_atTop_of_base_lt_one (b : ℝ) (hb₀ : -1 < b) (hb₁ : b < 1) :
    Tendsto (b ^ · : ℝ → ℝ) atTop (𝓝 (0 : ℝ))

Proof state:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ ∃ c, ∀ᶠ (x : ℝ) in atTop, ‖cos (x * π)‖ ≤ c * ‖1‖

Tactic:
exact ⟨1, Eventually.of_forall fun x => by simp [Real.abs_cos_le_one]⟩

Result:
no goals

Proof state:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x => rexp (log b * x) * cos (x * π)) =o[atTop] fun _x => 1 * 1

Tactic:
refine IsLittleO.mul_isBigO ?exp ?cos

Result:
case exp
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x => rexp (log b * x)) =o[atTop] fun _x => 1

case cos
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x => cos (x * π)) =O[atTop] fun _x => 1

Proof state:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ -b < 1

Tactic:
linarith

Result:
no goals

Proof state:
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun x => 0 ^ x) atTop (𝓝 0)

Tactic:
refine Tendsto.mono_right ?_ (Iff.mpr pure_le_nhds_iff rfl)

Result:
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun x => 0 ^ x) atTop (pure 0)

Proof state:
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun x => 0 ^ x) atTop (pure 0)

Tactic:
rw [tendsto_pure]

Result:
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ^ x = 0

Proof state:
case inr.inl
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun x => 0 ^ x) atTop (𝓝 0)

case inr.inr
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x => b ^ x) atTop (𝓝 0)

Tactic:
case inr.inl => refine Tendsto.mono_right ?_ (Iff.mpr pure_le_nhds_iff rfl)
  rw [tendsto_pure]
  filter_upwards [eventually_ne_atTop 0] with _ hx
  simp [hx]

Result:
case inr.inr
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x => b ^ x) atTop (𝓝 0)

Proof state:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x => rexp (log b * x)) =o[atTop] fun _x => 1

Tactic:
rw [isLittleO_const_iff one_ne_zero]

Result:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x => rexp (log b * x)) atTop (𝓝 0)

Proof state:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
x : ℝ
⊢ ‖cos (x * π)‖ ≤ 1 * ‖1‖

Tactic:
simp [Real.abs_cos_le_one]

Result:
no goals

Proof state:
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ^ x = 0

Tactic:
filter_upwards [eventually_ne_atTop 0] with _ hx

Result:
case h
hb₀ : -1 < 0
hb₁ : 0 < 1
a✝ : ℝ
hx : a✝ ≠ 0
⊢ 0 ^ a✝ = 0

Proof state:
case inl
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x => b ^ x) atTop (𝓝 0)

case inr.inl
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun x => 0 ^ x) atTop (𝓝 0)

case inr.inr
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x => b ^ x) atTop (𝓝 0)

Tactic:
case inl => simp_rw [Real.rpow_def_of_nonpos hb.le, hb.ne, ite_false]
  rw [← isLittleO_const_iff (c := (1 : ℝ)) one_ne_zero, (one_mul (1 : ℝ)).symm]
  refine IsLittleO.mul_isBigO ?exp ?cos
  case exp =>
    rw [isLittleO_const_iff one_ne_zero]
    refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
    rw [← log_neg_eq_log, log_neg_iff (by linarith)]
    linarith
  case cos =>
    rw [isBigO_iff]
    exact ⟨1, Eventually.of_forall fun x => by simp [Real.abs_cos_le_one]⟩

Result:
case inr.inl
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun x => 0 ^ x) atTop (𝓝 0)

case inr.inr
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x => b ^ x) atTop (𝓝 0)

Proof state:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ log b < 0

Tactic:
exact (log_neg_iff hb).mpr hb₁

Result:
no goals

Proof state:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x => cos (x * π)) =O[atTop] fun _x => 1

Tactic:
rw [isBigO_iff]

Result:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ ∃ c, ∀ᶠ (x : ℝ) in atTop, ‖cos (x * π)‖ ≤ c * ‖1‖

Proof state:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x => b ^ x) atTop (𝓝 0)

Tactic:
simp_rw [Real.rpow_def_of_nonpos hb.le, hb.ne, ite_false]

Result:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x => rexp (log b * x) * cos (x * π)) atTop (𝓝 0)

Proof state:
case inr.inr
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x => b ^ x) atTop (𝓝 0)

Tactic:
case inr.inr => simp_rw [Real.rpow_def_of_pos hb]
  refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
  exact (log_neg_iff hb).mpr hb₁

Result:
no goals

Proof state:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
⊢ Tendsto (fun x => b ^ x) atTop (𝓝 0)

Tactic:
rcases lt_trichotomy b 0 with hb|rfl|hb

Result:
case inl
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x => b ^ x) atTop (𝓝 0)

case inr.inl
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun x => 0 ^ x) atTop (𝓝 0)

case inr.inr
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x => b ^ x) atTop (𝓝 0)

Proof state:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x => rexp (log b * x)) atTop (𝓝 0)

Tactic:
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id

Result:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ log b < 0

Proof state:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x => b ^ x) atTop (𝓝 0)

Tactic:
simp_rw [Real.rpow_def_of_pos hb]

Result:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x => rexp (log b * x)) atTop (𝓝 0)

Proof state:
case exp
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x => rexp (log b * x)) =o[atTop] fun _x => 1

case cos
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x => cos (x * π)) =O[atTop] fun _x => 1

Tactic:
case exp =>
  rw [isLittleO_const_iff one_ne_zero]
  refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
  rw [← log_neg_eq_log, log_neg_iff (by linarith)]
  linarith

Result:
case cos
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x => cos (x * π)) =O[atTop] fun _x => 1

Proof state:
case h
hb₀ : -1 < 0
hb₁ : 0 < 1
a✝ : ℝ
hx : a✝ ≠ 0
⊢ 0 ^ a✝ = 0

Tactic:
simp [hx]

Result:
no goals

Proof state:
case cos
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x => cos (x * π)) =O[atTop] fun _x => 1

Tactic:
case cos =>
  rw [isBigO_iff]
  exact ⟨1, Eventually.of_forall fun x => by simp [Real.abs_cos_le_one]⟩

Result:
no goals

Proof state:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x => rexp (log b * x) * cos (x * π)) atTop (𝓝 0)

Tactic:
rw [← isLittleO_const_iff (c := (1 : ℝ)) one_ne_zero, (one_mul (1 : ℝ)).symm]

Result:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x => rexp (log b * x) * cos (x * π)) =o[atTop] fun _x => 1 * 1

Proof state:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ 0 < -b

Tactic:
linarith

Result:
no goals

Proof state:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ log b < 0

Tactic:
rw [← log_neg_eq_log, log_neg_iff (by linarith)]

Result:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ -b < 1

Proof state:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x => rexp (log b * x)) atTop (𝓝 0)

Tactic:
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id

Result:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ log b < 0