awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ¬∃ (n : ℤ), (↑n : ℝ) = a
⊢ HasSum (fun (n : ℤ) ↦ if (↑n : ℝ) + a = 0 then 0 else rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - 0)
have neg : ∀ (n : ℤ), (↑n : ℝ) + a ≠ 0
Tactic: suffices ∀ (n : ℤ), n + a ≠ 0 by simpa [this] using hasSum_int_evenKernel a ht
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ¬∃ (n : ℤ), (↑n : ℝ) = a
⊢ ∀ (n : ℤ), (↑n : ℝ) + a ≠ 0
have neg : ∀ (h : ∃ (n : ℤ), (↑n : ℝ) + a = 0), ∃ (n : ℤ), (↑n : ℝ) = a
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ (n : ℤ), (↑n : ℝ) + a = 0
⊢ ∃ (n : ℤ), (↑n : ℝ) = a
have neg : ∀ (n : ℤ) (hn : (↑n : ℝ) + a = 0), ∃ (n : ℤ), (↑n : ℝ) = a
Tactic: let ⟨n, hn⟩ := h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
⊢ HasSum
    (fun (n : ℕ) ↦
      2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
        rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 2 * t))
    (cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - 1)
have rw : HasSum
  (fun (x : ℕ) ↦
    (↑(2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) *
          rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) 2 * t)) :
      ℂ))
  ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
Tactic: rw [← hasSum_ofReal, ofReal_sub, ofReal_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a t : ℝ
ht : 0 < t
⊢ HasSum
    (fun (x : ℕ) ↦
      (↑(2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) *
            rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) 2 * t)) :
        ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
have this : HasSum
  (fun (n : ℕ) ↦
    cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
  ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) +
    cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2 * t)) : ℂ))
Tactic: have := (hasSum_int_cosKernel a ht).nat_add_neg
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑n : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 * t)) : ℂ) +
        cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑n : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) +
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2 * t)) : ℂ))
⊢ HasSum
    (fun (x : ℕ) ↦
      (↑(2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) *
            rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) 2 * t)) :
        ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
have this₁ : HasSum
  (fun (n : ℕ) ↦
    cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑(n + 1) : ℤ) : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑(n + 1) : ℤ) : ℝ) 2 * t)) : ℂ) +
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑(n + 1) : ℤ)) : ℂ)) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑(n + 1) : ℤ)) : ℝ) 2 * t)) : ℂ))
  ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) +
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) * (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2 * t)) : ℂ) -
    ∑ i ∈ Finset.range 1,
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑i : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑i : ℤ) : ℝ) 2 * t)) : ℂ) +
        cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑i : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑i : ℤ)) : ℝ) 2 * t)) : ℂ)))
Tactic: rw [← hasSum_nat_add_iff' 1] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (hypothesis)
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑(n + 1) : ℤ) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑(n + 1) : ℤ) : ℝ) 2 * t)) : ℂ) +
        cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑(n + 1) : ℤ)) : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑(n + 1) : ℤ)) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) +
        cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑0 : ℂ)) *
          (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2 * t)) : ℂ) -
      ∑ i ∈ Finset.range 1,
        (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(↑i : ℤ) : ℂ)) *
            (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑i : ℤ) : ℝ) 2 * t)) : ℂ) +
          cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(-(↑i : ℤ)) : ℂ)) *
            (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑i : ℤ)) : ℝ) 2 * t)) : ℂ)))
⊢ HasSum
    (fun (x : ℕ) ↦
      (↑(2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) *
            rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) 2 * t)) :
        ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
have this₁ : HasSum
  (fun (n : ℕ) ↦
    (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ))
  ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
Tactic: simp_rw [Finset.sum_range_one, Nat.cast_zero, neg_zero, Int.cast_zero, zero_pow two_ne_zero,
    mul_zero, zero_mul, Complex.exp_zero, Real.exp_zero, ofReal_one, mul_one, Int.cast_neg,
    Int.cast_natCast, neg_sq, ← add_mul, add_sub_assoc, ← sub_sub, sub_self, zero_sub,
    ← sub_eq_add_neg, mul_neg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
⊢ HasSum
    (fun (x : ℕ) ↦
      (↑(2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) *
            rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1) 2 * t)) :
        ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
