[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i in Finset.range n, |f i|) atTop (𝓝 r)
⊢ Summable f
[PROOFSTEP]
refine' summable_of_summable_norm ⟨r, (hasSum_iff_tendsto_nat_of_nonneg _ _).2 _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i in Finset.range n, |f i|) atTop (𝓝 r)
⊢ ∀ (i : ℕ), 0 ≤ ‖f i‖
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i in Finset.range n, |f i|) atTop (𝓝 r)
⊢ Tendsto (fun n => ∑ i in Finset.range n, ‖f i‖) atTop (𝓝 r)
[PROOFSTEP]
exact fun i ↦ norm_nonneg _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i in Finset.range n, |f i|) atTop (𝓝 r)
⊢ Tendsto (fun n => ∑ i in Finset.range n, ‖f i‖) atTop (𝓝 r)
[PROOFSTEP]
simpa only using hr
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝ : NormedField 𝕜
m : ℤ
hm : m < 0
⊢ Tendsto (fun x => ‖x ^ m‖) (𝓝[{0}ᶜ] 0) atTop
[PROOFSTEP]
rcases neg_surjective m with ⟨m, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝ : NormedField 𝕜
m : ℤ
hm : -m < 0
⊢ Tendsto (fun x => ‖x ^ (-m)‖) (𝓝[{0}ᶜ] 0) atTop
[PROOFSTEP]
rw [neg_lt_zero] at hm 
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝ : NormedField 𝕜
m : ℤ
hm : 0 < m
⊢ Tendsto (fun x => ‖x ^ (-m)‖) (𝓝[{0}ᶜ] 0) atTop
[PROOFSTEP]
lift m to ℕ using hm.le
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝ : NormedField 𝕜
m : ℕ
hm : 0 < ↑m
⊢ Tendsto (fun x => ‖x ^ (-↑m)‖) (𝓝[{0}ᶜ] 0) atTop
[PROOFSTEP]
rw [Int.coe_nat_pos] at hm 
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝ : NormedField 𝕜
m : ℕ
hm : 0 < m
⊢ Tendsto (fun x => ‖x ^ (-↑m)‖) (𝓝[{0}ᶜ] 0) atTop
[PROOFSTEP]
simp only [norm_pow, zpow_neg, zpow_ofNat, ← inv_pow]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝ : NormedField 𝕜
m : ℕ
hm : 0 < m
⊢ Tendsto (fun x => ‖x⁻¹‖ ^ m) (𝓝[{0}ᶜ] 0) atTop
[PROOFSTEP]
exact (tendsto_pow_atTop hm.ne').comp NormedField.tendsto_norm_inverse_nhdsWithin_0_atTop
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
𝕜 : Type u_5
𝔸 : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup 𝔸
inst✝ : NormedSpace 𝕜 𝔸
l : Filter ι
ε : ι → 𝕜
f : ι → 𝔸
hε : Tendsto ε l (𝓝 0)
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
⊢ Tendsto (ε • f) l (𝓝 0)
[PROOFSTEP]
rw [← isLittleO_one_iff 𝕜] at hε ⊢
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
𝕜 : Type u_5
𝔸 : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup 𝔸
inst✝ : NormedSpace 𝕜 𝔸
l : Filter ι
ε : ι → 𝕜
f : ι → 𝔸
hε : ε =o[l] fun _x => 1
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)
⊢ (ε • f) =o[l] fun _x => 1
[PROOFSTEP]
simpa using IsLittleO.smul_isBigO hε (hf.isBigO_const (one_ne_zero : (1 : 𝕜) ≠ 0))
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
⊢ ContinuousAt (fun x => x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m
[PROOFSTEP]
refine' ⟨_, continuousAt_zpow₀ _ _⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
⊢ ContinuousAt (fun x => x ^ m) x → x ≠ 0 ∨ 0 ≤ m
[PROOFSTEP]
contrapose!
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
⊢ x = 0 ∧ m < 0 → ¬ContinuousAt (fun x => x ^ m) x
[PROOFSTEP]
rintro ⟨rfl, hm⟩ hc
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
hm : m < 0
hc : ContinuousAt (fun x => x ^ m) 0
⊢ False
[PROOFSTEP]
exact
  not_tendsto_atTop_of_tendsto_nhds (hc.tendsto.mono_left nhdsWithin_le_nhds).norm
    (tendsto_norm_zpow_nhdsWithin_0_atTop hm)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ ContinuousAt Inv.inv x ↔ x ≠ 0
[PROOFSTEP]
simpa [(zero_lt_one' ℤ).not_le] using @continuousAt_zpow _ _ (-1) x
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
r₁ r₂ : ℝ
h : |r₁| < |r₂|
⊢ (fun n => r₁ ^ n) =o[atTop] fun n => r₂ ^ n
[PROOFSTEP]
refine' (IsLittleO.of_norm_left _).of_norm_right
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
r₁ r₂ : ℝ
h : |r₁| < |r₂|
⊢ (fun x => ‖r₁ ^ x‖) =o[atTop] fun x => ‖r₂ ^ x‖
[PROOFSTEP]
exact (isLittleO_pow_pow_of_lt_left (abs_nonneg r₁) h).congr (pow_abs r₁) (pow_abs r₂)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
have A : Ico 0 R ⊆ Ioo (-R) R := fun x hx ↦ ⟨(neg_lt_zero.2 (hx.1.trans_lt hx.2)).trans_le hx.1, hx.2⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
have B : Ioo 0 R ⊆ Ioo (-R) R := Subset.trans Ioo_subset_Ico_self A
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
tfae_have 1 → 3
[GOAL]
case tfae_1_to_3
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
⊢ (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
tfae_have 2 → 1
[GOAL]
case tfae_2_to_1
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
⊢ (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
exact fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
tfae_have 3 → 2
[GOAL]
case tfae_3_to_2
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
⊢ (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
[PROOFSTEP]
rintro ⟨a, ha, H⟩
[GOAL]
case tfae_3_to_2.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
a : ℝ
ha : a ∈ Set.Ioo (-R) R
H : f =O[atTop] fun x => a ^ x
⊢ ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
[PROOFSTEP]
rcases exists_between (abs_lt.2 ha) with ⟨b, hab, hbR⟩
[GOAL]
case tfae_3_to_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
a : ℝ
ha : a ∈ Set.Ioo (-R) R
H : f =O[atTop] fun x => a ^ x
b : ℝ
hab : |a| < b
hbR : b < R
⊢ ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
[PROOFSTEP]
exact
  ⟨b, ⟨(abs_nonneg a).trans_lt hab, hbR⟩,
    H.trans_isLittleO (isLittleO_pow_pow_of_abs_lt_left (hab.trans_le (le_abs_self b)))⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
tfae_have 2 → 4
[GOAL]
case tfae_2_to_4
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
⊢ (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
tfae_have 4 → 3
[GOAL]
case tfae_4_to_3
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
⊢ (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
exact fun ⟨a, ha, H⟩ ↦
  ⟨a, B ha, H⟩
    -- Add 5 and 6 using 4 → 6 → 5 → 3
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
tfae_have 4 → 6
[GOAL]
case tfae_4_to_6
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
⊢ (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
[PROOFSTEP]
rintro ⟨a, ha, H⟩
[GOAL]
case tfae_4_to_6.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : f =O[atTop] fun x => a ^ x
⊢ ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
[PROOFSTEP]
rcases bound_of_isBigO_nat_atTop H with ⟨C, hC₀, hC⟩
[GOAL]
case tfae_4_to_6.intro.intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : f =O[atTop] fun x => a ^ x
C : ℝ
hC₀ : C > 0
hC : ∀ ⦃x : ℕ⦄, a ^ x ≠ 0 → ‖f x‖ ≤ C * ‖a ^ x‖
⊢ ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
[PROOFSTEP]
refine' ⟨a, ha, C, hC₀, fun n ↦ _⟩
[GOAL]
case tfae_4_to_6.intro.intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : f =O[atTop] fun x => a ^ x
C : ℝ
hC₀ : C > 0
hC : ∀ ⦃x : ℕ⦄, a ^ x ≠ 0 → ‖f x‖ ≤ C * ‖a ^ x‖
n : ℕ
⊢ |f n| ≤ C * a ^ n
[PROOFSTEP]
simpa only [Real.norm_eq_abs, abs_pow, abs_of_nonneg ha.1.le] using hC (pow_ne_zero n ha.1.ne')
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
tfae_have 6 → 5
[GOAL]
case tfae_6_to_5
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
⊢ (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
exact fun ⟨a, ha, C, H₀, H⟩ ↦ ⟨a, ha.2, C, Or.inl H₀, H⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
tfae_have 5 → 3
[GOAL]
case tfae_5_to_3
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
⊢ (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
[PROOFSTEP]
rintro ⟨a, ha, C, h₀, H⟩
[GOAL]
case tfae_5_to_3.intro.intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
a : ℝ
ha : a < R
C : ℝ
h₀ : 0 < C ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ C * a ^ n
⊢ ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
[PROOFSTEP]
rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ (abs_nonneg _).trans (H n) with (rfl | ⟨hC₀, ha₀⟩)
[GOAL]
case tfae_5_to_3.intro.intro.intro.intro.inl
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
a : ℝ
ha : a < R
h₀ : 0 < 0 ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ 0 * a ^ n
⊢ ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
[PROOFSTEP]
obtain rfl : f = 0 := by
  ext n
  simpa using H n
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
a : ℝ
ha : a < R
h₀ : 0 < 0 ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ 0 * a ^ n
⊢ f = 0
[PROOFSTEP]
ext n
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
a : ℝ
ha : a < R
h₀ : 0 < 0 ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ 0 * a ^ n
n : ℕ
⊢ f n = OfNat.ofNat 0 n
[PROOFSTEP]
simpa using H n
[GOAL]
case tfae_5_to_3.intro.intro.intro.intro.inl
α : Type u_1
β : Type u_2
ι : Type u_3
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
a : ℝ
ha : a < R
h₀ : 0 < 0 ∨ 0 < R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ 0 =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ 0 =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ 0 =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ 0 =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ 0 =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ 0 =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ 0 =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ 0 =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ 0 =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ 0 =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ 0 =O[atTop] fun x => a ^ x) →
    ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |OfNat.ofNat 0 n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |OfNat.ofNat 0 n| ≤ C * a ^ n) →
    ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |OfNat.ofNat 0 n| ≤ C * a ^ n
H : ∀ (n : ℕ), |OfNat.ofNat 0 n| ≤ 0 * a ^ n
⊢ ∃ a, a ∈ Set.Ioo (-R) R ∧ 0 =O[atTop] fun x => a ^ x
[PROOFSTEP]
simp only [lt_irrefl, false_or_iff] at h₀ 
[GOAL]
case tfae_5_to_3.intro.intro.intro.intro.inl
α : Type u_1
β : Type u_2
ι : Type u_3
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
a : ℝ
ha : a < R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ 0 =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ 0 =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ 0 =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ 0 =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ 0 =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ 0 =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ 0 =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ 0 =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ 0 =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ 0 =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ 0 =O[atTop] fun x => a ^ x) →
    ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |OfNat.ofNat 0 n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |OfNat.ofNat 0 n| ≤ C * a ^ n) →
    ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |OfNat.ofNat 0 n| ≤ C * a ^ n
H : ∀ (n : ℕ), |OfNat.ofNat 0 n| ≤ 0 * a ^ n
h₀ : 0 < R
⊢ ∃ a, a ∈ Set.Ioo (-R) R ∧ 0 =O[atTop] fun x => a ^ x
[PROOFSTEP]
exact ⟨0, ⟨neg_lt_zero.2 h₀, h₀⟩, isBigO_zero _ _⟩
[GOAL]
case tfae_5_to_3.intro.intro.intro.intro.inr.intro
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
a : ℝ
ha : a < R
C : ℝ
h₀ : 0 < C ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ C * a ^ n
hC₀ : 0 < C
ha₀ : 0 ≤ a
⊢ ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
[PROOFSTEP]
exact
  ⟨a, A ⟨ha₀, ha⟩, isBigO_of_le' _ fun n ↦ (H n).trans <| mul_le_mul_of_nonneg_left (le_abs_self _) hC₀.le⟩
    -- Add 7 and 8 using 2 → 8 → 7 → 3
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 : (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
tfae_have 2 → 8
[GOAL]
case tfae_2_to_8
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 : (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
⊢ (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
[PROOFSTEP]
rintro ⟨a, ha, H⟩
[GOAL]
case tfae_2_to_8.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 : (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : f =o[atTop] fun x => a ^ x
⊢ ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
[PROOFSTEP]
refine' ⟨a, ha, (H.def zero_lt_one).mono fun n hn ↦ _⟩
[GOAL]
case tfae_2_to_8.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 : (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : f =o[atTop] fun x => a ^ x
n : ℕ
hn : ‖f n‖ ≤ 1 * ‖a ^ n‖
⊢ |f n| ≤ a ^ n
[PROOFSTEP]
rwa [Real.norm_eq_abs, Real.norm_eq_abs, one_mul, abs_pow, abs_of_pos ha.1] at hn 
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 : (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_8 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
tfae_have 8 → 7
[GOAL]
case tfae_8_to_7
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 : (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_8 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
⊢ (∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 : (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_8 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha.2, H⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 : (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_8 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
tfae_have 7 → 3
[GOAL]
case tfae_7_to_3
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 : (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_8 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
⊢ (∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
[PROOFSTEP]
rintro ⟨a, ha, H⟩
[GOAL]
case tfae_7_to_3.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 : (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_8 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
a : ℝ
ha : a < R
H : ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
⊢ ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
[PROOFSTEP]
have : 0 ≤ a := nonneg_of_eventually_pow_nonneg (H.mono fun n ↦ (abs_nonneg _).trans)
[GOAL]
case tfae_7_to_3.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 : (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_8 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
a : ℝ
ha : a < R
H : ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
this : 0 ≤ a
⊢ ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
[PROOFSTEP]
refine' ⟨a, A ⟨this, ha⟩, IsBigO.of_bound 1 _⟩
[GOAL]
case tfae_7_to_3.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 : (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_8 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
a : ℝ
ha : a < R
H : ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
this : 0 ≤ a
⊢ ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ 1 * ‖a ^ x‖
[PROOFSTEP]
simpa only [Real.norm_eq_abs, one_mul, abs_pow, abs_of_nonneg this]
  -- porting note: used to work without explicitly having 6 → 7
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 : (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_8 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_7_to_3 : (∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
tfae_have 6 → 7
[GOAL]
case tfae_6_to_7
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 : (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_8 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_7_to_3 : (∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
⊢ (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
[PROOFSTEP]
exact fun h ↦ tfae_8_to_7 <| tfae_2_to_8 <| tfae_3_to_2 <| tfae_5_to_3 <| tfae_6_to_5 h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 :
  (∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_4_to_6 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 : (∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_2_to_8 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x) → ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_7_to_3 : (∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x
tfae_6_to_7 :
  (∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
⊢ TFAE
    [∃ a, a ∈ Set.Ioo (-R) R ∧ f =o[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =o[atTop] fun x => a ^ x,
      ∃ a, a ∈ Set.Ioo (-R) R ∧ f =O[atTop] fun x => a ^ x, ∃ a, a ∈ Set.Ioo 0 R ∧ f =O[atTop] fun x => a ^ x,
      ∃ a, a < R ∧ ∃ C x, ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∃ C, C > 0 ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a, a < R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a, a ∈ Set.Ioo 0 R ∧ ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n]
[PROOFSTEP]
tfae_finish
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
⊢ (fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
[PROOFSTEP]
have : Tendsto (fun x : ℝ ↦ x ^ k) (𝓝[>] 1) (𝓝 1) :=
  ((continuous_id.pow k).tendsto' (1 : ℝ) 1 (one_pow _)).mono_left inf_le_left
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
⊢ (fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
[PROOFSTEP]
obtain ⟨r' : ℝ, hr' : r' ^ k < r, h1 : 1 < r'⟩ := ((this.eventually (gt_mem_nhds hr)).and self_mem_nhdsWithin).exists
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
⊢ (fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
[PROOFSTEP]
have h0 : 0 ≤ r' := zero_le_one.trans h1.le
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ (fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
[PROOFSTEP]
suffices : (fun n ↦ (n : R) ^ k : ℕ → R) =O[atTop] fun n : ℕ ↦ (r' ^ k) ^ n
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this✝ : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
this : (fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ k) ^ n
⊢ (fun n => ↑n ^ k) =o[atTop] fun n => r ^ n
case this
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ (fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ k) ^ n
[PROOFSTEP]
exact this.trans_isLittleO (isLittleO_pow_pow_of_lt_left (pow_nonneg h0 _) hr')
[GOAL]
case this
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ (fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ k) ^ n
[PROOFSTEP]
conv in (r' ^ _) ^ _ => rw [← pow_mul, mul_comm, pow_mul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
| (r' ^ k) ^ n
[PROOFSTEP]
rw [← pow_mul, mul_comm, pow_mul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
| (r' ^ k) ^ n
[PROOFSTEP]
rw [← pow_mul, mul_comm, pow_mul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
| (r' ^ k) ^ n
[PROOFSTEP]
rw [← pow_mul, mul_comm, pow_mul]
[GOAL]
case this
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ (fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ n) ^ k
[PROOFSTEP]
suffices : ∀ n : ℕ, ‖(n : R)‖ ≤ (r' - 1)⁻¹ * ‖(1 : R)‖ * ‖r' ^ n‖
[GOAL]
case this
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this✝ : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
this : ∀ (n : ℕ), ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖1‖ * ‖r' ^ n‖
⊢ (fun n => ↑n ^ k) =O[atTop] fun n => (r' ^ n) ^ k
case this
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ ∀ (n : ℕ), ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖1‖ * ‖r' ^ n‖
[PROOFSTEP]
exact (isBigO_of_le' _ this).pow _
[GOAL]
case this
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
⊢ ∀ (n : ℕ), ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖1‖ * ‖r' ^ n‖
[PROOFSTEP]
intro n
[GOAL]
case this
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖1‖ * ‖r' ^ n‖
[PROOFSTEP]
rw [mul_right_comm]
[GOAL]
case this
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ ‖↑n‖ ≤ (r' - 1)⁻¹ * ‖r' ^ n‖ * ‖1‖
[PROOFSTEP]
refine' n.norm_cast_le.trans (mul_le_mul_of_nonneg_right _ (norm_nonneg _))
[GOAL]
case this
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (fun x => x ^ k) (𝓝[Set.Ioi 1] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ ↑n ≤ (r' - 1)⁻¹ * ‖r' ^ n‖
[PROOFSTEP]
simpa [_root_.div_eq_inv_mul, Real.norm_eq_abs, abs_of_nonneg h0] using n.cast_le_pow_div_sub h1
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
r : ℝ
hr : 1 < r
⊢ Nat.cast =o[atTop] fun n => r ^ n
[PROOFSTEP]
simpa only [pow_one] using @isLittleO_pow_const_const_pow_of_one_lt R _ 1 _ hr
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
[PROOFSTEP]
by_cases h0 : r₁ = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : r₁ = 0
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
[PROOFSTEP]
refine' (isLittleO_zero _ _).congr' (mem_atTop_sets.2 <| ⟨1, fun n hn ↦ _⟩) EventuallyEq.rfl
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : r₁ = 0
n : ℕ
hn : n ≥ 1
⊢ n ∈ {x | (fun x => (fun _x => 0) x = (fun n => ↑n ^ k * r₁ ^ n) x) x}
[PROOFSTEP]
simp [zero_pow (zero_lt_one.trans_le hn), h0]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : ¬r₁ = 0
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
[PROOFSTEP]
rw [← Ne.def, ← norm_pos_iff] at h0 
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
[PROOFSTEP]
have A : (fun n ↦ (n : R) ^ k : ℕ → R) =o[atTop] fun n ↦ (r₂ / ‖r₁‖) ^ n :=
  isLittleO_pow_const_const_pow_of_one_lt k ((one_lt_div h0).2 h)
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
[PROOFSTEP]
suffices (fun n ↦ r₁ ^ n) =O[atTop] fun n ↦ ‖r₁‖ ^ n by
  simpa [div_mul_cancel _ (pow_pos h0 _).ne'] using A.mul_isBigO this
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n
this : (fun n => r₁ ^ n) =O[atTop] fun n => ‖r₁‖ ^ n
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
[PROOFSTEP]
simpa [div_mul_cancel _ (pow_pos h0 _).ne'] using A.mul_isBigO this
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n
⊢ (fun n => r₁ ^ n) =O[atTop] fun n => ‖r₁‖ ^ n
[PROOFSTEP]
exact IsBigO.of_bound 1 (by simpa using eventually_norm_pow_le r₁)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n
⊢ ∀ᶠ (x : ℕ) in atTop, ‖r₁ ^ x‖ ≤ 1 * ‖‖r₁‖ ^ x‖
[PROOFSTEP]
simpa using eventually_norm_pow_le r₁
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
r : ℝ
hr : |r| < 1
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)
[PROOFSTEP]
by_cases h0 : r = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
r : ℝ
hr : |r| < 1
h0 : r = 0
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)
[PROOFSTEP]
exact tendsto_const_nhds.congr' (mem_atTop_sets.2 ⟨1, fun n hn ↦ by simp [zero_lt_one.trans_le hn, h0]⟩)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
r : ℝ
hr : |r| < 1
h0 : r = 0
n : ℕ
hn : n ≥ 1
⊢ n ∈ {x | (fun x => 0 = (fun n => ↑n ^ k * r ^ n) x) x}
[PROOFSTEP]
simp [zero_lt_one.trans_le hn, h0]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)
[PROOFSTEP]
have hr' : 1 < |r|⁻¹ := one_lt_inv (abs_pos.2 h0) hr
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
hr' : 1 < |r|⁻¹
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)
[PROOFSTEP]
rw [tendsto_zero_iff_norm_tendsto_zero]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
hr' : 1 < |r|⁻¹
⊢ Tendsto (fun e => ‖↑e ^ k * r ^ e‖) atTop (𝓝 0)
[PROOFSTEP]
simpa [div_eq_mul_inv] using tendsto_pow_const_div_const_pow_of_one_lt k hr'
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ
hr : |r| < 1
⊢ Tendsto (fun n => ↑n * r ^ n) atTop (𝓝 0)
[PROOFSTEP]
simpa only [pow_one] using tendsto_pow_const_mul_const_pow_of_abs_lt_one 1 hr
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ
hr : 0 ≤ r
h'r : r < 1
⊢ Tendsto (fun n => ↑n * r ^ n) atTop (𝓝 0)
[PROOFSTEP]
simpa only [pow_one] using tendsto_pow_const_mul_const_pow_of_lt_one 1 hr h'r
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
⊢ Tendsto (fun n => x ^ n) atTop (𝓝 0)
[PROOFSTEP]
apply squeeze_zero_norm' (eventually_norm_pow_le x)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
⊢ Tendsto (fun n => ‖x‖ ^ n) atTop (𝓝 0)
[PROOFSTEP]
exact tendsto_pow_atTop_nhds_0_of_lt_1 (norm_nonneg _) h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
K : Type u_4
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
⊢ HasSum (fun n => ξ ^ n) (1 - ξ)⁻¹
[PROOFSTEP]
have xi_ne_one : ξ ≠ 1 := by
  contrapose! h
  simp [h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
K : Type u_4
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
⊢ ξ ≠ 1
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
K : Type u_4
inst✝ : NormedField K
ξ : K
h : ξ = 1
⊢ 1 ≤ ‖ξ‖
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
K : Type u_4
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
⊢ HasSum (fun n => ξ ^ n) (1 - ξ)⁻¹
[PROOFSTEP]
have A : Tendsto (fun n ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹)) :=
  ((tendsto_pow_atTop_nhds_0_of_norm_lt_1 h).sub tendsto_const_nhds).mul tendsto_const_nhds
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
K : Type u_4
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ HasSum (fun n => ξ ^ n) (1 - ξ)⁻¹
[PROOFSTEP]
rw [hasSum_iff_tendsto_nat_of_summable_norm]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
K : Type u_4
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Tendsto (fun n => ∑ i in Finset.range n, ξ ^ i) atTop (𝓝 (1 - ξ)⁻¹)
[PROOFSTEP]
simpa [geom_sum_eq, xi_ne_one, neg_inv, div_eq_mul_inv] using A
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
K : Type u_4
inst✝ : NormedField K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n => (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Summable fun i => ‖ξ ^ i‖
[PROOFSTEP]
simp [norm_pow, summable_geometric_of_lt_1 (norm_nonneg _) h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
K : Type u_4
inst✝ : NormedField K
ξ : K
⊢ (Summable fun n => ξ ^ n) ↔ ‖ξ‖ < 1
[PROOFSTEP]
refine' ⟨fun h ↦ _, summable_geometric_of_norm_lt_1⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
K : Type u_4
inst✝ : NormedField K
ξ : K
h : Summable fun n => ξ ^ n
⊢ ‖ξ‖ < 1
[PROOFSTEP]
obtain ⟨k : ℕ, hk : dist (ξ ^ k) 0 < 1⟩ := (h.tendsto_cofinite_zero.eventually (ball_mem_nhds _ zero_lt_one)).exists
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
K : Type u_4
inst✝ : NormedField K
ξ : K
h : Summable fun n => ξ ^ n
k : ℕ
hk : dist (ξ ^ k) 0 < 1
⊢ ‖ξ‖ < 1
[PROOFSTEP]
simp only [norm_pow, dist_zero_right] at hk 
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
K : Type u_4
inst✝ : NormedField K
ξ : K
h : Summable fun n => ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1
⊢ ‖ξ‖ < 1
[PROOFSTEP]
rw [← one_pow k] at hk 
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
K : Type u_4
inst✝ : NormedField K
ξ : K
h : Summable fun n => ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1 ^ k
⊢ ‖ξ‖ < 1
[PROOFSTEP]
exact lt_of_pow_lt_pow _ zero_le_one hk
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable fun n => ‖↑n ^ k * r ^ n‖
[PROOFSTEP]
rcases exists_between hr with ⟨r', hrr', h⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ Summable fun n => ‖↑n ^ k * r ^ n‖
[PROOFSTEP]
exact
  summable_of_isBigO_nat (summable_geometric_of_lt_1 ((norm_nonneg _).trans hrr'.le) h)
    (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt _ hrr').isBigO.norm_left
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ HasSum (fun n => ↑n * r ^ n) (r / (1 - r) ^ 2)
[PROOFSTEP]
have A : Summable (fun n ↦ (n : 𝕜) * r ^ n : ℕ → 𝕜) := by
  simpa only [pow_one] using summable_pow_mul_geometric_of_norm_lt_1 1 hr
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable fun n => ↑n * r ^ n
[PROOFSTEP]
simpa only [pow_one] using summable_pow_mul_geometric_of_norm_lt_1 1 hr
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
⊢ HasSum (fun n => ↑n * r ^ n) (r / (1 - r) ^ 2)
[PROOFSTEP]
have B : HasSum (r ^ · : ℕ → 𝕜) (1 - r)⁻¹ := hasSum_geometric_of_norm_lt_1 hr
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
⊢ HasSum (fun n => ↑n * r ^ n) (r / (1 - r) ^ 2)
[PROOFSTEP]
refine' A.hasSum_iff.2 _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
⊢ ∑' (b : ℕ), ↑b * r ^ b = r / (1 - r) ^ 2
[PROOFSTEP]
have hr' : r ≠ 1 := by
  rintro rfl
  simp [lt_irrefl] at hr 
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
⊢ r ≠ 1
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
hr : ‖1‖ < 1
A : Summable fun n => ↑n * 1 ^ n
B : HasSum (fun x => 1 ^ x) (1 - 1)⁻¹
⊢ False
[PROOFSTEP]
simp [lt_irrefl] at hr 
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
hr' : r ≠ 1
⊢ ∑' (b : ℕ), ↑b * r ^ b = r / (1 - r) ^ 2
[PROOFSTEP]
set s : 𝕜 := ∑' n : ℕ, n * r ^ n
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
hr' : r ≠ 1
s : 𝕜 := ∑' (n : ℕ), ↑n * r ^ n
⊢ s = r / (1 - r) ^ 2
[PROOFSTEP]
calc
  s = (1 - r) * s / (1 - r) := (mul_div_cancel_left _ (sub_ne_zero.2 hr'.symm)).symm
  _ = (s - r * s) / (1 - r) := by rw [_root_.sub_mul, one_mul]
  _ = (((0 : ℕ) * r ^ 0 + ∑' n : ℕ, (n + 1 : ℕ) * r ^ (n + 1)) - r * s) / (1 - r) := by rw [← tsum_eq_zero_add A]
  _ = ((r * ∑' n : ℕ, (n + 1) * r ^ n) - r * s) / (1 - r) := by
    simp [_root_.pow_succ, mul_left_comm _ r, _root_.tsum_mul_left]
  _ = r / (1 - r) ^ 2 := by simp [add_mul, tsum_add A B.summable, mul_add, B.tsum_eq, ← div_eq_mul_inv, sq, div_div]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
hr' : r ≠ 1
s : 𝕜 := ∑' (n : ℕ), ↑n * r ^ n
⊢ (1 - r) * s / (1 - r) = (s - r * s) / (1 - r)
[PROOFSTEP]
rw [_root_.sub_mul, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
hr' : r ≠ 1
s : 𝕜 := ∑' (n : ℕ), ↑n * r ^ n
⊢ (s - r * s) / (1 - r) = (↑0 * r ^ 0 + ∑' (n : ℕ), ↑(n + 1) * r ^ (n + 1) - r * s) / (1 - r)
[PROOFSTEP]
rw [← tsum_eq_zero_add A]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
hr' : r ≠ 1
s : 𝕜 := ∑' (n : ℕ), ↑n * r ^ n
⊢ (↑0 * r ^ 0 + ∑' (n : ℕ), ↑(n + 1) * r ^ (n + 1) - r * s) / (1 - r) =
    (r * ∑' (n : ℕ), (↑n + 1) * r ^ n - r * s) / (1 - r)
[PROOFSTEP]
simp [_root_.pow_succ, mul_left_comm _ r, _root_.tsum_mul_left]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
r : 𝕜
hr : ‖r‖ < 1
A : Summable fun n => ↑n * r ^ n
B : HasSum (fun x => r ^ x) (1 - r)⁻¹
hr' : r ≠ 1
s : 𝕜 := ∑' (n : ℕ), ↑n * r ^ n
⊢ (r * ∑' (n : ℕ), (↑n + 1) * r ^ n - r * s) / (1 - r) = r / (1 - r) ^ 2
[PROOFSTEP]
simp [add_mul, tsum_add A B.summable, mul_add, B.tsum_eq, ← div_eq_mul_inv, sq, div_div]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C r : ℝ
hr : r < 1
u : ℕ → α
h : ∀ (n : ℕ), ‖u n - u (n + 1)‖ ≤ C * r ^ n
⊢ ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ C * r ^ n
[PROOFSTEP]
simpa [dist_eq_norm] using h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ dist (∑ i in Finset.range n, f i) (∑ i in Finset.range (n + 1), f i) ≤ C * r ^ n
[PROOFSTEP]
rw [sum_range_succ, dist_eq_norm, ← norm_neg, neg_sub, add_sub_cancel']
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ ‖f n‖ ≤ C * r ^ n
[PROOFSTEP]
exact hf n
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ ‖∑ x in Finset.range n, f x - a‖ ≤ C * r ^ n / (1 - r)
[PROOFSTEP]
rw [← dist_eq_norm]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ dist (∑ x in Finset.range n, f x) a ≤ C * r ^ n / (1 - r)
[PROOFSTEP]
apply dist_le_of_le_geometric_of_tendsto r C hr (dist_partial_sum_le_of_le_geometric hf)
[GOAL]
case ha
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ Tendsto (fun n => ∑ i in Finset.range n, f i) atTop (𝓝 a)
[PROOFSTEP]
exact ha.tendsto_sum_nat
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f u : ℕ → α
n : ℕ
⊢ dist (∑ k in Finset.range (n + 1), u k) (∑ k in Finset.range n, u k) = ‖u n‖
[PROOFSTEP]
simp [dist_eq_norm, sum_range_succ]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f u : ℕ → α
n : ℕ
⊢ dist (∑ k in Finset.range n, u k) (∑ k in Finset.range (n + 1), u k) = ‖u n‖
[PROOFSTEP]
simp [dist_eq_norm', sum_range_succ]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
r : ℝ
hr : r < 1
h : ∀ (n : ℕ), ‖u n‖ ≤ C * r ^ n
⊢ ∀ (n : ℕ), dist (∑ k in Finset.range n, u k) (∑ k in Finset.range (n + 1), u k) ≤ C * r ^ n
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
⊢ CauchySeq fun n => ∑ k in Finset.range (n + 1), u k
[PROOFSTEP]
set v : ℕ → α := fun n ↦ if n < N then 0 else u n
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
⊢ CauchySeq fun n => ∑ k in Finset.range (n + 1), u k
[PROOFSTEP]
have hC : 0 ≤ C := (zero_le_mul_right <| pow_pos hr₀ N).mp ((norm_nonneg _).trans <| h N <| le_refl N)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
⊢ CauchySeq fun n => ∑ k in Finset.range (n + 1), u k
[PROOFSTEP]
have : ∀ n ≥ N, u n = v n := by
  intro n hn
  simp [hn, if_neg (not_lt.mpr hn)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
⊢ ∀ (n : ℕ), n ≥ N → u n = v n
[PROOFSTEP]
intro n hn
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
n : ℕ
hn : n ≥ N
⊢ u n = v n
[PROOFSTEP]
simp [hn, if_neg (not_lt.mpr hn)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
⊢ CauchySeq fun n => ∑ k in Finset.range (n + 1), u k
[PROOFSTEP]
refine' cauchySeq_sum_of_eventually_eq this (NormedAddCommGroup.cauchy_series_of_le_geometric' hr₁ _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
⊢ ℝ
[PROOFSTEP]
exact C
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
⊢ ∀ (n : ℕ), ‖v n‖ ≤ C * r ^ n
[PROOFSTEP]
intro n
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
⊢ ‖v n‖ ≤ C * r ^ n
[PROOFSTEP]
simp only
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
⊢ ‖if n < N then 0 else u n‖ ≤ C * r ^ n
[PROOFSTEP]
split_ifs with H
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
H : n < N
⊢ ‖0‖ ≤ C * r ^ n
[PROOFSTEP]
rw [norm_zero]
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
H : n < N
⊢ 0 ≤ C * r ^ n
[PROOFSTEP]
exact mul_nonneg hC (pow_nonneg hr₀.le _)
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
H : ¬n < N
⊢ ‖u n‖ ≤ C * r ^ n
[PROOFSTEP]
push_neg at H 
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : SeminormedAddCommGroup α
r✝ C✝ : ℝ
f : ℕ → α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n => if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ (n : ℕ), n ≥ N → u n = v n
n : ℕ
H : N ≤ n
⊢ ‖u n‖ ≤ C * r ^ n
[PROOFSTEP]
exact h _ H
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ Summable fun n => x ^ n
[PROOFSTEP]
have h1 : Summable fun n : ℕ ↦ ‖x‖ ^ n := summable_geometric_of_lt_1 (norm_nonneg _) h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
h1 : Summable fun n => ‖x‖ ^ n
⊢ Summable fun n => x ^ n
[PROOFSTEP]
refine' summable_of_norm_bounded_eventually _ h1 _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
h1 : Summable fun n => ‖x‖ ^ n
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖x ^ i‖ ≤ ‖x‖ ^ i
[PROOFSTEP]
rw [Nat.cofinite_eq_atTop]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
h1 : Summable fun n => ‖x‖ ^ n
⊢ ∀ᶠ (i : ℕ) in atTop, ‖x ^ i‖ ≤ ‖x‖ ^ i
[PROOFSTEP]
exact eventually_norm_pow_le x
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ ‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
[PROOFSTEP]
rw [tsum_eq_zero_add (NormedRing.summable_geometric_of_norm_lt_1 x h)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ ‖x ^ 0 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
[PROOFSTEP]
simp only [_root_.pow_zero]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ ‖1 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
[PROOFSTEP]
refine' le_trans (norm_add_le _ _) _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ ‖1‖ + ‖∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
[PROOFSTEP]
have : ‖∑' b : ℕ, (fun n ↦ x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1 :=
  by
  refine' tsum_of_norm_bounded _ fun b ↦ norm_pow_le' _ (Nat.succ_pos b)
  convert (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_1 (norm_nonneg x) h)
  simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ ‖∑' (b : ℕ), (fun n => x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1
[PROOFSTEP]
refine' tsum_of_norm_bounded _ fun b ↦ norm_pow_le' _ (Nat.succ_pos b)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ HasSum (fun b => ‖x‖ ^ (b + 1)) ((1 - ‖x‖)⁻¹ - 1)
[PROOFSTEP]
convert (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_1 (norm_nonneg x) h)
[GOAL]
case h.e'_6.h.e'_6
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ 1 = ∑ i in Finset.range 1, ‖x‖ ^ i
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this : ‖∑' (b : ℕ), (fun n => x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1
⊢ ‖1‖ + ‖∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
[PROOFSTEP]
linarith
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ (∑' (i : ℕ), x ^ i) * (1 - x) = 1
[PROOFSTEP]
have := (NormedRing.summable_geometric_of_norm_lt_1 x h).hasSum.mul_right (1 - x)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
⊢ (∑' (i : ℕ), x ^ i) * (1 - x) = 1
[PROOFSTEP]
refine' tendsto_nhds_unique this.tendsto_sum_nat _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
⊢ Tendsto (fun n => ∑ i in Finset.range n, x ^ i * (1 - x)) atTop (𝓝 1)
[PROOFSTEP]
have : Tendsto (fun n : ℕ ↦ 1 - x ^ n) atTop (𝓝 1) := by
  simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_0_of_norm_lt_1 h)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
⊢ Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
[PROOFSTEP]
simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_0_of_norm_lt_1 h)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
⊢ Tendsto (fun n => ∑ i in Finset.range n, x ^ i * (1 - x)) atTop (𝓝 1)
[PROOFSTEP]
convert ← this
[GOAL]
case h.e'_3.h
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
x✝ : ℕ
⊢ 1 - x ^ x✝ = ∑ i in Finset.range x✝, x ^ i * (1 - x)
[PROOFSTEP]
rw [← geom_sum_mul_neg, Finset.sum_mul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
⊢ (1 - x) * ∑' (i : ℕ), x ^ i = 1
[PROOFSTEP]
have := (NormedRing.summable_geometric_of_norm_lt_1 x h).hasSum.mul_left (1 - x)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)
⊢ (1 - x) * ∑' (i : ℕ), x ^ i = 1
[PROOFSTEP]
refine' tendsto_nhds_unique this.tendsto_sum_nat _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)
⊢ Tendsto (fun n => ∑ i in Finset.range n, (1 - x) * x ^ i) atTop (𝓝 1)
[PROOFSTEP]
have : Tendsto (fun n : ℕ ↦ 1 - x ^ n) atTop (nhds 1) := by
  simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_0_of_norm_lt_1 h)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)
⊢ Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
[PROOFSTEP]
simpa using tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_0_of_norm_lt_1 h)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
⊢ Tendsto (fun n => ∑ i in Finset.range n, (1 - x) * x ^ i) atTop (𝓝 1)
[PROOFSTEP]
convert ← this
[GOAL]
case h.e'_3.h
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
h : ‖x‖ < 1
this✝ : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)
this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)
x✝ : ℕ
⊢ 1 - x ^ x✝ = ∑ i in Finset.range x✝, (1 - x) * x ^ i
[PROOFSTEP]
rw [← mul_neg_geom_sum, Finset.mul_sum]
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
⊢ Summable f
[PROOFSTEP]
by_cases hr₀ : 0 ≤ r
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : 0 ≤ r
⊢ Summable f
[PROOFSTEP]
rw [eventually_atTop] at h 
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∃ a, ∀ (b : ℕ), b ≥ a → ‖f (b + 1)‖ ≤ r * ‖f b‖
hr₀ : 0 ≤ r
⊢ Summable f
[PROOFSTEP]
rcases h with ⟨N, hN⟩
[GOAL]
case pos.intro
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
⊢ Summable f
[PROOFSTEP]
rw [← @summable_nat_add_iff α _ _ _ _ N]
[GOAL]
case pos.intro
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
⊢ Summable fun n => f (n + N)
[PROOFSTEP]
refine'
  summable_of_norm_bounded (fun n ↦ ‖f N‖ * r ^ n) (Summable.mul_left _ <| summable_geometric_of_lt_1 hr₀ hr₁) fun n ↦ _
[GOAL]
case pos.intro
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
⊢ ‖f (n + N)‖ ≤ (fun n => ‖f N‖ * r ^ n) n
[PROOFSTEP]
simp only
[GOAL]
case pos.intro
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
⊢ ‖f (n + N)‖ ≤ ‖f N‖ * r ^ n
[PROOFSTEP]
conv_rhs => rw [mul_comm, ← zero_add N]
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
| ‖f N‖ * r ^ n
[PROOFSTEP]
rw [mul_comm, ← zero_add N]
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
| ‖f N‖ * r ^ n
[PROOFSTEP]
rw [mul_comm, ← zero_add N]
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
| ‖f N‖ * r ^ n
[PROOFSTEP]
rw [mul_comm, ← zero_add N]
[GOAL]
case pos.intro
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
⊢ ‖f (n + N)‖ ≤ r ^ n * ‖f (0 + N)‖
[PROOFSTEP]
refine' le_geom (u := fun n ↦ ‖f (n + N)‖) hr₀ n fun i _ ↦ _
[GOAL]
case pos.intro
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n i : ℕ
x✝ : i < n
⊢ (fun n => ‖f (n + N)‖) (i + 1) ≤ r * (fun n => ‖f (n + N)‖) i
[PROOFSTEP]
convert hN (i + N) (N.le_add_left i) using 3
[GOAL]
case h.e'_3.h.e'_3.h.e'_1
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ‖f (b + 1)‖ ≤ r * ‖f b‖
n i : ℕ
x✝ : i < n
⊢ i + 1 + N = i + N + 1
[PROOFSTEP]
ac_rfl
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : ¬0 ≤ r
⊢ Summable f
[PROOFSTEP]
push_neg at hr₀ 
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ Summable f
[PROOFSTEP]
refine' summable_of_norm_bounded_eventually 0 summable_zero _
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖f i‖ ≤ OfNat.ofNat 0 i
[PROOFSTEP]
rw [Nat.cofinite_eq_atTop]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ ∀ᶠ (i : ℕ) in atTop, ‖f i‖ ≤ OfNat.ofNat 0 i
[PROOFSTEP]
filter_upwards [h] with _ hn
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
a✝ : ℕ
hn : ‖f (a✝ + 1)‖ ≤ r * ‖f a✝‖
⊢ ‖f a✝‖ ≤ OfNat.ofNat 0 a✝
[PROOFSTEP]
by_contra' h
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h✝ : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
a✝ : ℕ
hn : ‖f (a✝ + 1)‖ ≤ r * ‖f a✝‖
h : OfNat.ofNat 0 a✝ < ‖f a✝‖
⊢ False
[PROOFSTEP]
exact not_lt.mpr (norm_nonneg _) (lt_of_le_of_lt hn <| mul_neg_of_neg_of_pos hr₀ h)
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
⊢ Summable f
[PROOFSTEP]
rcases exists_between hl₁ with ⟨r, hr₀, hr₁⟩
[GOAL]
case intro.intro
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
⊢ Summable f
[PROOFSTEP]
refine' summable_of_ratio_norm_eventually_le hr₁ _
[GOAL]
case intro.intro
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
⊢ ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
[PROOFSTEP]
filter_upwards [eventually_le_of_tendsto_lt hr₀ h, hf] with _ _ h₁
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : NormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
a✝¹ : ℕ
a✝ : ‖f (a✝¹ + 1)‖ / ‖f a✝¹‖ ≤ r
h₁ : f a✝¹ ≠ 0
⊢ ‖f (a✝¹ + 1)‖ ≤ r * ‖f a✝¹‖
[PROOFSTEP]
rwa [← div_le_iff (norm_pos_iff.mpr h₁)]
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖
⊢ ¬Summable f
[PROOFSTEP]
rw [eventually_atTop] at h 
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
h : ∃ a, ∀ (b : ℕ), b ≥ a → r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f
[PROOFSTEP]
rcases h with ⟨N₀, hN₀⟩
[GOAL]
case intro
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f
[PROOFSTEP]
rw [frequently_atTop] at hf 
[GOAL]
case intro
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f
[PROOFSTEP]
rcases hf N₀ with ⟨N, hNN₀ : N₀ ≤ N, hN⟩
[GOAL]
case intro.intro.intro
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
⊢ ¬Summable f
[PROOFSTEP]
rw [← @summable_nat_add_iff α _ _ _ _ N]
[GOAL]
case intro.intro.intro
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
⊢ ¬Summable fun n => f (n + N)
[PROOFSTEP]
refine' mt Summable.tendsto_atTop_zero fun h' ↦ not_tendsto_atTop_of_tendsto_nhds (tendsto_norm_zero.comp h') _
[GOAL]
case intro.intro.intro
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
⊢ Tendsto ((fun a => ‖a‖) ∘ fun n => f (n + N)) atTop atTop
[PROOFSTEP]
convert tendsto_atTop_of_geom_le _ hr _
[GOAL]
case intro.intro.intro.convert_2
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
⊢ 0 < ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
[PROOFSTEP]
refine' lt_of_le_of_ne (norm_nonneg _) _
[GOAL]
case intro.intro.intro.convert_2
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
⊢ 0 ≠ ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
[PROOFSTEP]
intro h''
[GOAL]
case intro.intro.intro.convert_2
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
h'' : 0 = ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
⊢ False
[PROOFSTEP]
specialize hN₀ N hNN₀
[GOAL]
case intro.intro.intro.convert_2
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
h'' : 0 = ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
hN₀ : r * ‖f N‖ ≤ ‖f (N + 1)‖
⊢ False
[PROOFSTEP]
simp only [comp_apply, zero_add] at h'' 
[GOAL]
case intro.intro.intro.convert_2
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
hN₀ : r * ‖f N‖ ≤ ‖f (N + 1)‖
h'' : 0 = ‖f N‖
⊢ False
[PROOFSTEP]
exact hN h''.symm
[GOAL]
case intro.intro.intro.convert_3
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
⊢ ∀ (n : ℕ), r * ((fun a => ‖a‖) ∘ fun n => f (n + N)) n ≤ ((fun a => ‖a‖) ∘ fun n => f (n + N)) (n + 1)
[PROOFSTEP]
intro i
[GOAL]
case intro.intro.intro.convert_3
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
i : ℕ
⊢ r * ((fun a => ‖a‖) ∘ fun n => f (n + N)) i ≤ ((fun a => ‖a‖) ∘ fun n => f (n + N)) (i + 1)
[PROOFSTEP]
dsimp only [comp_apply]
[GOAL]
case intro.intro.intro.convert_3
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
i : ℕ
⊢ r * ‖f (i + N)‖ ≤ ‖f (i + 1 + N)‖
[PROOFSTEP]
convert hN₀ (i + N) (hNN₀.trans (N.le_add_left i)) using 3
[GOAL]
case h.e'_4.h.e'_3.h.e'_1
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, b ≥ a ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), b ≥ N₀ → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto (fun n => f (n + N)) atTop (𝓝 0)
i : ℕ
⊢ i + 1 + N = i + N + 1
[PROOFSTEP]
ac_rfl
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
⊢ ¬Summable f
[PROOFSTEP]
have key : ∀ᶠ n in atTop, ‖f n‖ ≠ 0 :=
  by
  filter_upwards [eventually_ge_of_tendsto_gt hl h] with _ hn hc
  rw [hc, _root_.div_zero] at hn 
  linarith
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
⊢ ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
[PROOFSTEP]
filter_upwards [eventually_ge_of_tendsto_gt hl h] with _ hn hc
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
a✝ : ℕ
hn : 1 ≤ ‖f (a✝ + 1)‖ / ‖f a✝‖
hc : ‖f a✝‖ = 0
⊢ False
[PROOFSTEP]
rw [hc, _root_.div_zero] at hn 
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
a✝ : ℕ
hn : 1 ≤ 0
hc : ‖f a✝‖ = 0
⊢ False
[PROOFSTEP]
linarith
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
⊢ ¬Summable f
[PROOFSTEP]
rcases exists_between hl with ⟨r, hr₀, hr₁⟩
[GOAL]
case intro.intro
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
⊢ ¬Summable f
[PROOFSTEP]
refine' not_summable_of_ratio_norm_eventually_ge hr₀ key.frequently _
[GOAL]
case intro.intro
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
⊢ ∀ᶠ (n : ℕ) in atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖
[PROOFSTEP]
filter_upwards [eventually_ge_of_tendsto_gt hr₁ h, key] with _ _ h₁
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
a✝¹ : ℕ
a✝ : r ≤ ‖f (a✝¹ + 1)‖ / ‖f a✝¹‖
h₁ : ‖f a✝¹‖ ≠ 0
⊢ r * ‖f a✝¹‖ ≤ ‖f (a✝¹ + 1)‖
[PROOFSTEP]
rwa [← le_div_iff (lt_of_le_of_ne (norm_nonneg _) h₁.symm)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n => ∑ i in Finset.range (n + 1), f i • z i
[PROOFSTEP]
simp_rw [Finset.sum_range_by_parts _ _ (Nat.succ _), sub_eq_add_neg, Nat.succ_sub_succ_eq_sub, tsub_zero]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n =>
    f n • ∑ i in Finset.range (succ n), z i +
      -∑ x in Finset.range n, (f (x + 1) + -f x) • ∑ i in Finset.range (x + 1), z i
[PROOFSTEP]
apply
  (NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded hf0
      ⟨b, eventually_map.mpr <| eventually_of_forall fun n ↦ hgb <| n + 1⟩).cauchySeq.add
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n => -∑ x in Finset.range n, (f (x + 1) + -f x) • ∑ i in Finset.range (x + 1), z i
[PROOFSTEP]
refine' CauchySeq.neg _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n => ∑ x in Finset.range n, (f (x + 1) + -f x) • ∑ i in Finset.range (x + 1), z i
[PROOFSTEP]
refine'
  cauchySeq_range_of_norm_bounded _ _
    (fun n ↦ _ : ∀ n, ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n => ∑ i in Finset.range n, b * |f (i + 1) - f i|
[PROOFSTEP]
simp_rw [abs_of_nonneg (sub_nonneg_of_le (hfa (Nat.le_succ _))), ← mul_sum]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n => b * ∑ x in Finset.range n, (f (succ x) - f x)
[PROOFSTEP]
apply Real.uniformContinuous_const_mul.comp_cauchySeq
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n => ∑ x in Finset.range n, (f (succ x) - f x)
[PROOFSTEP]
simp_rw [sum_range_sub, sub_eq_add_neg]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n => f n + -f 0
[PROOFSTEP]
exact (Tendsto.cauchySeq hf0).add_const
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
n : ℕ
⊢ ‖(f (n + 1) + -f n) • Finset.sum (Finset.range (n + 1)) z‖ ≤ b * |f (n + 1) - f n|
[PROOFSTEP]
rw [norm_smul, mul_comm]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
n : ℕ
⊢ ‖Finset.sum (Finset.range (n + 1)) z‖ * ‖f (n + 1) + -f n‖ ≤ b * |f (n + 1) - f n|
[PROOFSTEP]
exact mul_le_mul_of_nonneg_right (hgb _) (abs_nonneg _)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n => ∑ i in Finset.range (n + 1), f i • z i
[PROOFSTEP]
have hfa' : Monotone fun n ↦ -f n := fun _ _ hab ↦ neg_le_neg <| hfa hab
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
⊢ CauchySeq fun n => ∑ i in Finset.range (n + 1), f i • z i
[PROOFSTEP]
have hf0' : Tendsto (fun n ↦ -f n) atTop (𝓝 0) := by
  convert hf0.neg
  norm_num
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
⊢ Tendsto (fun n => -f n) atTop (𝓝 0)
[PROOFSTEP]
convert hf0.neg
[GOAL]
case h.e'_5.h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
⊢ 0 = -0
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
hf0' : Tendsto (fun n => -f n) atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ i in Finset.range (n + 1), f i • z i
[PROOFSTEP]
convert (hfa'.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0' hzb).neg
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
hf0' : Tendsto (fun n => -f n) atTop (𝓝 0)
x✝ : ℕ
⊢ ∑ i in Finset.range (x✝ + 1), f i • z i = (-fun n => ∑ i in Finset.range (n + 1), -f i • z i) x✝
[PROOFSTEP]
funext
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), ‖∑ i in Finset.range n, z i‖ ≤ b
hfa' : Monotone fun n => -f n
hf0' : Tendsto (fun n => -f n) atTop (𝓝 0)
x✝ : ℕ
⊢ ∑ i in Finset.range (x✝ + 1), f i • z i = (-fun n => ∑ i in Finset.range (n + 1), -f i • z i) x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
n : ℕ
⊢ ‖∑ i in Finset.range n, (-1) ^ i‖ ≤ 1
[PROOFSTEP]
rw [neg_one_geom_sum]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
n : ℕ
⊢ ‖if Even n then 0 else 1‖ ≤ 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
n : ℕ
h✝ : Even n
⊢ ‖0‖ ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
n : ℕ
h✝ : ¬Even n
⊢ ‖1‖ ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ i in Finset.range (n + 1), (-1) ^ i * f i
[PROOFSTEP]
simp_rw [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ x in Finset.range (n + 1), f x * (-1) ^ x
[PROOFSTEP]
exact hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ i in Finset.range (n + 1), (-1) ^ i * f i
[PROOFSTEP]
simp_rw [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n => ∑ x in Finset.range (n + 1), f x * (-1) ^ x
[PROOFSTEP]
exact hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
x : ℝ
⊢ Summable fun n => x ^ n / ↑n !
[PROOFSTEP]
have A : (0 : ℝ) < ⌊‖x‖⌋₊ + 1 := zero_lt_one.trans_le (by simp)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
x : ℝ
⊢ 1 ≤ ↑⌊‖x‖⌋₊ + 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
⊢ Summable fun n => x ^ n / ↑n !
[PROOFSTEP]
have B : ‖x‖ / (⌊‖x‖⌋₊ + 1) < 1 :=
  (div_lt_one A).2
    (Nat.lt_floor_add_one _)
      -- Then we apply the ratio test. The estimate works for `n ≥ ⌊‖x‖⌋₊`.
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
⊢ Summable fun n => x ^ n / ↑n !
[PROOFSTEP]
suffices : ∀ n ≥ ⌊‖x‖⌋₊, ‖x ^ (n + 1) / (n + 1)!‖ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
this : ∀ (n : ℕ), n ≥ ⌊‖x‖⌋₊ → ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
⊢ Summable fun n => x ^ n / ↑n !
case this
α : Type u_1
β : Type u_2
ι : Type u_3
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
⊢ ∀ (n : ℕ), n ≥ ⌊‖x‖⌋₊ → ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
[PROOFSTEP]
exact
  summable_of_ratio_norm_eventually_le B
    (eventually_atTop.2 ⟨⌊‖x‖⌋₊, this⟩)
      -- Finally, we prove the upper estimate
[GOAL]
case this
α : Type u_1
β : Type u_2
ι : Type u_3
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
⊢ ∀ (n : ℕ), n ≥ ⌊‖x‖⌋₊ → ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
[PROOFSTEP]
intro n hn
[GOAL]
case this
α : Type u_1
β : Type u_2
ι : Type u_3
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
[PROOFSTEP]
calc
  ‖x ^ (n + 1) / (n + 1)!‖ = ‖x‖ / (n + 1) * ‖x ^ n / (n !)‖ := by
    rw [_root_.pow_succ, Nat.factorial_succ, Nat.cast_mul, ← _root_.div_mul_div_comm, norm_mul, norm_div,
      Real.norm_coe_nat, Nat.cast_succ]
  _ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / (n !)‖ :=
    -- Porting note: this was `by mono* with 0 ≤ ‖x ^ n / (n !)‖, 0 ≤ ‖x‖ <;> apply norm_nonneg`
          -- but we can't wait on `mono`.mul_le_mul_of_nonneg_right
      (div_le_div (norm_nonneg x) (le_refl ‖x‖) A (add_le_add (mono_cast hn) (le_refl 1))) (norm_nonneg (x ^ n / n !))
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x ^ (n + 1) / ↑(n + 1)!‖ = ‖x‖ / (↑n + 1) * ‖x ^ n / ↑n !‖
[PROOFSTEP]
rw [_root_.pow_succ, Nat.factorial_succ, Nat.cast_mul, ← _root_.div_mul_div_comm, norm_mul, norm_div, Real.norm_coe_nat,
  Nat.cast_succ]
