awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
pos :
  ∀ (h : a = 0),
    ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - 1) fun (t : ℝ) ↦ rexp (-p * t)
neg :
  ∀ (h : ¬a = 0),
    ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - 0) fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ),
    0 < p ∧
      IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : a = 0
pos : ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 0 t - 1) fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - 1) fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
rw [h]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : a = 0
hfg : ∀ᶠ (x : ℝ) in atTop, ‖F_nat 0 0 x - 1‖ ≤ rexp (-π * x) / (1 - rexp (-π * x))
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 0 t - 1) fun (t : ℝ) ↦ rexp (-π * t) / (1 - rexp (-π * t))

Tactic:
apply Eventually.isBigO

Premises used: Filter.Eventually.isBigO
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : a = 0
h₁ : ∀ (t : ℝ) (ht : 0 < t), ‖F_nat 0 0 t - 1‖ ≤ rexp (-π * t) / (1 - rexp (-π * t))
⊢ ∀ᶠ (x : ℝ) in atTop, ‖F_nat 0 0 x - 1‖ ≤ rexp (-π * x) / (1 - rexp (-π * 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
h : a = 0
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 0 t - 1‖ ≤ rexp (-π * t) / (1 - rexp (-π * t))

Tactic:
F_nat_zero_zero_sub_le ht

Premises used: HurwitzKernelBounds.F_nat_zero_zero_sub_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : a = 0
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 0 t - 1‖ ≤ rexp (-π * t) / (1 - rexp (-π * t))

Tactic:
exact F_nat_zero_zero_sub_le ht

Premises used: HurwitzKernelBounds.F_nat_zero_zero_sub_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : a = 0
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 0 t - 1) fun (t : ℝ) ↦ rexp (-π * t) / (1 - rexp (-π * t))

Tactic:
have : (fun t ↦ F_nat 0 0 t - 1) =O[atTop] fun t ↦ rexp (-π * t) / (1 - rexp (-π * t)) := by
      apply Eventually.isBigO
      filter_upwards [eventually_gt_atTop 0] with t ht
      exact F_nat_zero_zero_sub_le ht
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : a = 0
this : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 0 t - 1) fun (t : ℝ) ↦ rexp (-π * t) / (1 - rexp (-π * t))
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 0 t - 1) fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
⟨_, pi_pos, this.trans ?_⟩

Premises used: Real.pi_pos, Asymptotics.IsBigO.trans, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : a = 0
this : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 0 t - 1) fun (t : ℝ) ↦ rexp (-π * t) / (1 - rexp (-π * t))
pos : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-π * t) / (1 - rexp (-π * t))) fun (t : ℝ) ↦ rexp (-π * t)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 0 t - 1) fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
refine ⟨_, pi_pos, this.trans ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : a = 0
this : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 0 t - 1) fun (t : ℝ) ↦ rexp (-π * t) / (1 - rexp (-π * t))
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-π * t) / (1 - rexp (-π * t))) fun (t : ℝ) ↦ rexp (-π * t)

Tactic:
simpa using (isBigO_refl (fun t ↦ rexp (-π * t)) _).mul isBigO_one_aux

Premises used: Real.pi, HMul.hMul, Asymptotics.IsBigO.mul, Real.exp, _private.0.HurwitzKernelBounds.isBigO_one_aux, Neg.neg, Asymptotics.isBigO_refl
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
neg : ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t) fun (t : ℝ) ↦ rexp (-p * t)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - 0) fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
simp_rw [sub_zero]

Premises used: sub_zero
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
hfg : ∀ᶠ (x : ℝ) in atTop, ‖F_nat 0 a x‖ ≤ rexp (-π * HPow.hPow (β := ℕ) a 2 * x) / (1 - rexp (-π * x))
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t) fun (t : ℝ) ↦
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))

Tactic:
apply Eventually.isBigO

Premises used: Filter.Eventually.isBigO
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
h₁ : ∀ (t : ℝ) (ht : 0 < t), ‖F_nat 0 a t‖ ≤ rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))
⊢ ∀ᶠ (x : ℝ) in atTop, ‖F_nat 0 a x‖ ≤ rexp (-π * HPow.hPow (β := ℕ) a 2 * x) / (1 - rexp (-π * 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
h : ¬a = 0
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 a t‖ ≤ rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))

Tactic:
F_nat_zero_le ha ht

Premises used: HurwitzKernelBounds.F_nat_zero_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 a t‖ ≤ rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))

Tactic:
exact F_nat_zero_le ha ht

Premises used: HurwitzKernelBounds.F_nat_zero_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t) fun (t : ℝ) ↦
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))

Tactic:
have : (fun t ↦ F_nat 0 a t) =O[atTop] fun t ↦ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)) := by
      apply Eventually.isBigO
      filter_upwards [eventually_gt_atTop 0] with t ht
      exact F_nat_zero_le ha ht
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
this :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t) fun (t : ℝ) ↦
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t) fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
⟨π * a ^ 2, mul_pos pi_pos (sq_pos_of_ne_zero h), this.trans ?_⟩

