awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
h_1 : Nontrivial R
this : 1 ≤ norm.{u_4} (E := R) 1
linarith : 1 - ‖x‖ < 0 → ‖x‖ - 1 + (1 - ‖x‖ - 0) = 0
⊢ 0 ≤ 1 - ‖x‖

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
h_1 : Nontrivial R
this : 1 ≤ norm.{u_4} (E := R) 1
⊢ 0 ≤ (1 - ‖x‖)⁻¹

Tactic:
have : 0 ≤ (1 - ‖x‖)⁻¹ := inv_nonneg.2 (by linarith)
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
x : R
h : ‖x‖ < 1
hx : ¬Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ x ^ n
h_1 : Nontrivial R
this_1 : 1 ≤ norm.{u_4} (E := R) 1
this : 0 ≤ (1 - ‖x‖)⁻¹
linarith :
  norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹ < 0 →
    1 - norm.{u_4} (E := R) 1 + (HMul.hMul (α := ℝ) 1 0 - 1 * (1 - ‖x‖)⁻¹) +
        (1 * norm.{u_4} (E := R) 1 - HMul.hMul (α := ℝ) 1 1 + 1 * (1 - ‖x‖)⁻¹ - HMul.hMul (α := ℝ) 1 0) =
      0
⊢ 0 ≤ norm.{u_4} (E := R) 1 - 1 + (1 - ‖x‖)⁻¹

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ (∑' (i : ℕ), x ^ i) * (1 - x) = 1

Tactic:
(summable_geometric_of_norm_lt_one h).tsum_pow_mul_one_sub

Premises used: Summable.tsum_pow_mul_one_sub, summable_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ (1 - x) * ∑' (i : ℕ), x ^ i = 1

Tactic:
(summable_geometric_of_norm_lt_one h).one_sub_mul_tsum_pow

Premises used: Summable.one_sub_mul_tsum_pow, summable_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
rw : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ (i + 1)) 1 = ∑' (i : ℕ), x ^ i
rw₁ : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ (i + 1)) 1 = HPow.hPow (β := ℕ) x 0 + ∑' (b : ℕ), x ^ (b + 1)
rw₂ : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ (i + 1)) 1 = HAdd.hAdd (α := R) 1 (∑' (b : ℕ), x ^ (b + 1))
rw₃ rw₄ : HAdd.hAdd (α := R) 1 (∑' (i : ℕ), x ^ (i + 1)) = HAdd.hAdd (α := R) 1 (∑' (b : ℕ), x ^ (b + 1))
⊢ ∑' (i : ℕ), x ^ (i + 1) = HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1

Tactic:
rw [eq_sub_iff_add_eq, (summable_geometric_of_norm_lt_one h).tsum_eq_zero_add,
    pow_zero, add_comm]

Premises used: Summable.tsum_eq_zero_add, eq_sub_iff_add_eq, add_comm, pow_zero, summable_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
simp_rw : Eq.{u_4 + 1} (α := R) (∑' (i : ℕ), x * x ^ i) (∑' (i : ℕ), x ^ (i + 1))
⊢ x * ∑' (i : ℕ), x ^ i = ∑' (i : ℕ), x ^ (i + 1)

Tactic:
simp_rw [← (summable_geometric_of_norm_lt_one h).tsum_mul_left, ← _root_.pow_succ']

Premises used: Summable.tsum_mul_left, summable_geometric_of_norm_lt_one, pow_succ'
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
rw : HMul.hMul (α := R) 1 (∑' (i : ℕ), x ^ i) + x * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
rw₁ : ∑' (i : ℕ), x ^ i + x * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
rw₂ : HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ i) (∑' (i : ℕ), x ^ (i + 1)) = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
rw₃ : ∑' (i : ℕ), x ^ i + HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1 = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1
rw₄ :
  ∑' (i : ℕ), x ^ i + HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1 =
    HAdd.hAdd (α := R) (∑' (i : ℕ), x ^ i) (∑' (i : ℕ), x ^ i) - 1
rw₅ rw₆ :
  ∑' (i : ℕ), x ^ i + HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1 =
    ∑' (i : ℕ), x ^ i + HSub.hSub (α := R) (∑' (i : ℕ), x ^ i) 1
⊢ (1 + x) * ∑' (i : ℕ), x ^ i = HMul.hMul (α := R) 2 (∑' (i : ℕ), x ^ i) - 1

Tactic:
rw [add_mul, one_mul, geom_series_mul_shift x h, geom_series_succ x h, two_mul, add_sub_assoc]

Premises used: add_sub_assoc, add_mul, geom_series_mul_shift, geom_series_succ, two_mul, one_mul
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
change : (↑(Units.oneSub x h)⁻¹ : R) = (1 - x)⁻¹ʳ
⊢ ∑' (i : ℕ), x ^ i = (1 - x)⁻¹ʳ

Tactic:
change (Units.oneSub x h)⁻¹ = (1 - x)⁻¹ʳ

Premises used: HSub.hSub, Units.oneSub, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
rw : (↑(Units.oneSub x h) : R)⁻¹ʳ = (1 - x)⁻¹ʳ
⊢ (↑(Units.oneSub x h)⁻¹ : R) = (1 - x)⁻¹ʳ

Tactic:
rw [← Ring.inverse_unit]

Premises used: Ring.inverse_unit
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ (↑(Units.oneSub x h) : R)⁻¹ʳ = (1 - x)⁻¹ʳ

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ HasSum.{u_4, 0} (α := R) (fun (n : ℕ) ↦ x ^ n) (∑' (b : ℕ), x ^ b)

Tactic:
(summable_geometric_of_norm_lt_one h).hasSum

Premises used: Summable.hasSum, summable_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
h₁ : (1 - x)⁻¹ʳ = ∑' (b : ℕ), x ^ b
⊢ HasSum (fun (i : ℕ) ↦ x ^ i) (1 - x)⁻¹ʳ

Tactic:
convert! (summable_geometric_of_norm_lt_one h).hasSum

Premises used: Summable.hasSum, summable_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ (1 - x)⁻¹ʳ = ∑' (b : ℕ), x ^ b

Tactic:
(geom_series_eq_inverse x h).symm

Premises used: Eq.symm, geom_series_eq_inverse
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ (1 - x)⁻¹ʳ = ∑' (b : ℕ), x ^ b

Tactic:
exact (geom_series_eq_inverse x h).symm

Premises used: Eq.symm, geom_series_eq_inverse
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ IsUnit (1 - x)

Tactic:
⟨Units.oneSub x h, rfl⟩

Premises used: IsUnit, Units.oneSub, Exists.intro, rfl
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
contrapose! : ∀ (h : ξ = 1), 1 ≤ ‖ξ‖
⊢ ξ ≠ 1

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : ξ = 1
⊢ 1 ≤ ‖ξ‖

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
⊢ ξ ≠ 1

Tactic:
have xi_ne_one : ξ ≠ 1 := by
    contrapose! h
    simp [h]
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
⊢ Tendsto (fun (n : ℕ) ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 (HSub.hSub (α := K) 0 1 * (ξ - 1)⁻¹))

Tactic:
have A : Tendsto (fun n ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹)) :=
    ((tendsto_pow_atTop_nhds_zero_of_norm_lt_one h).sub tendsto_const_nhds).mul tendsto_const_nhds
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun (n : ℕ) ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 (HSub.hSub (α := K) 0 1 * (ξ - 1)⁻¹))
rw : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, ξ ^ i) atTop (𝓝 (1 - ξ)⁻¹)
rw₁ : Summable (α := ℝ) fun (i : ℕ) ↦ ‖ξ ^ i‖
⊢ HasSum (fun (n : ℕ) ↦ ξ ^ n) (1 - ξ)⁻¹

