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

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

Tactic:
obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_nat_one (le_refl 0)

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

Proof state:
case H.intro.intro
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t => rexp (-p * t)
⊢ ∃ p, 0 < p ∧ sinKernel ↑a =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' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t => rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop, ‖sinKernel (↑a) x‖ ≤ 2 * HurwitzKernelBounds.F_nat 1 0 x

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

Tactic:
rw [norm_mul, norm_mul, norm_mul, norm_two, mul_assoc, mul_assoc,
  mul_le_mul_iff_of_pos_left two_pos, HurwitzKernelBounds.f_nat, pow_one, add_zero,
  norm_of_nonneg (exp_pos _).le, Real.norm_eq_abs, Nat.abs_cast, ← mul_assoc,
  mul_le_mul_iff_of_pos_right (exp_pos _)]

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

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

Tactic:
intro n

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

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

Tactic:
rw [HurwitzKernelBounds.F_nat, ← (hasSum_nat_sinKernel a ht).tsum_eq]

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

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

Tactic:
apply tsum_of_norm_bounded (g := fun n ↦ 2 * HurwitzKernelBounds.f_nat 1 0 t n)

Result:
case h.hg
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t => rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ HasSum (fun n => 2 * HurwitzKernelBounds.f_nat 1 0 t n) (2 * ∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n)

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

Proof state:
case h.hg
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t => rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ HasSum (fun n => 2 * HurwitzKernelBounds.f_nat 1 0 t n) (2 * ∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n)

Tactic:
exact (HurwitzKernelBounds.summable_f_nat 1 0 ht).hasSum.mul_left _

Result:
no goals

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

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

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

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

Tactic:
exact mul_le_of_le_one_right (Nat.cast_nonneg _) (abs_sin_le_one _)

Result:
no goals