awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
suffices :
  ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (t : ℝ) ↦
          rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
            a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
        fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (F_nat 1 a) fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
suffices ∃ p, 0 < p ∧ (fun t ↦ rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2
      + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop] fun t ↦ exp (-p * t) by
    let ⟨p, hp, hp'⟩ := this
    refine ⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩
    filter_upwards [eventually_gt_atTop 0] with t ht
    exact F_nat_one_le ha ht
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1

Tactic:
simpa only [inv_pow, one_pow] using isBigO_one_aux.pow 2

Premises used: one_pow, inv_pow, _private.0.HurwitzKernelBounds.isBigO_one_aux, Asymptotics.IsBigO.pow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1

Tactic:
have aux' : IsBigO atTop (fun t : ℝ ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) (fun _ ↦ (1 : ℝ)) := by
    simpa only [inv_pow, one_pow] using isBigO_one_aux.pow 2
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
inl :
  ∀ (ha : LE.le (α := ℝ) 0 0),
    ∃ (p : ℝ),
      0 < p ∧
        IsBigO (E := ℝ) (F := ℝ) atTop
          (fun (t : ℝ) ↦
            rexp (-π * (HPow.hPow (α := ℝ) (β := ℕ) 0 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
              0 * rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) 0 2 * t) / (1 - rexp (-π * t)))
          fun (t : ℝ) ↦ rexp (-p * t)
inr :
  ∀ (ha' : 0 < a),
    ∃ (p : ℝ),
      0 < p ∧
        IsBigO (E := ℝ) (F := ℝ) atTop
          (fun (t : ℝ) ↦
            rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
              a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
          fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (t : ℝ) ↦
          rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
            a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
        fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
rcases eq_or_lt_of_le ha with rfl | ha'

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha : LE.le (α := ℝ) 0 0
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (t : ℝ) ↦
      rexp (-π * (HPow.hPow (α := ℝ) (β := ℕ) 0 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
        0 * rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) 0 2 * t) / (1 - rexp (-π * t)))
    fun (t : ℝ) ↦ rexp (-π * t)

Tactic:
simpa only [zero_pow two_ne_zero, zero_add, mul_one, zero_mul, zero_div,
      add_zero] using (isBigO_refl _ _).mul aux'

Premises used: MulZeroClass.zero_mul, zero_div, Asymptotics.IsBigO.mul, zero_add, two_ne_zero, mul_one, add_zero, zero_pow
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha : LE.le (α := ℝ) 0 0
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (t : ℝ) ↦
          rexp (-π * (HPow.hPow (α := ℝ) (β := ℕ) 0 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
            0 * rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) 0 2 * t) / (1 - rexp (-π * t)))
        fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
exact ⟨_, pi_pos, by simpa only [zero_pow two_ne_zero, zero_add, mul_one, zero_mul, zero_div,
      add_zero] using (isBigO_refl _ _).mul aux'⟩
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha' : 0 < a
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (t : ℝ) ↦
          rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
            a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
        fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
⟨π * a ^ 2, mul_pos pi_pos <| pow_pos ha' _, IsBigO.add ?_ ?_⟩

Premises used: pow_pos, Real.pi, HMul.hMul, Real.pi_pos, Asymptotics.IsBigO.add, mul_pos, HPow.hPow, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha' : 0 < a
inr :
  IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (t : ℝ) ↦ rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)
    fun (t : ℝ) ↦ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)
inr₁ :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
    fun (t : ℝ) ↦ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (t : ℝ) ↦
          rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
            a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
        fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
refine ⟨π * a ^ 2, mul_pos pi_pos <| pow_pos ha' _, IsBigO.add ?_ ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha' : 0 < a
h : ∀ (t : ℝ), rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)
| fun (t : ℝ) ↦ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)

Tactic:
enter [t]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha' : 0 < a
t : ℝ
h : rexp (-(π * HPow.hPow (β := ℕ) a 2) * t) * 1
| rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)