Tactic:
rw [hasSum_iff_tendsto_nat_of_summable_norm]

Premises used: hasSum_iff_tendsto_nat_of_summable_norm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun (n : ℕ) ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 (HSub.hSub (α := K) 0 1 * (ξ - 1)⁻¹))
⊢ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, ξ ^ i) atTop (𝓝 (1 - ξ)⁻¹)

Tactic:
simpa [geom_sum_eq, xi_ne_one, neg_inv, div_eq_mul_inv] using A

Premises used: geom_sum_eq, div_eq_mul_inv, neg_inv
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun (n : ℕ) ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 (HSub.hSub (α := K) 0 1 * (ξ - 1)⁻¹))
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖ξ ^ i‖

Tactic:
simp [norm_pow, summable_geometric_of_lt_one (norm_nonneg _) h]

Premises used: norm_pow, summable_geometric_of_lt_one, norm_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : Field R
inst_1 : Field S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : TopologicalSpace S
inst_4 : IsStrictOrderedRing S
inst_5 : Archimedean S
_i : OrderTopology S
K : Type u_4
inst_6 : NormedDivisionRing K
ξ : K
⊢ HasSummableGeomSeries K

Tactic:
⟨fun _ h ↦ (hasSum_geometric_of_norm_lt_one h).summable⟩

