awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
⊢ (if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re) ≤
    if n = 0 then 0 else ‖g n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have isTrue : n = 0 → LE.le (α := ℝ) 0 0
Tactic: split
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
isTrue : n = 0 → LE.le (α := ℝ) 0 0
⊢ (if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re) ≤
    if n = 0 then 0 else ‖g n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have isFalse : ¬n = 0 → ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re ≤ ‖g n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: split
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
n : ℕ
h : ‖f n‖ ≤ ‖g n‖
h_1 : ¬n = 0
⊢ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re ≤ ‖g n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have isFalse : 0 ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
⊢ ‖term f s' n‖ ≤ ‖term f s n‖
have simp : (if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s'.re) ≤
  if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: simp only [norm_term_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
⊢ (if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s'.re) ≤
    if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have split : n = 0 → LE.le (α := ℝ) 0 0
Tactic: split
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
split : n = 0 → LE.le (α := ℝ) 0 0
⊢ (if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s'.re) ≤
    if n = 0 then 0 else ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have isFalse : ¬n = 0 → ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s'.re ≤ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: split
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
hn : ¬n = 0
⊢ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s'.re ≤ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have hdb : LE.le (α := ℝ) 1 (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
⊢ 0 ≤ if n = 0 then 0 else a n / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)
have pos : ∀ (hn : n = 0), LE.le (α := ℂ) 0 0
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
pos : ∀ (hn : n = 0), LE.le (α := ℂ) 0 0
⊢ 0 ≤ if n = 0 then 0 else a n / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)
have neg : ∀ (hn : ¬n = 0), 0 ≤ a n / HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (hypothesis)
Goal:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[atTop] g
hf : LSeriesSummable f s
⊢ LSeriesSummable g s
have h₁ : f =ᶠ[cofinite] g
Tactic: rw [← Nat.cofinite_eq_atTop] at h
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
⊢ LSeriesSummable g s
have refine : ∀ᶠ (i : ℕ) in cofinite, ‖term g s i‖ ≤ ‖term f s i‖
Tactic: refine (summable_norm_iff.mpr hf).of_norm_bounded_eventually ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
⊢ term f s =ᶠ[cofinite] term g s
have rw : ∀ (h : ∃ (s : Set ℕ), Membership.mem (γ := Filter ℕ) cofinite s ∧ Set.EqOn f g s) (hf : LSeriesSummable f s),
  ∃ (s_1 : Set ℕ), Membership.mem (γ := Filter ℕ) cofinite s_1 ∧ Set.EqOn (term f s) (term g s) s_1
Tactic: rw [eventuallyEq_iff_exists_mem] at h ⊢
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
h : ∃ (s : Set ℕ), Membership.mem (γ := Filter ℕ) cofinite s ∧ Set.EqOn f g s
hf : LSeriesSummable f s
⊢ ∃ (s_1 : Set ℕ), Membership.mem (γ := Filter ℕ) cofinite s_1 ∧ Set.EqOn (term f s) (term g s) s_1
have obtain : ∀ (S : Set ℕ) (hS : Membership.mem (γ := Filter ℕ) cofinite S) (hS' : Set.EqOn f g S),
  ∃ (s_1 : Set ℕ), Membership.mem (γ := Filter ℕ) cofinite s_1 ∧ Set.EqOn (term f s) (term g s) s_1
Tactic: obtain ⟨S, hS, hS'⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
S : Set ℕ
hS : Membership.mem (γ := Filter ℕ) cofinite S
hS' : Set.EqOn f g S
⊢ ∃ (s_1 : Set ℕ), Membership.mem (γ := Filter ℕ) cofinite s_1 ∧ Set.EqOn (term f s) (term g s) s_1
have refine : ∀ (n : ℕ) (hn : n ∈ S \ {0}), term f s n = term g s n
Tactic: refine ⟨S \ {0}, diff_mem hS <| (Set.finite_singleton 0).compl_mem_cofinite, fun n hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (hypothesis)
Goal:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
S : Set ℕ
hS : Membership.mem (γ := Filter ℕ) cofinite S
hS' : Set.EqOn f g S
n : ℕ
hn : n ∈ S \ {0}
⊢ term f s n = term g s n
have hn₁ : n ∈ S ∧ ¬n = 0
Tactic: rw [Set.mem_diff, Set.mem_singleton_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (hypothesis)
Goal:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖term g s i‖ ≤ ‖term f s i‖
have this : term f s =ᶠ[cofinite] term g s
Tactic: have : term f s =ᶠ[cofinite] term g s := by
    rw [eventuallyEq_iff_exists_mem] at h ⊢
    obtain ⟨S, hS, hS'⟩ := h
    refine ⟨S \ {0}, diff_mem hS <| (Set.finite_singleton 0).compl_mem_cofinite, fun n hn ↦ ?_⟩
    rw [Set.mem_diff, Set.mem_singleton_iff] at hn
    simp [hn.2, hS' hn.1]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
hf : LSeriesSummable f s
⊢ LSeriesSummable f s'
have rw : ∀ (hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖), Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s' x‖
Tactic: rw [LSeriesSummable, ← summable_norm_iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
⊢ LSeries 0 = 0
have h : ∀ (x : ℂ), LSeries 0 x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
s : ℂ
n : ℕ
⊢ term δ s n = if n = 1 then 1 else 0
have inl : term δ s 0 = if Eq (α := ℕ) 0 1 then 1 else 0
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
s : ℂ
n : ℕ
inl : term δ s 0 = if Eq (α := ℕ) 0 1 then 1 else 0
⊢ term δ s n = if n = 1 then 1 else 0
have inr : ∀ (hn : n ≠ 0), term δ s n = if n = 1 then 1 else 0
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term δ s n = if n = 1 then 1 else 0
have inr : ∀ (hn' : n = 1), term δ s n = if n = 1 then 1 else 0
Tactic: rcases eq_or_ne n 1 with hn' | hn'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
inr : ∀ (hn' : n = 1), term δ s n = if n = 1 then 1 else 0
⊢ term δ s n = if n = 1 then 1 else 0
have inr₁ : ∀ (hn' : n ≠ 1), term δ s n = if n = 1 then 1 else 0
Tactic: rcases eq_or_ne n 1 with hn' | hn'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
⊢ f * δ = f 1 • δ
have h : ∀ (n : ℕ), (f * δ) n = (f 1 • δ) n
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
n : ℕ
⊢ (f * δ) n = (f 1 • δ) n
have pos : ∀ (hn : n = 1), (f * δ) n = (f 1 • δ) n
Tactic: by_cases hn : n = 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
n : ℕ
pos : ∀ (hn : n = 1), (f * δ) n = (f 1 • δ) n
⊢ (f * δ) n = (f 1 • δ) n
have neg : ∀ (hn : ¬n = 1), (f * δ) n = (f 1 • δ) n
Tactic: by_cases hn : n = 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
h : f 1 = 1
⊢ f * δ = δ
have rw : f 1 • δ = δ
Tactic: rw [mul_delta_eq_smul_delta, h, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
h : f 1 = 1
rw : f 1 • δ = δ
⊢ f * δ = δ
have rw₁ : HSMul.hSMul (α := ℂ) 1 δ = δ
Tactic: rw [mul_delta_eq_smul_delta, h, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
h : f 1 = 1
rw : f 1 • δ = δ
rw₁ : HSMul.hSMul (α := ℂ) 1 δ = δ
⊢ f * δ = δ
have rw₂ : δ = δ
Tactic: rw [mul_delta_eq_smul_delta, h, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
⊢ L δ = 1
have h : ∀ (x : ℂ), L δ x = 1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (hypothesis)
Goal:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have h₁ : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖
Tactic: replace h := h.norm
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
s : ℂ
h : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖
⊢ ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have h₁ : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ (∑' (n : ℕ), ‖term f s n‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: use tsum fun n ↦ ‖term f s n‖
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
s : ℂ
h : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖
⊢ ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ (∑' (n : ℕ), ‖term f s n‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have h₁ : ∀ (n : ℕ) (hn₀ : n ≠ 0) (hn : (∑' (n : ℕ), ‖term f s n‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re < ‖f n‖), False
Tactic: by_contra! ⟨n, hn₀, hn⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (hypothesis)
Goal:
f : ℕ → ℂ
s : ℂ
h : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re < ‖f n‖
⊢ False
have this : ‖term f s n‖ ≤ ∑' (i : ℕ), ‖term f s i‖
Tactic: have := h.le_tsum n fun _ _ ↦ norm_nonneg _
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (hypothesis)
Goal:
f : ℕ → ℂ
s : ℂ
h : Summable (α := ℝ) fun (x : ℕ) ↦ ‖term f s x‖
n : ℕ
hn₀ : n ≠ 0
hn : (∑' (n : ℕ), ‖term f s n‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re < ‖f n‖
this : ‖term f s n‖ ≤ ∑' (i : ℕ), ‖term f s i‖
⊢ False
have this₁ : ‖f n‖ ≤ (∑' (i : ℕ), ‖term f s i‖) * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: rw [norm_term_eq, if_neg hn₀,
    div_le_iff₀ <| Real.rpow_pos_of_pos (Nat.cast_pos.mpr <| Nat.pos_of_ne_zero hn₀) _] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have obtain : ∀ (C : ℝ) (hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) s.re),
  Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: obtain ⟨C, hC⟩ := h.le_const_mul_rpow
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have refine : ∀ (n : ℕ) (hn : n ≥ 1), ‖f n‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) s.re‖
Tactic: refine Asymptotics.IsBigO.of_bound C <| eventually_atTop.mpr ⟨1, fun n hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
n : ℕ
hn : n ≥ 1
⊢ ‖f n‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑n : ℝ) s.re‖
have h₁ : ‖HPow.hPow (α := ℝ) (↑n : ℝ) s.re‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: convert! hC n (Nat.pos_iff_ne_zero.mp hn) using 2
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
n : ℕ
hn : n ≥ 1
⊢ ‖HPow.hPow (α := ℝ) (↑n : ℝ) s.re‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have h₁ : |HPow.hPow (α := ℝ) (↑n : ℝ) s.re| = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: rw [Real.norm_eq_abs, Real.abs_rpow_of_nonneg n.cast_nonneg, abs_of_nonneg n.cast_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
n : ℕ
hn : n ≥ 1
h₁ : |HPow.hPow (α := ℝ) (↑n : ℝ) s.re| = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ ‖HPow.hPow (α := ℝ) (↑n : ℝ) s.re‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have h₂ : HPow.hPow (α := ℝ) |(↑n : ℝ)| s.re = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: rw [Real.norm_eq_abs, Real.abs_rpow_of_nonneg n.cast_nonneg, abs_of_nonneg n.cast_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) s.re
n : ℕ
hn : n ≥ 1
h₁ : |HPow.hPow (α := ℝ) (↑n : ℝ) s.re| = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
h₂ : HPow.hPow (α := ℝ) |(↑n : ℝ)| s.re = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ ‖HPow.hPow (α := ℝ) (↑n : ℝ) s.re‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have h₃ : HPow.hPow (α := ℝ) (↑n : ℝ) s.re = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: rw [Real.norm_eq_abs, Real.abs_rpow_of_nonneg n.cast_nonneg, abs_of_nonneg n.cast_nonneg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
⊢ LSeriesSummable f s
have obtain : ∀ (C : ℝ) (hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)), LSeriesSummable f s
Tactic: obtain ⟨C, hC⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (hypothesis)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
⊢ LSeriesSummable f s
have hC₀ : 0 ≤ C
Tactic: have hC₀ : 0 ≤ C := (norm_nonneg <| f 1).trans <| by simpa using hC 1 one_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
have simp_rw : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ)‖ * ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-(s + (1 - (↑x : ℂ))))‖
Tactic: simp_rw [div_eq_mul_inv, norm_mul, ← cpow_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
⊢ -s.re + x - 1 < -1
have linarith : -1 ≤ -s.re + x - 1 → -1 - (-s.re + x - 1) + (x - s.re) = 0
Tactic: linarith only [hs]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (hypothesis)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ)‖ * ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-(s + (1 - (↑x : ℂ))))‖
have hsx : -s.re + x - 1 < -1
Tactic: have hsx : -s.re + x - 1 < -1 := by linarith only [hs]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ)‖ * ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-(s + (1 - (↑x : ℂ))))‖
have refine_1 : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re + x - 1)
Tactic: refine Summable.mul_left _ <|
      Summable.of_norm_bounded_eventually_nat (g := fun n ↦ (n : ℝ) ^ (-s.re + x - 1)) ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
refine_1 : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re + x - 1)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ)‖ * ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-(s + (1 - (↑x : ℂ))))‖
have refine_2 : ∀ᶠ (i : ℕ) in Filter.atTop,
  ‖‖HPow.hPow (α := ℂ) (↑i : ℂ) (-(s + (1 - (↑x : ℂ))))‖‖ ≤
    (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re + x - 1)) i
Tactic: refine Summable.mul_left _ <|
      Summable.of_norm_bounded_eventually_nat (g := fun n ↦ (n : ℝ) ^ (-s.re + x - 1)) ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ ∀ᶠ (i : ℕ) in Filter.atTop,
    ‖‖HPow.hPow (α := ℂ) (↑i : ℂ) (-(s + (1 - (↑x : ℂ))))‖‖ ≤
      (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re + x - 1)) i
have refine_2 : ∃ (a : ℕ), ∀ b ≥ a, ‖HPow.hPow (α := ℂ) (↑b : ℂ) (-(s + (1 - (↑x : ℂ))))‖ ≤ HPow.hPow (α := ℝ) (↑b : ℝ) (-s.re + x - 1)
Tactic: simp only [norm_norm, Filter.eventually_atTop]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
⊢ ∃ (a : ℕ),
    ∀ b ≥ a, ‖HPow.hPow (α := ℂ) (↑b : ℂ) (-(s + (1 - (↑x : ℂ))))‖ ≤ HPow.hPow (α := ℝ) (↑b : ℝ) (-s.re + x - 1)
have refine_2 : ∀ (n : ℕ) (hn : n ≥ 1),
  ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-(s + (1 - (↑x : ℂ))))‖ = HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re + x - 1)
