α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
⊢ IsCauSeq abv fun m => ∑ n in range m, f n
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
⊢ IsCauSeq abv fun m => ∑ n in range m, f n
have har1 : |r| < 1 := by rwa [abs_of_nonneg hr0]
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
⊢ ∀ (m : ℕ), Nat.succ n ≤ m → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
⊢ IsCauSeq abv fun m => ∑ n in range m, f n
refine'
  isCauSeq_series_of_abv_le_of_isCauSeq n.succ _
    (isCauSeq_geo_series_const (abv (f n.succ) * r⁻¹ ^ n.succ) har1)
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
⊢ ∀ (m : ℕ), Nat.succ n ≤ m → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
intro m hmn
case inl
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
r_zero : r = 0
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m

case inr
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
r_ne_zero : ¬r = 0
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
cases' Classical.em (r = 0) with r_zero r_ne_zero
case inr
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
r_ne_zero : ¬r = 0
k : ℕ
hk : m - Nat.succ n = k
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
case inr
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
r_ne_zero : ¬r = 0
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
generalize hk : m - n.succ = k
case inr
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
r_ne_zero : ¬r = 0
k : ℕ
hk : m - Nat.succ n = k
r_pos : 0 < r
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
case inr
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
r_ne_zero : ¬r = 0
k : ℕ
hk : m - Nat.succ n = k
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
have r_pos : 0 < r := lt_of_le_of_ne hr0 (Ne.symm r_ne_zero)
case inr
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
r_ne_zero : ¬r = 0
k : ℕ
r_pos : 0 < r
hk : m = k + Nat.succ n
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
case inr
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
r_ne_zero : ¬r = 0
k : ℕ
hk : m - Nat.succ n = k
r_pos : 0 < r
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
replace hk : m = k + n.succ := (tsub_eq_iff_eq_add_of_le hmn).1 hk
case inr.zero
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k : ℕ
r_pos : 0 < r
hk✝ : m✝ = k + Nat.succ n✝
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.zero + Nat.succ n
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m

case inr.succ
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k✝ : ℕ
r_pos : 0 < r
hk✝ : m✝ = k✝ + Nat.succ n✝
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)) →
      ∀ (m : ℕ), Nat.succ n ≤ m → m = k + Nat.succ n → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.succ k + Nat.succ n
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
case inr
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
r_ne_zero : ¬r = 0
k : ℕ
r_pos : 0 < r
hk : m = k + Nat.succ n
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
induction' k with k ih generalizing m n
no goals
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
⊢ abs' r < 1
rwa [abs_of_nonneg hr0]
case inl
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
r_zero : r = 0
m_pos : 0 < m
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
case inl
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
r_zero : r = 0
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
have m_pos := lt_of_lt_of_le (Nat.succ_pos n) hmn
case inl
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
r_zero : r = 0
m_pos : 0 < m
this : abv (f (Nat.succ (Nat.pred m))) ≤ r * abv (f (Nat.pred m))
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
case inl
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
r_zero : r = 0
m_pos : 0 < m
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
have := h m.pred (Nat.le_of_succ_le_succ (by rwa [Nat.succ_pred_eq_of_pos m_pos]))
no goals
case inl
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
r_zero : r = 0
m_pos : 0 < m
this : abv (f (Nat.succ (Nat.pred m))) ≤ r * abv (f (Nat.pred m))
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
simpa [r_zero, Nat.succ_pred_eq_of_pos m_pos, pow_succ] using this
no goals
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m : ℕ
hmn : Nat.succ n ≤ m
r_zero : r = 0
m_pos : 0 < m
⊢ Nat.succ n ≤ Nat.succ (Nat.pred m)
rwa [Nat.succ_pred_eq_of_pos m_pos]
case inr.zero.h
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k : ℕ
r_pos : 0 < r
hk✝ : m✝ = k + Nat.succ n✝
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.zero + Nat.succ n
⊢ r ^ Nat.succ n ≠ 0
case inr.zero
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k : ℕ
r_pos : 0 < r
hk✝ : m✝ = k + Nat.succ n✝
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.zero + Nat.succ n
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
rw [hk, Nat.zero_add, mul_right_comm, inv_pow _ _, ← div_eq_mul_inv, mul_div_cancel]
no goals
case inr.zero.h
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k : ℕ
r_pos : 0 < r
hk✝ : m✝ = k + Nat.succ n✝
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.zero + Nat.succ n
⊢ r ^ Nat.succ n ≠ 0
exact (ne_of_lt (pow_pos r_pos _)).symm
case inr.succ
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k✝ : ℕ
r_pos : 0 < r
hk✝ : m✝ = k✝ + Nat.succ n✝
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)) →
      ∀ (m : ℕ), Nat.succ n ≤ m → m = k + Nat.succ n → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.succ k + Nat.succ n
kn : k + Nat.succ n ≥ Nat.succ n
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
case inr.succ
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k✝ : ℕ
r_pos : 0 < r
hk✝ : m✝ = k✝ + Nat.succ n✝
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)) →
      ∀ (m : ℕ), Nat.succ n ≤ m → m = k + Nat.succ n → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.succ k + Nat.succ n
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
have kn : k + n.succ ≥ n.succ := by
  rw [← zero_add n.succ]; exact add_le_add (Nat.zero_le _) (by simp)