Premises used: hasSum_geometric_of_norm_lt_one, HasSummableGeomSeries.mk, HasSum.summable
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
⊢ ∑' (n : ℕ), ξ ^ n = (1 - ξ)⁻¹

Tactic:
(hasSum_geometric_of_norm_lt_one h).tsum_eq

Premises used: hasSum_geometric_of_norm_lt_one, HasSum.tsum_eq
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
r : ℝ
h : |r| < 1
⊢ HasSum (fun (n : ℕ) ↦ r ^ n) (1 - r)⁻¹

Tactic:
hasSum_geometric_of_norm_lt_one h

Premises used: hasSum_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
r : ℝ
h : |r| < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ r ^ n

Tactic:
summable_geometric_of_norm_lt_one h

Premises used: summable_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
r : ℝ
h : |r| < 1
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
tsum_geometric_of_norm_lt_one h

Premises used: tsum_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
⊢ (Summable.{u_4, 0} (α := K) fun (n : ℕ) ↦ ξ ^ n) ↔ ‖ξ‖ < 1

Tactic:
⟨fun h ↦ ?_, summable_geometric_of_norm_lt_one⟩

Premises used: Iff.intro, summable_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
refine : ∀ (h : Summable.{u_4, 0} (α := K) fun (n : ℕ) ↦ ξ ^ n), ‖ξ‖ < 1
⊢ (Summable.{u_4, 0} (α := K) fun (n : ℕ) ↦ ξ ^ n) ↔ ‖ξ‖ < 1

Tactic:
refine ⟨fun h ↦ ?_, summable_geometric_of_norm_lt_one⟩
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : Summable.{u_4, 0} (α := K) fun (n : ℕ) ↦ ξ ^ n
obtain : ∀ (k : ℕ) (hk : dist (ξ ^ k) 0 < 1), ‖ξ‖ < 1
⊢ ‖ξ‖ < 1

Tactic:
obtain ⟨k : ℕ, hk : dist (ξ ^ k) 0 < 1⟩ :=
    (h.tendsto_cofinite_zero.eventually (ball_mem_nhds _ zero_lt_one)).exists

Premises used: Filter.Eventually.exists, Metric.ball_mem_nhds, zero_lt_one, Summable.tendsto_cofinite_zero, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : Summable.{u_4, 0} (α := K) fun (n : ℕ) ↦ ξ ^ n
k : ℕ
hk : dist (ξ ^ k) 0 < 1
⊢ ‖ξ‖ ^ k < 1

Tactic:
simp only [norm_pow, dist_zero_right] at hk

Premises used: norm_pow, dist_zero_right
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : Summable.{u_4, 0} (α := K) fun (n : ℕ) ↦ ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1
⊢ ‖ξ‖ ^ k < HPow.hPow (α := ℝ) 1 k

Tactic:
rw [← one_pow k] at hk

Premises used: one_pow
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : Summable.{u_4, 0} (α := K) fun (n : ℕ) ↦ ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < HPow.hPow (α := ℝ) 1 k
⊢ ‖ξ‖ < 1

Tactic:
lt_of_pow_lt_pow_left₀ _ zero_le_one hk

Premises used: lt_of_pow_lt_pow_left₀, zero_le_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
K : Type u_4
inst : NormedDivisionRing K
ξ : K
h : Summable.{u_4, 0} (α := K) fun (n : ℕ) ↦ ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < HPow.hPow (α := ℝ) 1 k
⊢ ‖ξ‖ < 1

Tactic:
exact lt_of_pow_lt_pow_left₀ _ zero_le_one hk

Premises used: lt_of_pow_lt_pow_left₀, zero_le_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
rcases : ∀ (r' : ℝ) (hrr' : ‖r‖ < r') (h : r' < 1), Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖

Tactic:
rcases exists_between hr with ⟨r', hrr', h⟩

Premises used: exists_between
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ ‖‖r‖‖ < r'

Tactic:
rw [← norm_norm] at hrr'

Premises used: norm_norm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
hrr'₁ : ‖‖r‖‖ < r'
⊢ r' < 1