Tactic: refine ⟨1, fun n hn ↦ le_of_eq ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsx : -s.re + x - 1 < -1
n : ℕ
hn : n ≥ 1
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) (-(s + (1 - (↑x : ℂ))))‖ = HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re + x - 1)
have refine_2 : HPow.hPow (α := ℝ) (↑n : ℝ) (-(s.re + (1 - x))) = HPow.hPow (α := ℝ) (↑n : ℝ) (-s.re + x - 1)
Tactic: simp only [norm_natCast_cpow_of_pos hn, add_re, sub_re, neg_re, ofReal_re, one_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (hypothesis)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
⊢ LSeriesSummable f s
have hsum : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
Tactic: have hsum : Summable fun n : ℕ ↦ ‖(C : ℂ) / n ^ (s + (1 - x))‖ := by
    simp_rw [div_eq_mul_inv, norm_mul, ← cpow_neg]
    have hsx : -s.re + x - 1 < -1 := by linarith only [hs]
    refine Summable.mul_left _ <|
      Summable.of_norm_bounded_eventually_nat (g := fun n ↦ (n : ℝ) ^ (-s.re + x - 1)) ?_ ?_
    · simpa
    · simp only [norm_norm, Filter.eventually_atTop]
      refine ⟨1, fun n hn ↦ le_of_eq ?_⟩
      simp only [norm_natCast_cpow_of_pos hn, add_re, sub_re, neg_re, ofReal_re, one_re]
      ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsum : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
⊢ LSeriesSummable f s
have refine : ∀ (n : ℕ), ‖term f s n‖ ≤ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
Tactic: refine Summable.of_norm <| hsum.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsum : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
n : ℕ
⊢ ‖term f s n‖ ≤ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
have inl : ‖term f s 0‖ ≤ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑0 : ℂ) (s + (1 - (↑x : ℂ)))‖
Tactic: rcases n.eq_zero_or_pos with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsum : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
n : ℕ
inl : ‖term f s 0‖ ≤ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑0 : ℂ) (s + (1 - (↑x : ℂ)))‖
⊢ ‖term f s n‖ ≤ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
have inr : ∀ (hn : n > 0), ‖term f s n‖ ≤ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
Tactic: rcases n.eq_zero_or_pos with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (hypothesis)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsum : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
n : ℕ
hn : n > 0
⊢ ‖term f s n‖ ≤ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
have hn' : 0 < HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: have hn' : 0 < (n : ℝ) ^ s.re := Real.rpow_pos_of_pos (Nat.cast_pos.mpr hn) _
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
hC₀ : 0 ≤ C
hsum : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
n : ℕ
hn : n > 0
hn' : 0 < HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ ‖term f s n‖ ≤ ‖(↑C : ℂ) / HPow.hPow (α := ℂ) (↑n : ℂ) (s + (1 - (↑x : ℂ)))‖
have inr : ‖f n‖ ≤ C * HPow.hPow (α := ℝ) (↑n : ℝ) (-(s + (1 - (↑x : ℂ))).re + s.re)
Tactic: simp_rw [term_of_ne_zero hn.ne', norm_div, norm_natCast_cpow_of_pos hn, div_le_iff₀ hn',
    norm_real, Real.norm_of_nonneg hC₀, div_eq_mul_inv, mul_assoc,
    ← Real.rpow_neg <| Nat.cast_nonneg _, ← Real.rpow_add <| Nat.cast_pos.mpr hn]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
