awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (hypothesis)
Goal:
a : ℝ
ha : 0 ≤ a
h : a = 0
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 0 t - 1) fun (t : ℝ) ↦ rexp (-p * t)
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
have pos : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-π * t) / (1 - rexp (-π * t))) fun (t : ℝ) ↦ rexp (-π * t)
Tactic: refine ⟨_, pi_pos, this.trans ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - 0) fun (t : ℝ) ↦ rexp (-p * t)
have neg : ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t) fun (t : ℝ) ↦ rexp (-p * t)
Tactic: simp_rw [sub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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))
have hfg : ∀ᶠ (x : ℝ) in atTop, ‖F_nat 0 a x‖ ≤ rexp (-π * HPow.hPow (β := ℕ) a 2 * x) / (1 - rexp (-π * x))
Tactic: apply Eventually.isBigO
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
⊢ ∀ᶠ (x : ℝ) in atTop, ‖F_nat 0 a x‖ ≤ rexp (-π * HPow.hPow (β := ℕ) a 2 * x) / (1 - rexp (-π * x))
have h₁ : ∀ (t : ℝ) (ht : 0 < t), ‖F_nat 0 a t‖ ≤ rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))
Tactic: filter_upwards [eventually_gt_atTop 0] with t ht
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (hypothesis)
Goal:
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t) fun (t : ℝ) ↦ rexp (-p * t)
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
have neg : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
  fun (t : ℝ) ↦ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)
Tactic: refine ⟨π * a ^ 2, mul_pos pi_pos (sq_pos_of_ne_zero h), this.trans ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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))
have 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)))
Tactic: refine tsum_of_norm_bounded ?_ (f_le_g_nat 1 ha ht)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < 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)))
have 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)))
Tactic: simp_rw [pow_one, add_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < 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)))
have 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)
Tactic: apply HasSum.add
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ 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)))
have hg : HasSum (fun (b : ℕ) ↦ a * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t))
  (a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
Tactic: apply HasSum.add
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (hypothesis)
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun (b : ℕ) ↦ (↑b : ℝ) * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t))
    (rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)
have h0' : ‖rexp (-π * t)‖ < 1
Tactic: have h0' : ‖rexp (-π * t)‖ < 1 := by
      simpa only [norm_eq_abs, abs_exp] using exp_lt_aux ht
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ HasSum (fun (b : ℕ) ↦ (↑b : ℝ) * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t))
    (rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)
have h : Eq (α := ℕ → ℝ) (fun (b : ℕ) ↦ (↑b : ℝ) * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t)) fun (i : ℕ) ↦
  rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * ((↑i : ℝ) * rexp (-π * t) ^ i)
Tactic: convert! (hasSum_coe_mul_geometric_of_norm_lt_one h0').mul_left (exp (-π * a ^ 2 * t)) using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ HasSum (fun (b : ℕ) ↦ (↑b : ℝ) * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t))
    (rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t) / HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)
have 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)
Tactic: convert! (hasSum_coe_mul_geometric_of_norm_lt_one h0').mul_left (exp (-π * a ^ 2 * t)) using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ Eq (α := ℕ → ℝ) (fun (b : ℕ) ↦ (↑b : ℝ) * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t)) fun (i : ℕ) ↦
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * ((↑i : ℝ) * rexp (-π * t) ^ i)
have h : ∀ (n : ℕ),
  (↑n : ℝ) * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * ((↑n : ℝ) * rexp (-π * t) ^ n)
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
n : ℕ
⊢ (↑n : ℝ) * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
    rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * ((↑n : ℝ) * rexp (-π * t) ^ n)
have h : (↑n : ℝ) * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
  (↑n : ℝ) * rexp ((↑n : ℝ) * (-π * t) + -π * HPow.hPow (β := ℕ) a 2 * t)
Tactic: rw [mul_comm (exp _), ← Real.exp_nat_mul, mul_assoc (n : ℝ), ← Real.exp_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ 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)
have 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)
Tactic: rw [mul_add, add_mul, mul_one, exp_add, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mul_add, add_mul, mul_one, exp_add, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mul_add, add_mul, mul_one, exp_add, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mul_add, add_mul, mul_one, exp_add, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mul_add, add_mul, mul_one, exp_add, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun (b : ℕ) ↦ a * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t))
    (a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
have h : Eq (α := ℕ → ℝ) (fun (b : ℕ) ↦ a * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t)) fun (i : ℕ) ↦
  a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ i
Tactic: convert! (hasSum_geometric_of_lt_one (exp_pos _).le <| exp_lt_aux ht).mul_left _ using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ Eq (α := ℕ → ℝ) (fun (b : ℕ) ↦ a * rexp (-π * ((↑b : ℝ) + HPow.hPow (β := ℕ) a 2) * t)) fun (i : ℕ) ↦
    a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ i
have h : ∀ (n : ℕ),
  a * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
    a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) * rexp (-π * t) ^ n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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) * rexp (-π * t) ^ n
have h : a * rexp (-π * ((↑n : ℝ) + HPow.hPow (β := ℕ) a 2) * t) =
  a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t + (↑n : ℝ) * (-π * t))
Tactic: rw [← Real.exp_nat_mul, mul_assoc _ (exp _), ← Real.exp_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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 : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (F_nat 1 a) fun (t : ℝ) ↦ rexp (-p * t)
have 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)
Tactic: let ⟨p, hp, hp'⟩ := this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
have 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))
Tactic: refine ⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ ∀ᶠ (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))
have 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))
Tactic: filter_upwards [eventually_gt_atTop 0] with t ht
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
⊢ ∃ (p : ℝ), 0 < p ∧ IsBigO (F := ℝ) atTop (F_nat 1 a) fun (t : ℝ) ↦ rexp (-p * t)
have 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)
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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (hypothesis)
Goal:
a : ℝ
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)
have aux' : 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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : ℝ
ha : 0 ≤ a
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
⊢ ∃ (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)
have 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)
Tactic: rcases eq_or_lt_of_le ha with rfl | ha'
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases eq_or_lt_of_le ha with rfl | ha'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
have 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)
Tactic: refine ⟨π * a ^ 2, mul_pos pi_pos <| pow_pos ha' _, IsBigO.add ?_ ?_⟩