have refine : ∀ (n : ℕ),
  (↑(2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
          rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 2 * t)) :
      ℂ) =
    (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ)
Tactic: refine this.congr_fun fun n ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
n : ℕ
⊢ (↑(2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
          rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 2 * t)) :
      ℂ) =
    (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
      (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ)
have push_cast : 2 * Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) *
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ)) =
  (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) +
      cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))) *
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
n : ℕ
⊢ 2 * Complex.cos (2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) *
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ)) =
    (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) +
        cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))) *
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ))
have rw : (cexp (2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * I) +
      cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * I)) *
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ)) =
  (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) +
      cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))) *
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ))
Tactic: rw [Complex.cos, mul_div_cancel₀ _ two_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
n : ℕ
⊢ (cexp (2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * I) +
        cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * I)) *
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ)) =
    (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) +
        cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))) *
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ))
have e_a : 2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * I =
  2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1
Tactic: congr 3
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun (n : ℕ) ↦
      (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)) + cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * (↑(n + 1) : ℂ)))) *
        (↑(rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1) : ℝ) 2 * t)) : ℂ))
    ((↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t) : ℂ) - 1)
n : ℕ
e_a :
  2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * I =
    2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1
⊢ (cexp (2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * I) +
        cexp (-(2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * I)) *
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ)) =
    (cexp (2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) +
        cexp (-(2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))) *
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * (↑t : ℂ))
have e_a₁ : -(2 * (↑π : ℂ) * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * I =
  -(2 * (↑π : ℂ) * I * (↑a : ℂ) * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
Tactic: congr 3
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
b : ℝ
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (x : ℝ) ↦
          evenKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x -
            if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
        fun (x : ℝ) ↦ rexp (-p * x)
have H : ∀ (p : ℝ) (hp : 0 < p)
  (hp' :
    IsBigO (E := ℝ) (F := ℝ) atTop
      (fun (t : ℝ) ↦
        HurwitzKernelBounds.F_int 0 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) t -
          if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
      fun (t : ℝ) ↦ rexp (-p * t)),
  ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (x : ℝ) ↦
          evenKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x -
            if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
        fun (x : ℝ) ↦ rexp (-p * x)
Tactic: obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub b
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
b p : ℝ
hp : 0 < p
hp' :
  IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (t : ℝ) ↦
      HurwitzKernelBounds.F_int 0 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) t -
        if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
    fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (x : ℝ) ↦
          evenKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x -
            if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
        fun (x : ℝ) ↦ rexp (-p * x)
have H : EventuallyEq (β := ℝ) atTop
  (fun (x : ℝ) ↦
    evenKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x -
      if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
  fun (t : ℝ) ↦
  HurwitzKernelBounds.F_int 0 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) t -
    if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0
Tactic: refine ⟨p, hp, (EventuallyEq.isBigO ?_).trans hp'⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
b p : ℝ
hp : 0 < p
hp' :
  IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (t : ℝ) ↦
      HurwitzKernelBounds.F_int 0 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) t -
        if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
    fun (t : ℝ) ↦ rexp (-p * t)
⊢ EventuallyEq (β := ℝ) atTop
    (fun (x : ℝ) ↦
      evenKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x -
        if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
    fun (t : ℝ) ↦
    HurwitzKernelBounds.F_int 0 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) t -
      if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0
have h : ∀ (t : ℝ) (h : 0 < t),
  (evenKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) t -
      if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0) =
    HurwitzKernelBounds.F_int 0 (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) t -
      if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0
