awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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)
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
⊢ ∃ (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:
refine ⟨p, hp, (EventuallyEq.isBigO ?_).trans hp'⟩
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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)
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
⊢ 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:
filter_upwards [eventually_gt_atTop 0] with t h

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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)
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:
simp [← (hasSum_int_evenKernel b h).tsum_eq, HurwitzKernelBounds.F_int, HurwitzKernelBounds.f_int]

Premises used: HurwitzKernelBounds.f_int, HurwitzZeta.hasSum_int_evenKernel, HasSum.tsum_eq, HurwitzKernelBounds.F_int
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
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)
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ evenKernel a x - if a = 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]

Premises used: HurwitzKernelBounds.f_int, OfNat.ofNat, HurwitzKernelBounds.F_int, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : ℝ
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)
⊢ ∃ (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

Premises used: HurwitzKernelBounds.isBigO_atTop_F_nat_zero_sub, zero_le_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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)

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

Premises used: Asymptotics.IsBigO.const_mul_left, Asymptotics.IsBigO.trans, Filter.Eventually.isBigO, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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)
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)
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x - 1) fun (x : ℝ) ↦
        rexp (-p * x)

Tactic:
refine ⟨p, hp, (Eventually.isBigO ?_).trans (hp'.const_mul_left 2)⟩
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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)
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)
⊢ ∀ᶠ (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:
filter_upwards [eventually_gt_atTop 0] with t ht

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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
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)
⊢ ‖cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t - 1‖ ≤
    2 * (HurwitzKernelBounds.F_nat 0 1 t - if Eq (α := ℝ) 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]

Premises used: sub_zero, if_false, HasSum.tsum_eq, one_ne_zero, HurwitzKernelBounds.F_nat, HurwitzZeta.hasSum_nat_cosKernel₀, eq_false_intro
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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
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
⊢ 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:
apply tsum_of_norm_bounded ((HurwitzKernelBounds.summable_f_nat 0 1 ht).hasSum.mul_left 2)

Premises used: HasSum.mul_left, HurwitzKernelBounds.summable_f_nat, Summable.hasSum, OfNat.ofNat, tsum_of_norm_bounded
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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 : ℕ
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)
⊢ ‖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

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]

Premises used: Real.norm_two, mul_assoc, two_pos, mul_le_mul_iff_of_pos_left, LT.lt.le, norm_mul, pow_zero, HurwitzKernelBounds.f_nat, one_mul, Real.norm_eq_abs, Real.norm_of_nonneg, Real.exp_pos
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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 : ℕ
⊢ |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:
mul_le_of_le_one_left (exp_pos _).le (abs_cos_le_one _)

Premises used: Real.abs_cos_le_one, LT.lt.le, mul_le_of_le_one_left, Real.exp_pos
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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 : ℕ
⊢ |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:
exact mul_le_of_le_one_left (exp_pos _).le (abs_cos_le_one _)

Premises used: Real.abs_cos_le_one, LT.lt.le, mul_le_of_le_one_left, Real.exp_pos
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
H :
  ∀ (a : ℝ),
    ∃ (p : ℝ),
      0 < p ∧
        IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x - 1) fun (x : ℝ) ↦
          rexp (-p * x)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cosKernel a 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 _)

Premises used: Real.abs_cos_le_one, Real.norm_two, sub_zero, mul_assoc, if_false, two_pos, mul_le_mul_iff_of_pos_left, LT.lt.le, norm_mul, HurwitzKernelBounds.isBigO_atTop_F_nat_zero_sub, pow_zero, zero_le_one, mul_le_of_le_one_left, HurwitzKernelBounds.f_nat, one_ne_zero, OfNat.ofNat, HurwitzKernelBounds.F_nat, eq_false_intro, one_mul, Real.norm_eq_abs, Real.norm_of_nonneg, Real.exp_pos, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (ofReal ∘ evenKernel a) (1 / x) = (1 * (↑(x ^ (1 / 2)) : ℂ)) • (ofReal ∘ cosKernel a) x

Tactic:
simp [← ofReal_mul, evenKernel_functional_equation, inv_rpow (le_of_lt hx)]

Premises used: Real.inv_rpow, le_of_lt, HurwitzZeta.evenKernel_functional_equation, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
r : ℝ
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
⊢ 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
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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)
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
⊢ 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' ⊢

Premises used: Asymptotics.isBigO_norm_left
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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)
h : ∀ (x : ℝ), ‖evenKernel a x - if a = 0 then 1 else 0‖
| IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) fun (x : ℝ) ↦ rexp (-v * x)

Tactic:
enter [2, x]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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 : ℝ
h : ‖(↑(evenKernel a x) : ℂ) - if a = 0 then 1 else 0‖
| ‖evenKernel a x - if a = 0 then 1 else 0‖

Tactic:
rw [← norm_real, ofReal_sub, apply_ite ((↑) : ℝ → ℂ), ofReal_one, ofReal_zero]

Premises used: apply_ite, Complex.ofReal_one, Complex.norm_real, Complex.ofReal, Complex.ofReal_zero, Complex.ofReal_sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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)
h : ∀ (x : ℝ), ‖(↑(evenKernel a x) : ℂ) - if a = 0 then 1 else 0‖
| IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) fun (x : ℝ) ↦ rexp (-v * x)

Tactic:
enter [2, x]; rw [← norm_real, ofReal_sub, apply_ite ((↑) : ℝ → ℂ), ofReal_one, ofReal_zero]

Premises used: apply_ite, Complex.ofReal_one, Complex.norm_real, Complex.ofReal, Complex.ofReal_zero, Complex.ofReal_sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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)

Tactic:
conv at hv' =>
      enter [2, x]; rw [← norm_real, ofReal_sub, apply_ite ((↑) : ℝ → ℂ), ofReal_one, ofReal_zero]