Tactic:
rw [← norm_norm] at hrr'

Premises used: norm_norm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
apply : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖) fun (n : ℕ) ↦ r' ^ n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖

Tactic:
apply summable_of_isBigO_nat (summable_geometric_of_lt_one ((norm_nonneg _).trans hrr'.le) h)

Premises used: LT.lt.le, LE.le.trans, summable_geometric_of_lt_one, norm_nonneg, summable_of_isBigO_nat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
apply : ∀ᶠ (x : ℕ) in atTop, ‖‖(↑(u x) : R) * r ^ x‖‖ ≤ norm.{u_4} (E := R) 1 * ‖(↑(u x) : ℝ) * ‖r‖ ^ x‖
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖) fun (n : ℕ) ↦ (↑(u n) : ℝ) * ‖r‖ ^ n

Tactic:
apply (IsBigOWith.of_bound (c := ‖(1 : R)‖) ?_).isBigO

Premises used: Asymptotics.IsBigOWith.isBigO, Asymptotics.IsBigOWith.of_bound
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
h₁ : ∀ (n : ℕ) (hn : ‖r ^ n‖ ≤ ‖r‖ ^ n), ‖‖(↑(u n) : R) * r ^ n‖‖ ≤ norm.{u_4} (E := R) 1 * ‖(↑(u n) : ℝ) * ‖r‖ ^ n‖
⊢ ∀ᶠ (x : ℕ) in atTop, ‖‖(↑(u x) : R) * r ^ x‖‖ ≤ norm.{u_4} (E := R) 1 * ‖(↑(u x) : ℝ) * ‖r‖ ^ x‖

Tactic:
filter_upwards [eventually_norm_pow_le r] with n hn

Premises used: eventually_norm_pow_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
h₁ : ‖(↑(u n) : R) * r ^ n‖ ≤ norm.{u_4} (E := R) 1 * ((↑(u n) : ℝ) * ‖r‖ ^ n)
⊢ ‖‖(↑(u n) : R) * r ^ n‖‖ ≤ norm.{u_4} (E := R) 1 * ‖(↑(u n) : ℝ) * ‖r‖ ^ n‖

Tactic:
simp only [norm_mul, Real.norm_eq_abs, abs_cast, norm_pow, abs_norm]

Premises used: norm_pow, Nat.abs_cast, norm_mul, abs_norm, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
h₁ : norm.{u_4} (E := R) (↑(u n) : R) * ‖r ^ n‖ ≤ norm.{u_4} (E := R) 1 * ((↑(u n) : ℝ) * ‖r‖ ^ n)
⊢ ‖(↑(u n) : R) * r ^ n‖ ≤ norm.{u_4} (E := R) 1 * ((↑(u n) : ℝ) * ‖r‖ ^ n)

Tactic:
apply (norm_mul_le _ _).trans

Premises used: LE.le.trans, norm_mul_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
h₁ : norm.{u_4} (E := R) (↑(u n) : R) ≤ (↑(u n) : ℝ) * norm.{u_4} (E := R) 1
⊢ norm.{u_4} (E := R) (↑(u n) : R) * ‖r ^ n‖ ≤ (↑(u n) : ℝ) * norm.{u_4} (E := R) 1 * ‖r‖ ^ n

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ norm.{u_4} (E := R) (↑(u n) : R) ≤ (↑(u n) : ℝ) * norm.{u_4} (E := R) 1

Tactic:
norm_cast_le (u n)

Premises used: Nat.norm_cast_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ norm.{u_4} (E := R) (↑(u n) : R) ≤ (↑(u n) : ℝ) * norm.{u_4} (E := R) 1

Tactic:
exact norm_cast_le (u n)

Premises used: Nat.norm_cast_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ norm.{u_4} (E := R) (↑(u n) : R) * ‖r ^ n‖ ≤ (↑(u n) : ℝ) * norm.{u_4} (E := R) 1 * ‖r‖ ^ n

Tactic:
have : ‖(u n : R)‖ * ‖r ^ n‖ ≤ (u n * ‖(1 : R)‖) * ‖r‖ ^ n := by
        gcongr; exact norm_cast_le (u n)
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
this : norm.{u_4} (E := R) (↑(u n) : R) * ‖r ^ n‖ ≤ (↑(u n) : ℝ) * norm.{u_4} (E := R) 1 * ‖r‖ ^ n
⊢ (↑(u n) : ℝ) * norm.{u_4} (E := R) 1 * ‖r‖ ^ n = norm.{u_4} (E := R) 1 * ((↑(u n) : ℝ) * ‖r‖ ^ n)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
this : norm.{u_4} (E := R) (↑(u n) : R) * ‖r ^ n‖ ≤ (↑(u n) : ℝ) * norm.{u_4} (E := R) 1 * ‖r‖ ^ n
⊢ norm.{u_4} (E := R) (↑(u n) : R) * ‖r ^ n‖ ≤ norm.{u_4} (E := R) 1 * ((↑(u n) : ℝ) * ‖r‖ ^ n)

Tactic:
exact this.trans (le_of_eq (by ring))

Premises used: LE.le.trans, le_of_eq
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ) * ‖r‖ ^ n) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ) * ‖r‖ ^ n