Tactic:
rw [← mul_one (rexp _)]

Premises used: Real.exp, mul_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha' : 0 < a
h : ∀ (t : ℝ), rexp (-(π * HPow.hPow (β := ℕ) a 2) * t) * 1
| fun (t : ℝ) ↦ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)

Tactic:
enter [t]; rw [← mul_one (rexp _)]

Premises used: Real.exp, mul_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha' : 0 < a
inr :
  IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (t : ℝ) ↦ rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)
    fun (t : ℝ) ↦ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t) * 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (t : ℝ) ↦ rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)
    fun (t : ℝ) ↦ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)

Tactic:
conv_rhs => enter [t]; rw [← mul_one (rexp _)]

Premises used: Real.exp, mul_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha' : 0 < a
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (t : ℝ) ↦ rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)
    fun (t : ℝ) ↦ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t) * 1

Tactic:
(Eventually.isBigO ?_).mul aux'

Premises used: Asymptotics.IsBigO.mul, DivInvMonoid.div', Filter.Eventually.isBigO
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha' : 0 < a
inr : ∀ᶠ (x : ℝ) in atTop, ‖rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * x)‖ ≤ rexp (-(π * HPow.hPow (β := ℕ) a 2) * x)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (t : ℝ) ↦ rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)
    fun (t : ℝ) ↦ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t) * 1

Tactic:
refine (Eventually.isBigO ?_).mul aux'

Premises used: Asymptotics.IsBigO.mul, Filter.Eventually.isBigO
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha' : 0 < a
h : ∀ (t : ℝ) (ht : 0 < t), ‖rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t)‖ ≤ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)
⊢ ∀ᶠ (x : ℝ) in atTop, ‖rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * x)‖ ≤ rexp (-(π * HPow.hPow (β := ℕ) a 2) * x)

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha' : 0 < a
t : ℝ
ht : 0 < t
h : -π * (HPow.hPow (β := ℕ) a 2 + 1) * t ≤ -(π * HPow.hPow (β := ℕ) a 2) * t
⊢ ‖rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t)‖ ≤ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)

Tactic:
rw [norm_of_nonneg (exp_pos _).le, exp_le_exp]

Premises used: LT.lt.le, Real.exp_le_exp, Real.norm_of_nonneg, Real.exp_pos
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha' : 0 < a
t : ℝ
ht : 0 < t
nlinarith :
  -(π * HPow.hPow (β := ℕ) a 2) * t < -π * (HPow.hPow (β := ℕ) a 2 + 1) * t →
    -(π * HPow.hPow (β := ℕ) a 2) * t - -π * (HPow.hPow (β := ℕ) a 2 + 1) * t + (0 - (0 - t) * (0 - π)) = 0
⊢ -π * (HPow.hPow (β := ℕ) a 2 + 1) * t ≤ -(π * HPow.hPow (β := ℕ) a 2) * t

Tactic:
nlinarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha' : 0 < a
inr :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ a * (rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))))
    fun (t : ℝ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * t)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
    fun (t : ℝ) ↦ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)

Tactic:
simp_rw [mul_div_assoc, ← neg_mul]

Premises used: mul_div_assoc, neg_mul
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha' : 0 < a
inr :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * x) / (1 - rexp (-π * x)))
    fun (t : ℝ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * t)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ a * (rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))))
    fun (t : ℝ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * t)

Tactic:
apply IsBigO.const_mul_left

Premises used: Asymptotics.IsBigO.const_mul_left
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha' : 0 < a
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * x) / (1 - rexp (-π * x)))
    fun (t : ℝ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * t)

Tactic:
simpa only [mul_one] using (isBigO_refl _ _).mul isBigO_one_aux