Tactic: filter_upwards [eventually_gt_atTop 0] with t h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ evenKernel a x - if a = 0 then 1 else 0) fun (x : ℝ) ↦ rexp (-p * x)
have H : ∀ (b : ℝ),
  ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (x : ℝ) ↦
          evenKernel (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) x -
            if Eq (α := UnitAddCircle) (↑b : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
        fun (x : ℝ) ↦ rexp (-p * x)
Tactic: induction a using QuotientAddGroup.induction_on with | H b =>
  obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub b
  refine ⟨p, hp, (EventuallyEq.isBigO ?_).trans hp'⟩
  filter_upwards [eventually_gt_atTop 0] with t h
  simp [← (hasSum_int_evenKernel b h).tsum_eq, HurwitzKernelBounds.F_int, HurwitzKernelBounds.f_int]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : ℝ
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x - 1) fun (x : ℝ) ↦
        rexp (-p * x)
have H : ∀ (p : ℝ) (hp : 0 < p)
  (hp' :
    IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ HurwitzKernelBounds.F_nat 0 1 t - if Eq (α := ℝ) 1 0 then 1 else 0)
      fun (t : ℝ) ↦ rexp (-p * t)),
  ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x - 1) fun (x : ℝ) ↦
        rexp (-p * x)
Tactic: obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_nat_zero_sub zero_le_one
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a p : ℝ
hp : 0 < p
hp' :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ HurwitzKernelBounds.F_nat 0 1 t - if Eq (α := ℝ) 1 0 then 1 else 0)
    fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x - 1) fun (x : ℝ) ↦
        rexp (-p * x)
have H : ∀ᶠ (x : ℝ) in atTop,
  ‖cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x - 1‖ ≤
    2 * (HurwitzKernelBounds.F_nat 0 1 x - if Eq (α := ℝ) 1 0 then 1 else 0)
Tactic: refine ⟨p, hp, (Eventually.isBigO ?_).trans (hp'.const_mul_left 2)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a p : ℝ
hp : 0 < p
hp' :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ HurwitzKernelBounds.F_nat 0 1 t - if Eq (α := ℝ) 1 0 then 1 else 0)
    fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop,
    ‖cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x - 1‖ ≤
      2 * (HurwitzKernelBounds.F_nat 0 1 x - if Eq (α := ℝ) 1 0 then 1 else 0)
have h : ∀ (t : ℝ) (ht : 0 < t),
  ‖cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - 1‖ ≤
    2 * (HurwitzKernelBounds.F_nat 0 1 t - if Eq (α := ℝ) 1 0 then 1 else 0)
Tactic: filter_upwards [eventually_gt_atTop 0] with t ht
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a p : ℝ
hp : 0 < p
hp' :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ HurwitzKernelBounds.F_nat 0 1 t - if Eq (α := ℝ) 1 0 then 1 else 0)
    fun (t : ℝ) ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - 1‖ ≤
    2 * (HurwitzKernelBounds.F_nat 0 1 t - if Eq (α := ℝ) 1 0 then 1 else 0)
have h : Norm.norm (E := ℝ)
    (∑' (b : ℕ),
      2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑b : ℝ) 1) *
        rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑b : ℝ) 1) 2 * t)) ≤
  HMul.hMul (α := ℝ) 2 (∑' (n : ℕ), HurwitzKernelBounds.f_nat 0 1 t n)
Tactic: simp only [eq_false_intro one_ne_zero, if_false, sub_zero,
    ← (hasSum_nat_cosKernel₀ a ht).tsum_eq, HurwitzKernelBounds.F_nat]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a p : ℝ
hp : 0 < p
hp' :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ HurwitzKernelBounds.F_nat 0 1 t - if Eq (α := ℝ) 1 0 then 1 else 0)
    fun (t : ℝ) ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ Norm.norm (E := ℝ)
      (∑' (b : ℕ),
        2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑b : ℝ) 1) *
          rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑b : ℝ) 1) 2 * t)) ≤
    HMul.hMul (α := ℝ) 2 (∑' (n : ℕ), HurwitzKernelBounds.f_nat 0 1 t n)
have h : ∀ (i : ℕ),
  ‖2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑i : ℝ) 1) *
        rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1) 2 * t)‖ ≤
    2 * HurwitzKernelBounds.f_nat 0 1 t i