⊢ LSeriesSummable f s
have obtain : ∀ (C : ℝ) (hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖), LSeriesSummable f s
Tactic: obtain ⟨C, hC⟩ := Asymptotics.isBigO_iff.mp h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (goal)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
⊢ LSeriesSummable f s
have obtain : ∀ (m : ℕ) (hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖), LSeriesSummable f s
Tactic: obtain ⟨m, hm⟩ := eventually_atTop.mp hC
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (hypothesis)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
⊢ LSeriesSummable f s
have hC'₀ : 0 ≤ C'
Tactic: have hC'₀ : 0 ≤ C' := (le_max' _ _ (mem_insert.mpr (Or.inl rfl))).trans <| le_max_right ..
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.Basic (hypothesis)
Goal:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑x_1 : ℝ) (x - 1)‖
m : ℕ
hm : ∀ b ≥ m, ‖f b‖ ≤ C * ‖HPow.hPow (α := ℝ) (↑b : ℝ) (x - 1)‖
C' : ℝ := max C (max' (insert 0 (image (fun (n : ℕ) ↦ ‖f n‖ / HPow.hPow (α := ℝ) (↑n : ℝ) (x - 1)) (range m))) ⋯)
hC'₀ : 0 ≤ C'
⊢ LSeriesSummable f s
have hCC' : C ≤ C'
Tactic: have hCC' : C ≤ C' := le_max_left ..