Premises used: Asymptotics.IsBigO.mul, _private.0.HurwitzKernelBounds.isBigO_one_aux, mul_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a : ℝ
ha : 0 ≤ a
t : ℝ
n : ℕ
⊢ 0 ≤ (↑n : ℝ) + a

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a : ℝ
ha : 0 ≤ a
t : ℝ
n : ℕ
rw : |(↑(Int.ofNat n) : ℝ) + a| ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑(Int.ofNat n) : ℝ) + a) 2 * t) = f_nat k a t n
rw₁ :
  |(↑(Int.ofNat n) : ℝ) + a| ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑(Int.ofNat n) : ℝ) + a) 2 * t) =
    ((↑n : ℝ) + a) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
rw₂ :
  |(↑(↑n : ℤ) : ℝ) + a| ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑(↑n : ℤ) : ℝ) + a) 2 * t) =
    ((↑n : ℝ) + a) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
rw₃ :
  |(↑n : ℝ) + a| ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t) =
    ((↑n : ℝ) + a) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
rw₄ rw₅ :
  ((↑n : ℝ) + a) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t) =
    ((↑n : ℝ) + a) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
⊢ f_int k a t (Int.ofNat n) = f_nat k a t n

Tactic:
rw [f_int, f_nat, Int.ofNat_eq_natCast, Int.cast_natCast, abs_of_nonneg (by positivity)]

Premises used: HurwitzKernelBounds.f_int, Int.cast_natCast, Int.ofNat_eq_natCast, HurwitzKernelBounds.f_nat, abs_of_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
push_cast : -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a = -((↑n : ℝ) + (1 - a))
⊢ (↑(Int.negSucc n) : ℝ) + a = -((↑n : ℝ) + (1 - a))

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a = -((↑n : ℝ) + (1 - a))

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
ring ring₁ : -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a = -((↑n : ℝ) + (1 - a))
⊢ (↑(Int.negSucc n) : ℝ) + a = -((↑n : ℝ) + (1 - a))

Tactic:
{ push_cast; ring }
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ (↑(Int.negSucc n) : ℝ) + a = -((↑n : ℝ) + (1 - a))

Tactic:
have : (Int.negSucc n) + a = -(n + (1 - a)) := by { push_cast; ring }
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
this : (↑(Int.negSucc n) : ℝ) + a = -((↑n : ℝ) + (1 - a))
linarith : (↑n : ℝ) + (1 - a) < 0 → HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (a - 1) + ((↑n : ℝ) + (1 - a) - 0) = 0
⊢ 0 ≤ (↑n : ℝ) + (1 - a)

Tactic:
linarith
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
this : (↑(Int.negSucc n) : ℝ) + a = -((↑n : ℝ) + (1 - a))
rw :
  |(↑(Int.negSucc n) : ℝ) + a| ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑(Int.negSucc n) : ℝ) + a) 2 * t) =
    f_nat k (1 - a) t n
rw₁ :
  |(↑(Int.negSucc n) : ℝ) + a| ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑(Int.negSucc n) : ℝ) + a) 2 * t) =
    ((↑n : ℝ) + (1 - a)) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + (1 - a)) 2 * t)
rw₂ :
  |(-((↑n : ℝ) + (1 - a)))| ^ k * rexp (-π * HPow.hPow (β := ℕ) (-((↑n : ℝ) + (1 - a))) 2 * t) =
    ((↑n : ℝ) + (1 - a)) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + (1 - a)) 2 * t)
rw₃ :
  |(↑n : ℝ) + (1 - a)| ^ k * rexp (-π * HPow.hPow (β := ℕ) (-((↑n : ℝ) + (1 - a))) 2 * t) =
    ((↑n : ℝ) + (1 - a)) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + (1 - a)) 2 * t)
rw₄ :
  |(↑n : ℝ) + (1 - a)| ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + (1 - a)) 2 * t) =
    ((↑n : ℝ) + (1 - a)) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + (1 - a)) 2 * t)