Tactic: apply tsum_of_norm_bounded ((HurwitzKernelBounds.summable_f_nat 0 1 ht).hasSum.mul_left 2)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a p : ℝ
hp : 0 < p
hp' :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ HurwitzKernelBounds.F_nat 0 1 t - if Eq (α := ℝ) 1 0 then 1 else 0)
    fun (t : ℝ) ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖2 * Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
        rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 2 * t)‖ ≤
    2 * HurwitzKernelBounds.f_nat 0 1 t n
have h : |Real.cos (2 * π * a * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)| *
    rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 2 * t) ≤
  rexp (-π * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 2 * t)
Tactic: rw [norm_mul, norm_mul, norm_two, mul_assoc, mul_le_mul_iff_of_pos_left two_pos,
    norm_of_nonneg (exp_pos _).le, HurwitzKernelBounds.f_nat, pow_zero, one_mul, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cosKernel a x - 1) fun (x : ℝ) ↦ rexp (-p * x)
have H : ∀ (a : ℝ),
  ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x - 1) fun (x : ℝ) ↦
        rexp (-p * x)
Tactic: induction a using QuotientAddGroup.induction_on with | H a =>
  obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_nat_zero_sub zero_le_one
  refine ⟨p, hp, (Eventually.isBigO ?_).trans (hp'.const_mul_left 2)⟩
  filter_upwards [eventually_gt_atTop 0] with t ht
  simp only [eq_false_intro one_ne_zero, if_false, sub_zero,
    ← (hasSum_nat_cosKernel₀ a ht).tsum_eq, HurwitzKernelBounds.F_nat]
  apply tsum_of_norm_bounded ((HurwitzKernelBounds.summable_f_nat 0 1 ht).hasSum.mul_left 2)
  intro n
  rw [norm_mul, norm_mul, norm_two, mul_assoc, mul_le_mul_iff_of_pos_left two_pos,
    norm_of_nonneg (exp_pos _).le, HurwitzKernelBounds.f_nat, pow_zero, one_mul, Real.norm_eq_abs]
  exact mul_le_of_le_one_left (exp_pos _).le (abs_cos_le_one _)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
r : ℝ
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ evenKernel a) x - if a = 0 then 1 else 0) fun (x : ℝ) ↦ x ^ r
have let : ∀ (v : ℝ) (hv : 0 < v)
  (hv' :
    IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ evenKernel a x - if a = 0 then 1 else 0) fun (x : ℝ) ↦ rexp (-v * x)),
  IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ evenKernel a) x - if a = 0 then 1 else 0) fun (x : ℝ) ↦ x ^ r
Tactic: let ⟨v, hv, hv'⟩ := isBigO_atTop_evenKernel_sub a
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ evenKernel a x - if a = 0 then 1 else 0) fun (x : ℝ) ↦ rexp (-v * x)
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ evenKernel a) x - if a = 0 then 1 else 0) fun (x : ℝ) ↦ x ^ r
have rw : ∀
  (hv' :
    IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) fun (x : ℝ) ↦
      rexp (-v * x)),
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖(ofReal ∘ evenKernel a) x - if a = 0 then 1 else 0‖) fun (x : ℝ) ↦
    x ^ r
Tactic: rw [← isBigO_norm_left] at hv' ⊢
Cleared hypotheses: hv'
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) fun (x : ℝ) ↦ rexp (-v * x)
| IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) fun (x : ℝ) ↦ rexp (-v * x)
have h : ∀ (x : ℝ), ‖evenKernel a x - if a = 0 then 1 else 0‖
Tactic: enter [2, x]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) fun (x : ℝ) ↦ rexp (-v * x)
x : ℝ
| ‖evenKernel a x - if a = 0 then 1 else 0‖
have h : ‖(↑(evenKernel a x) : ℂ) - if a = 0 then 1 else 0‖
Tactic: rw [← norm_real, ofReal_sub, apply_ite ((↑) : ℝ → ℂ), ofReal_one, ofReal_zero]