-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- The function `cosKernel a - 1` has exponential decay at `+∞`, for any `a`. -/
lemma isBigO_atTop_cosKernel_sub (a : UnitAddCircle) :
    ∃ p, 0 < p ∧ IsBigO atTop (cosKernel a · - 1) (fun x ↦ Real.exp (-p * x))

Proof state:
case H.intro.intro
a p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop, ‖cosKernel (↑a) x - 1‖ ≤ 2 * (HurwitzKernelBounds.F_nat 0 1 x - if 1 = 0 then 1 else 0)

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Result:
case h
a p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖cosKernel (↑a) t - 1‖ ≤ 2 * (HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0)

Proof state:
case h
a p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ∀ (i : ℕ),
    ‖2 * Real.cos (2 * π * a * (↑i + 1)) * rexp (-π * (↑i + 1) ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 0 1 t i

Tactic:
intro n

Result:
case h
a p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖2 * Real.cos (2 * π * a * (↑n + 1)) * rexp (-π * (↑n + 1) ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 0 1 t n

Proof state:
case h
a p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖2 * Real.cos (2 * π * a * (↑n + 1)) * rexp (-π * (↑n + 1) ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 0 1 t n

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]

Result:
case h
a p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ |Real.cos (2 * π * a * (↑n + 1))| * rexp (-π * (↑n + 1) ^ 2 * t) ≤ rexp (-π * (↑n + 1) ^ 2 * t)

Proof state:
a : UnitAddCircle
⊢ ∃ p, 0 < p ∧ (fun x => cosKernel a x - 1) =O[atTop] 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 _)

Result:
no goals

Proof state:
case H
a : ℝ
⊢ ∃ p, 0 < p ∧ (fun x => cosKernel (↑a) x - 1) =O[atTop] fun x => rexp (-p * x)

Tactic:
obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_nat_zero_sub zero_le_one

Result:
case H.intro.intro
a p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
⊢ ∃ p, 0 < p ∧ (fun x => cosKernel (↑a) x - 1) =O[atTop] fun x => rexp (-p * x)

Proof state:
case h
a p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ |Real.cos (2 * π * a * (↑n + 1))| * rexp (-π * (↑n + 1) ^ 2 * t) ≤ rexp (-π * (↑n + 1) ^ 2 * t)

Tactic:
exact mul_le_of_le_one_left (exp_pos _).le (abs_cos_le_one _)

Result:
no goals

Proof state:
case h
a p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖cosKernel (↑a) t - 1‖ ≤ 2 * (HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0)

Tactic:
simp only [eq_false_intro one_ne_zero, if_false, sub_zero,
  ← (hasSum_nat_cosKernel₀ a ht).tsum_eq, HurwitzKernelBounds.F_nat]

Result:
case h
a p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖∑' (b : ℕ), 2 * Real.cos (2 * π * a * (↑b + 1)) * rexp (-π * (↑b + 1) ^ 2 * t)‖ ≤
    2 * ∑' (n : ℕ), HurwitzKernelBounds.f_nat 0 1 t n

Proof state:
case h
a p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖∑' (b : ℕ), 2 * Real.cos (2 * π * a * (↑b + 1)) * rexp (-π * (↑b + 1) ^ 2 * t)‖ ≤
    2 * ∑' (n : ℕ), HurwitzKernelBounds.f_nat 0 1 t n

Tactic:
apply tsum_of_norm_bounded ((HurwitzKernelBounds.summable_f_nat 0 1 ht).hasSum.mul_left 2)

Result:
case h
a p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ∀ (i : ℕ),
    ‖2 * Real.cos (2 * π * a * (↑i + 1)) * rexp (-π * (↑i + 1) ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 0 1 t i

Proof state:
case H.intro.intro
a p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
⊢ ∃ p, 0 < p ∧ (fun x => cosKernel (↑a) x - 1) =O[atTop] fun x => rexp (-p * x)

Tactic:
refine ⟨p, hp, (Eventually.isBigO ?_).trans (hp'.const_mul_left 2)⟩

Result:
case H.intro.intro
a p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop, ‖cosKernel (↑a) x - 1‖ ≤ 2 * (HurwitzKernelBounds.F_nat 0 1 x - if 1 = 0 then 1 else 0)