Premises used: apply_ite, Complex.ofReal_one, Complex.norm_real, Complex.ofReal, Complex.ofReal_zero, Complex.ofReal_sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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

Tactic:
hv'.trans (isLittleO_exp_neg_mul_rpow_atTop hv _).isBigO

Premises used: isLittleO_exp_neg_mul_rpow_atTop, Asymptotics.IsBigO.trans, Asymptotics.IsLittleO.isBigO
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
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

Tactic:
exact hv'.trans (isLittleO_exp_neg_mul_rpow_atTop hv _).isBigO

Premises used: isLittleO_exp_neg_mul_rpow_atTop, Asymptotics.IsBigO.trans, Asymptotics.IsLittleO.isBigO
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
r : ℝ
obtain :
  ∀ (p : ℝ) (hp : 0 < p)
    (hp' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cosKernel a x - 1) fun (x : ℝ) ↦ rexp (-p * x)),
    IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ cosKernel a) x - 1) fun (x : ℝ) ↦ x ^ r
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ cosKernel a) x - 1) fun (x : ℝ) ↦ x ^ r

Tactic:
obtain ⟨p, hp, hp'⟩ := isBigO_atTop_cosKernel_sub a

Premises used: HurwitzZeta.isBigO_atTop_cosKernel_sub
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
r p : ℝ
hp : 0 < p
hp' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cosKernel a x - 1) fun (x : ℝ) ↦ rexp (-p * x)
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (ofReal ∘ cosKernel a) x - 1) fun (x : ℝ) ↦ x ^ r

Tactic:
simpa using isBigO_ofReal_left.mpr <| hp'.trans (isLittleO_exp_neg_mul_rpow_atTop hp r).isBigO

Premises used: Iff.mpr, isLittleO_exp_neg_mul_rpow_atTop, Asymptotics.IsBigO.trans, Asymptotics.IsLittleO.isBigO, Complex.isBigO_ofReal_left
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
⊢ WeakFEPair.g
      { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1,
        f₀ := if Eq (α := UnitAddCircle) 0 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯,
        hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ :
        WeakFEPair ℂ } =
    ofReal ∘ evenKernel 0

Tactic:
simp [evenKernel_eq_cosKernel_of_zero]

Premises used: HurwitzZeta.evenKernel_eq_cosKernel_of_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
⊢ WeakFEPair.f
      { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1,
        f₀ := if Eq (α := UnitAddCircle) 0 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯,
        hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ :
        WeakFEPair ℂ } =
    ofReal ∘ cosKernel 0

Tactic:
simp [evenKernel_eq_cosKernel_of_zero]

Premises used: HurwitzZeta.evenKernel_eq_cosKernel_of_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
⊢ (WeakFEPair.ε
        { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1,
          f₀ := if Eq (α := UnitAddCircle) 0 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯,
          hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ :
          WeakFEPair ℂ })⁻¹ =
    1

Tactic:
simp [evenKernel_eq_cosKernel_of_zero]

Premises used: HurwitzZeta.evenKernel_eq_cosKernel_of_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
⊢ WeakFEPair.g₀
      { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1,
        f₀ := if Eq (α := UnitAddCircle) 0 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯,
        hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ :
        WeakFEPair ℂ } =
    if Eq (α := UnitAddCircle) 0 0 then 1 else 0

Tactic:
simp [evenKernel_eq_cosKernel_of_zero]

Premises used: HurwitzZeta.evenKernel_eq_cosKernel_of_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
⊢ WeakFEPair.f₀
      { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1,
        f₀ := if Eq (α := UnitAddCircle) 0 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯,
        hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ :
        WeakFEPair ℂ } =
    1

Tactic:
simp [evenKernel_eq_cosKernel_of_zero]

Premises used: HurwitzZeta.evenKernel_eq_cosKernel_of_zero
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
e_f : ofReal ∘ evenKernel (-a) = ofReal ∘ evenKernel a
e_g : ofReal ∘ cosKernel (-a) = ofReal ∘ cosKernel a
e_f₀ : Eq (α := ℂ) (if -a = 0 then 1 else 0) (if a = 0 then 1 else 0)
⊢ Eq (α := WeakFEPair ℂ)
    { f := ofReal ∘ evenKernel (-a), g := ofReal ∘ cosKernel (-a), k := 1 / 2, ε := 1, f₀ := if -a = 0 then 1 else 0,
      g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
      hf_top := ⋯, hg_top := ⋯ }
    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1, f₀ := if a = 0 then 1 else 0, g₀ := 1,
      hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
      hf_top := ⋯, hg_top := ⋯ }

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ ofReal ∘ evenKernel (-a) = ofReal ∘ evenKernel a

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ ofReal ∘ cosKernel (-a) = ofReal ∘ cosKernel a

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
⊢ Eq (α := ℂ) (if -a = 0 then 1 else 0) (if a = 0 then 1 else 0)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
rw :
  (hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 -
      ((hurwitzEvenFEPair a).ε / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).g₀ / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)
⊢ completedHurwitzZetaEven a s = completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)

Tactic:
rw [completedHurwitzZetaEven, WeakFEPair.Λ, sub_div, sub_div]

Premises used: WeakFEPair.Λ, sub_div, HurwitzZeta.completedHurwitzZetaEven
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
e_a :
  (hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
e_a₁ : ((hurwitzEvenFEPair a).ε / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).g₀ / 2 = 1 / (1 - s)
⊢ (hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 -
      ((hurwitzEvenFEPair a).ε / ((↑(hurwitzEvenFEPair a).k : ℂ) - s / 2)) • (hurwitzEvenFEPair a).g₀ / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)

Tactic:
congr 1