rw₅ rw₆ :
  ((↑n : ℝ) + (1 - a)) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + (1 - a)) 2 * t) =
    ((↑n : ℝ) + (1 - a)) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + (1 - a)) 2 * t)
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n

Tactic:
rw [f_int, f_nat, this, abs_neg, neg_sq, abs_of_nonneg (by linarith)]

Premises used: HurwitzKernelBounds.f_int, abs_neg, neg_sq, HurwitzKernelBounds.f_nat, abs_of_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
hf : Summable (α := ℝ) fun (a_1 : ℤ) ↦ ‖f_int k a t a_1‖
⊢ Summable (f_int k a t)

Tactic:
apply Summable.of_norm

Premises used: Summable.of_norm
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
hf :
  ∀ (n : ℤ),
    ‖f_int k a t n‖ =
      Norm.norm (E := ℝ)
        ((fun (t_1 : ℤ) ↦ (Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) t_1 : ℝ)) n)
⊢ Summable (α := ℝ) fun (a_1 : ℤ) ↦ ‖f_int k a t a_1‖

Tactic:
suffices ∀ n, ‖f_int k a t n‖ = ‖(Int.rec (f_nat k a t) (f_nat k (1 - a) t) : ℤ → ℝ) n‖ from
    funext this ▸ (HasSum.int_rec (summable_f_nat k a ht).hasSum
      (summable_f_nat k (1 - a) ht).hasSum).summable.norm
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℤ
hf :
  ∀ (a_1 : ℕ),
    ‖f_int k a t (Int.ofNat a_1)‖ =
      Norm.norm (E := ℝ)
        ((fun (t_1 : ℤ) ↦ (Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) t_1 : ℝ))
          (Int.ofNat a_1))
hf₁ :
  ∀ (m : ℕ),
    ‖f_int k a t (Int.negSucc m)‖ =
      Norm.norm (E := ℝ)
        ((fun (t_1 : ℤ) ↦ (Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) t_1 : ℝ))
          (Int.negSucc m))
⊢ ‖f_int k a t n‖ =
    Norm.norm (E := ℝ)
      ((fun (t_1 : ℤ) ↦ (Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) t_1 : ℝ)) n)

Tactic:
rcases n with - | m
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
a_1 : ℕ
⊢ ‖f_int k a t (Int.ofNat a_1)‖ =
    Norm.norm (E := ℝ)
      ((fun (t_1 : ℤ) ↦ (Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) t_1 : ℝ))
        (Int.ofNat a_1))

Tactic:
simp only [f_int, f_nat, Int.ofNat_eq_natCast, Int.cast_natCast, norm_mul, norm_eq_abs, abs_pow,
      abs_abs]

Premises used: HurwitzKernelBounds.f_int, Int.cast_natCast, Int.ofNat_eq_natCast, norm_mul, HurwitzKernelBounds.f_nat, abs_abs, Real.norm_eq_abs, abs_pow
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
push_cast : -HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + a = -((↑m : ℝ) + (1 - a))
⊢ -(↑(m + 1) : ℝ) + a = -((↑m : ℝ) + (1 - a))

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ -HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + a = -((↑m : ℝ) + (1 - a))

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
ring ring₁ : -HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + a = -((↑m : ℝ) + (1 - a))
⊢ -(↑(m + 1) : ℝ) + a = -((↑m : ℝ) + (1 - a))