Premises used: Real.pi, HMul.hMul, Real.pi_pos, Asymptotics.IsBigO.trans, mul_pos, HPow.hPow, And.intro, Exists.intro, sq_pos_of_ne_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
this :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t) fun (t : ℝ) ↦
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))
neg :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ 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 : ℝ) ↦ F_nat 0 a t) fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
refine ⟨π * a ^ 2, mul_pos pi_pos (sq_pos_of_ne_zero h), this.trans ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
this :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t) fun (t : ℝ) ↦
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
    fun (t : ℝ) ↦ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)

Tactic:
simpa only [neg_mul π (a ^ 2), mul_one] using (isBigO_refl _ _).mul isBigO_one_aux

Premises used: Real.pi, Asymptotics.IsBigO.mul, HPow.hPow, _private.0.HurwitzKernelBounds.isBigO_one_aux, neg_mul, mul_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ ‖F_nat 1 a t‖ ≤
    rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
      a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))

Tactic:
tsum_of_norm_bounded ?_ (f_le_g_nat 1 ha ht)

Premises used: HurwitzKernelBounds.f_le_g_nat, OfNat.ofNat, tsum_of_norm_bounded, HurwitzKernelBounds.F_nat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
refine :
  HasSum (g_nat 1 a t)
    (rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
      a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
⊢ ‖F_nat 1 a t‖ ≤
    rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
      a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))

Tactic:
refine tsum_of_norm_bounded ?_ (f_le_g_nat 1 ha ht)

Premises used: HurwitzKernelBounds.f_le_g_nat, OfNat.ofNat, tsum_of_norm_bounded
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
simp_rw :
  HasSum
    (fun (n : ℕ) ↦
      (↑n : ℝ) * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) +
        a * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t))
    (rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
      a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 1 * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t))
    (rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
      a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))

Tactic:
simp_rw [pow_one, add_mul]

Premises used: add_mul, pow_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
hf :
  HasSum (fun (b : ℕ) ↦ (↑b : ℝ) * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t))
    (rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)
hg :
  HasSum (fun (b : ℕ) ↦ a * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t))
    (a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
⊢ HasSum
    (fun (n : ℕ) ↦
      (↑n : ℝ) * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) +
        a * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t))
    (rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
      a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))

Tactic:
apply HasSum.add

Premises used: HasSum.add
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ ‖rexp (-π * t)‖ < 1

Tactic:
simpa only [norm_eq_abs, abs_exp] using exp_lt_aux ht

Premises used: _private.0.HurwitzKernelBounds.exp_lt_aux, Real.norm_eq_abs, Real.abs_exp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ ‖rexp (-π * t)‖ < 1