case inr.succ
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k✝ : ℕ
r_pos : 0 < r
hk✝ : m✝ = k✝ + Nat.succ n✝
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)) →
      ∀ (m : ℕ), Nat.succ n ≤ m → m = k + Nat.succ n → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.succ k + Nat.succ n
kn : k + Nat.succ n ≥ Nat.succ n
⊢ abv (f (Nat.succ (k + Nat.succ n))) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ (k + Nat.succ n) * r
case inr.succ
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k✝ : ℕ
r_pos : 0 < r
hk✝ : m✝ = k✝ + Nat.succ n✝
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)) →
      ∀ (m : ℕ), Nat.succ n ≤ m → m = k + Nat.succ n → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.succ k + Nat.succ n
kn : k + Nat.succ n ≥ Nat.succ n
⊢ abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
erw [hk, Nat.succ_add, pow_succ' r, ← mul_assoc]
case inr.succ
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k✝ : ℕ
r_pos : 0 < r
hk✝ : m✝ = k✝ + Nat.succ n✝
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)) →
      ∀ (m : ℕ), Nat.succ n ≤ m → m = k + Nat.succ n → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.succ k + Nat.succ n
kn : k + Nat.succ n ≥ Nat.succ n
⊢ abv (f (k + Nat.succ n)) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ (k + Nat.succ n)
case inr.succ
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k✝ : ℕ
r_pos : 0 < r
hk✝ : m✝ = k✝ + Nat.succ n✝
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)) →
      ∀ (m : ℕ), Nat.succ n ≤ m → m = k + Nat.succ n → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.succ k + Nat.succ n
kn : k + Nat.succ n ≥ Nat.succ n
⊢ abv (f (Nat.succ (k + Nat.succ n))) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ (k + Nat.succ n) * r
refine
  le_trans (by rw [mul_comm] <;> exact h _ (Nat.le_of_succ_le kn))
    (mul_le_mul_of_nonneg_right ?_ hr0)
no goals
case inr.succ
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k✝ : ℕ
r_pos : 0 < r
hk✝ : m✝ = k✝ + Nat.succ n✝
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)) →
      ∀ (m : ℕ), Nat.succ n ≤ m → m = k + Nat.succ n → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.succ k + Nat.succ n
kn : k + Nat.succ n ≥ Nat.succ n
⊢ abv (f (k + Nat.succ n)) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ (k + Nat.succ n)
exact ih _ h _ (by simp) rfl
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k✝ : ℕ
r_pos : 0 < r
hk✝ : m✝ = k✝ + Nat.succ n✝
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)) →
      ∀ (m : ℕ), Nat.succ n ≤ m → m = k + Nat.succ n → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.succ k + Nat.succ n
⊢ k + (0 + Nat.succ n) ≥ 0 + Nat.succ n
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k✝ : ℕ
r_pos : 0 < r
hk✝ : m✝ = k✝ + Nat.succ n✝
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)) →
      ∀ (m : ℕ), Nat.succ n ≤ m → m = k + Nat.succ n → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.succ k + Nat.succ n
⊢ k + Nat.succ n ≥ Nat.succ n
rw [← zero_add n.succ]
no goals
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k✝ : ℕ
r_pos : 0 < r
hk✝ : m✝ = k✝ + Nat.succ n✝
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)) →
      ∀ (m : ℕ), Nat.succ n ≤ m → m = k + Nat.succ n → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.succ k + Nat.succ n
⊢ k + (0 + Nat.succ n) ≥ 0 + Nat.succ n
exact add_le_add (Nat.zero_le _) (by simp)
no goals
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k✝ : ℕ
r_pos : 0 < r
hk✝ : m✝ = k✝ + Nat.succ n✝
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)) →
      ∀ (m : ℕ), Nat.succ n ≤ m → m = k + Nat.succ n → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.succ k + Nat.succ n
⊢ Nat.succ n ≤ 0 + Nat.succ n
simp
no goals
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k✝ : ℕ
r_pos : 0 < r
hk✝ : m✝ = k✝ + Nat.succ n✝
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)) →
      ∀ (m : ℕ), Nat.succ n ≤ m → m = k + Nat.succ n → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.succ k + Nat.succ n
kn : k + Nat.succ n ≥ Nat.succ n
⊢ abv (f (Nat.succ (k + Nat.succ n))) ≤ ?m.60360 * r
rw [mul_comm] <;> exact h _ (Nat.le_of_succ_le kn)
no goals
α : Type u_1
inst✝³ : LinearOrderedField α
inst✝² : Archimedean α
β : Type u_2
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
n✝ : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h✝ : ∀ (m : ℕ), n✝ ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
har1 : abs' r < 1
m✝ : ℕ
hmn✝ : Nat.succ n✝ ≤ m✝
r_ne_zero : ¬r = 0
k✝ : ℕ
r_pos : 0 < r
hk✝ : m✝ = k✝ + Nat.succ n✝
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)) →
      ∀ (m : ℕ), Nat.succ n ≤ m → m = k + Nat.succ n → abv (f m) ≤ abv (f (Nat.succ n)) * r⁻¹ ^ Nat.succ n * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f (Nat.succ m)) ≤ r * abv (f m)
m : ℕ
hmn : Nat.succ n ≤ m
hk : m = Nat.succ k + Nat.succ n
kn : k + Nat.succ n ≥ Nat.succ n
⊢ Nat.succ n ≤ k + Nat.succ n
simp