Tactic:
hu.mul (isBigO_refl _ _)

Premises used: Asymptotics.IsBigO.mul, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
simp : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * ‖r‖ ^ n) fun (n : ℕ) ↦ r' ^ n
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(n ^ k) : ℝ) * ‖r‖ ^ n) fun (n : ℕ) ↦ r' ^ n

Tactic:
simp only [cast_pow]

Premises used: Nat.cast_pow
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * ‖r‖ ^ n) fun (n : ℕ) ↦ r' ^ n

Tactic:
(isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO

Premises used: Asymptotics.IsLittleO.isBigO, isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * ‖r‖ ^ n) fun (n : ℕ) ↦ r' ^ n

Tactic:
exact (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO

Premises used: Asymptotics.IsLittleO.isBigO, isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(u n) : ℝ)) fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
fun : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖) fun (n : ℕ) ↦ (↑(u n) : ℝ) * ‖r‖ ^ n
fun₁ : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ (↑(n ^ k) : ℝ) * ‖r‖ ^ n) fun (n : ℕ) ↦ r' ^ n
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖(↑(u n) : R) * r ^ n‖) fun (n : ℕ) ↦ r' ^ n

Tactic:
calc
  fun n ↦ ‖↑(u n) * r ^ n‖
  _ =O[atTop] fun n ↦ u n * ‖r‖ ^ n := by
      apply (IsBigOWith.of_bound (c := ‖(1 : R)‖) ?_).isBigO
      filter_upwards [eventually_norm_pow_le r] with n hn
      simp only [norm_mul, Real.norm_eq_abs, abs_cast, norm_pow, abs_norm]
      apply (norm_mul_le _ _).trans
      have : ‖(u n : R)‖ * ‖r ^ n‖ ≤ (u n * ‖(1 : R)‖) * ‖r‖ ^ n := by
        gcongr; exact norm_cast_le (u n)
      exact this.trans (le_of_eq (by ring))
  _ =O[atTop] fun n ↦ ↑(n ^ k) * ‖r‖ ^ n := hu.mul (isBigO_refl _ _)
  _ =O[atTop] fun n ↦ r' ^ n := by
      simp only [cast_pow]
      exact (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO

Premises used: Norm.norm, HMul.hMul, Asymptotics.IsBigO.mul, Nat.cast, Filter.atTop, HPow.hPow, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
simp : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑(n ^ k) : R) * r ^ n‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖HPow.hPow (α := R) (↑n : R) k * r ^ n‖

Tactic:
simp only [← cast_pow]

Premises used: Nat.cast_pow
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑(n ^ k) : R) * r ^ n‖

Tactic:
summable_norm_mul_geometric_of_norm_lt_one (k := k) (u := fun n ↦ n ^ k) hr
    (isBigO_refl _ _)

Premises used: summable_norm_mul_geometric_of_norm_lt_one, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑(n ^ k) : R) * r ^ n‖

Tactic:
exact summable_norm_mul_geometric_of_norm_lt_one (k := k) (u := fun n ↦ n ^ k) hr
    (isBigO_refl _ _)

Premises used: summable_norm_mul_geometric_of_norm_lt_one, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
r : R
hr : ‖r‖ < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖r ^ n‖

Tactic:
simpa using summable_norm_pow_mul_geometric_of_norm_lt_one 0 hr

Premises used: summable_norm_pow_mul_geometric_of_norm_lt_one, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ (↑((n + 0).choose 0) : R) * r ^ n) ((1 - r)⁻¹ʳ ^ HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simpa using hasSum_geom_series_inverse r hr

Premises used: hasSum_geom_series_inverse