Tactic:
have h0' : ‖rexp (-π * t)‖ < 1 := by
      simpa only [norm_eq_abs, abs_exp] using exp_lt_aux ht
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ HasSum (fun (i : ℕ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * ((↑i : ℝ) * rexp (-π * t) ^ i))
    (rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * (rexp (-π * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2))

Tactic:
(hasSum_coe_mul_geometric_of_norm_lt_one h0').mul_left (exp (-π * a ^ 2 * t))

Premises used: Real.pi, HMul.hMul, HasSum.mul_left, Real.exp, hasSum_coe_mul_geometric_of_norm_lt_one, HPow.hPow, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
h :
  Eq (α := ℕ → ℝ) (fun (b : ℕ) ↦ (↑b : ℝ) * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t)) fun (i : ℕ) ↦
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * ((↑i : ℝ) * rexp (-π * t) ^ i)
h₁ :
  rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 =
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * (rexp (-π * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)
⊢ HasSum (fun (b : ℕ) ↦ (↑b : ℝ) * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t))
    (rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)

Tactic:
convert! (hasSum_coe_mul_geometric_of_norm_lt_one h0').mul_left (exp (-π * a ^ 2 * t)) using 1

Premises used: Real.pi, HMul.hMul, HasSum.mul_left, Real.exp, hasSum_coe_mul_geometric_of_norm_lt_one, HPow.hPow, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
h :
  ∀ (n : ℕ),
    (↑n : ℝ) * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
      rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * ((↑n : ℝ) * rexp (-π * t) ^ n)
⊢ Eq (α := ℕ → ℝ) (fun (b : ℕ) ↦ (↑b : ℝ) * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t)) fun (i : ℕ) ↦
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * ((↑i : ℝ) * rexp (-π * t) ^ i)

Tactic:
ext1 n
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
n : ℕ
h :
  (↑n : ℝ) * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
    (↑n : ℝ) * rexp ((↑n : ℝ) * (-π * t) + -π * HPow.hPow (β := ℕ) a 2 * t)
⊢ (↑n : ℝ) * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * ((↑n : ℝ) * rexp (-π * t) ^ n)

Tactic:
rw [mul_comm (exp _), ← Real.exp_nat_mul, mul_assoc (n : ℝ), ← Real.exp_add]

Premises used: mul_assoc, Real.exp, Nat.cast, mul_comm, Real.exp_nat_mul, Real.exp_add
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
n : ℕ
⊢ (↑n : ℝ) * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
    (↑n : ℝ) * rexp ((↑n : ℝ) * (-π * t) + -π * HPow.hPow (β := ℕ) a 2 * t)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
h :
  rexp ((-π * HPow.hPow (β := ℕ) a 2 + -π * 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 =
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * (rexp (-π * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)
h₁ :
  rexp (-π * HPow.hPow (β := ℕ) a 2 * t + -π * 1 * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 =
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * (rexp (-π * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)
h₂ :
  rexp (-π * HPow.hPow (β := ℕ) a 2 * t + -π * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 =
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * (rexp (-π * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)
h₃ :
  rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 =
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * (rexp (-π * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)
h₄ h₅ :
  rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * (rexp (-π * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2) =
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * (rexp (-π * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)
⊢ rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 =
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * (rexp (-π * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)

Tactic:
rw [mul_add, add_mul, mul_one, exp_add, mul_div_assoc]

Premises used: add_mul, mul_div_assoc, mul_add, mul_one, Real.exp_add
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun (i : ℕ) ↦ a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ i)
    (a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * (1 - rexp (-π * t))⁻¹)

Tactic:
(hasSum_geometric_of_lt_one (exp_pos _).le <| exp_lt_aux ht).mul_left _

Premises used: _private.0.HurwitzKernelBounds.exp_lt_aux, LT.lt.le, HasSum.mul_left, hasSum_geometric_of_lt_one, Real.exp_pos
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h :
  Eq (α := ℕ → ℝ) (fun (b : ℕ) ↦ a * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t)) fun (i : ℕ) ↦
    a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ i
⊢ HasSum (fun (b : ℕ) ↦ a * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t))
    (a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))

Tactic:
convert! (hasSum_geometric_of_lt_one (exp_pos _).le <| exp_lt_aux ht).mul_left _ using 1

Premises used: _private.0.HurwitzKernelBounds.exp_lt_aux, LT.lt.le, HasSum.mul_left, hasSum_geometric_of_lt_one, Real.exp_pos
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h :
  ∀ (n : ℕ),
    a * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
      a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ n
⊢ Eq (α := ℕ → ℝ) (fun (b : ℕ) ↦ a * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t)) fun (i : ℕ) ↦
    a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ i

Tactic:
ext1 n
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
h :
  a * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
    a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t + (↑n : ℝ) * (-π * t))
⊢ a * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
    a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ n

Tactic:
rw [← Real.exp_nat_mul, mul_assoc _ (exp _), ← Real.exp_add]

Premises used: mul_assoc, Real.exp, Real.exp_nat_mul, Real.exp_add
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ a * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
    a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t + (↑n : ℝ) * (-π * t))

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
this :
  ∃ (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)
let :
  ∀ (p : ℝ) (hp : 0 < p)
    (hp' :
      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)
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (F_nat 1 a) fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
let ⟨p, hp, hp'⟩ := this
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
this :
  ∃ (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 : ℝ
hp : 0 < p
hp' :
  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:
⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩

Premises used: Asymptotics.IsBigO.trans, Filter.Eventually.isBigO, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
this :
  ∃ (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 : ℝ
hp : 0 < p
hp' :
  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)
refine :
  ∀ᶠ (x : ℝ) in atTop,
    ‖F_nat 1 a x‖ ≤
      rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * x) / HPow.hPow (β := ℕ) (1 - rexp (-π * x)) 2 +
        a * rexp (-π * HPow.hPow (β := ℕ) a 2 * x) / (1 - rexp (-π * x))
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (F_nat 1 a) fun (t : ℝ) ↦ rexp (-p * t)

Tactic:
refine ⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
this :
  ∃ (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 : ℝ
hp : 0 < p
hp' :
  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)
h :
  ∀ (t : ℝ) (ht : 0 < t),
    ‖F_nat 1 a t‖ ≤
      rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
        a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))
⊢ ∀ᶠ (x : ℝ) in atTop,
    ‖F_nat 1 a x‖ ≤
      rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * x) / HPow.hPow (β := ℕ) (1 - rexp (-π * x)) 2 +
        a * rexp (-π * HPow.hPow (β := ℕ) a 2 * x) / (1 - rexp (-π * 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
this :
  ∃ (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 : ℝ
hp : 0 < p
hp' :
  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)
t : ℝ
ht : 0 < t
⊢ ‖F_nat 1 a t‖ ≤
    rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
      a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))

Tactic:
F_nat_one_le ha ht

Premises used: HurwitzKernelBounds.F_nat_one_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
Goal:
a : ℝ
ha : 0 ≤ a
this :
  ∃ (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 : ℝ
hp : 0 < p
hp' :
  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)
t : ℝ
ht : 0 < t
⊢ ‖F_nat 1 a t‖ ≤
    rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2 +
      a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))

Tactic:
exact F_nat_one_le ha ht

Premises used: HurwitzKernelBounds.F_nat_one_le