Tactic:
{ push_cast; ring }
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a : UnitAddCircle
t b : ℝ
simp_rw : Eq (α := ℝ) (∑' (n : ℤ), f_int k (b + 1) t n) (∑' (c : ℤ), f_int k b t ((Equiv.addRight 1 : (a : ℤ) → ℤ) c))
⊢ Eq (α := ℝ) ((fun (b : ℝ) ↦ (∑' (n : ℤ), f_int k b t n : ℝ)) (b + 1))
    ((fun (b : ℝ) ↦ (∑' (n : ℤ), f_int k b t n : ℝ)) b)

Tactic:
simp_rw [← (Equiv.addRight (1 : ℤ)).tsum_eq (f := fun n ↦ f_int k b t n)]

Premises used: Equiv.addRight, HurwitzKernelBounds.f_int, Equiv.tsum_eq, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a : UnitAddCircle
t b : ℝ
⊢ Eq (α := ℝ) (∑' (n : ℤ), f_int k (b + 1) t n) (∑' (c : ℤ), f_int k b t ((Equiv.addRight 1 : (a : ℤ) → ℤ) c))

Tactic:
simp only [f_int, ← add_assoc, add_comm, Equiv.coe_addRight, Int.cast_add, Int.cast_one]

Premises used: HurwitzKernelBounds.f_int, add_assoc, Int.cast_add, Equiv.coe_addRight, add_comm, Int.cast_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
t : ℝ
ht : 0 < t
⊢ ∑' (b : ℤ), Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) b =
    HAdd.hAdd (α := ℝ) (∑' (b : ℕ), f_nat k a t b) (∑' (b : ℕ), f_nat k (1 - a) t b)

Tactic:
((summable_f_nat k a ht).hasSum.int_rec (summable_f_nat k (1 - a) ht).hasSum).tsum_eq

Premises used: HSub.hSub, HurwitzKernelBounds.summable_f_nat, HasSum.tsum_eq, Summable.hasSum, HasSum.int_rec, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
t : ℝ
ht : 0 < t
h : ∀ (n : ℤ), f_int k a t n = Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) n
⊢ ∑' (n : ℤ), f_int k a t n = HAdd.hAdd (α := ℝ) (∑' (n : ℕ), f_nat k a t n) (∑' (n : ℕ), f_nat k (1 - a) t n)

Tactic:
convert!
    ((summable_f_nat k a ht).hasSum.int_rec (summable_f_nat k (1 - a) ht).hasSum).tsum_eq using
    3 with n

Premises used: HSub.hSub, HurwitzKernelBounds.summable_f_nat, HasSum.tsum_eq, Summable.hasSum, HasSum.int_rec, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
t : ℝ
ht : 0 < t
n : ℤ
h :
  ∀ (a_1 : ℕ),
    f_int k a t (Int.ofNat a_1) = Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) (Int.ofNat a_1)
h₁ :
  ∀ (a_1 : ℕ),
    f_int k a t (Int.negSucc a_1) =
      Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) (Int.negSucc a_1)
⊢ f_int k a t n = Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) n

Tactic:
cases n
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
t : ℝ
ht : 0 < t
a_1 : ℕ
h h₁ : f_nat k a t a_1 = Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) (Int.ofNat a_1)
⊢ f_int k a t (Int.ofNat a_1) = Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) (Int.ofNat a_1)

Tactic:
rw [f_int_ofNat _ ha.1]

Premises used: And.left, HurwitzKernelBounds.f_int_ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
k : ℕ
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
t : ℝ
ht : 0 < t
a_1 : ℕ
h h₁ : f_nat k (1 - a) t a_1 = Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) (Int.negSucc a_1)
⊢ f_int k a t (Int.negSucc a_1) =
    Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) (Int.negSucc a_1)

Tactic:
rw [f_int_negSucc _ ha.2]

Premises used: HurwitzKernelBounds.f_int_negSucc, And.right
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : UnitAddCircle
obtain :
  ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Ico 0 1) a),
    ∃ (p : ℝ),
      0 < p ∧
        IsBigO (E := ℝ) (F := ℝ) atTop
          (fun (t : ℝ) ↦
            F_int 0 (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t -
              if Eq (α := UnitAddCircle) (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) 0 then 1 else 0)
          fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_int 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
obtain ⟨a, ha, rfl⟩ := a.eq_coe_Ico

Premises used: AddCircle.eq_coe_Ico, rfl