awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ ∃ (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 : ℝ) ↦ a * 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 <| pow_pos ha' _, IsBigO.add ?_ ?_⟩
-- 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
| fun (t : ℝ) ↦ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)
have h : ∀ (t : ℝ), rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)
Tactic: enter [t]
-- 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
t : ℝ
| rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)
have h : rexp (-(π * HPow.hPow (β := ℕ) a 2) * t) * 1
Tactic: rw [← mul_one (rexp _)]
-- 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
| fun (t : ℝ) ↦ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)
have h : ∀ (t : ℝ), rexp (-(π * HPow.hPow (β := ℕ) a 2) * t) * 1
Tactic: enter [t]; rw [← mul_one (rexp _)]
-- 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
⊢ 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)
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) * 1
Tactic: conv_rhs => enter [t]; rw [← mul_one (rexp _)]
-- 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
⊢ 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
have inr : ∀ᶠ (x : ℝ) in atTop, ‖rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * x)‖ ≤ rexp (-(π * HPow.hPow (β := ℕ) a 2) * x)
Tactic: refine (Eventually.isBigO ?_).mul aux'
-- 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
⊢ ∀ᶠ (x : ℝ) in atTop, ‖rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * x)‖ ≤ rexp (-(π * HPow.hPow (β := ℕ) a 2) * x)
have h : ∀ (t : ℝ) (ht : 0 < t), ‖rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t)‖ ≤ rexp (-(π * HPow.hPow (β := ℕ) a 2) * 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
aux' : IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ (HPow.hPow (β := ℕ) (1 - rexp (-π * t)) 2)⁻¹) fun (x : ℝ) ↦ 1
ha' : 0 < a
t : ℝ
ht : 0 < t
⊢ ‖rexp (-π * (HPow.hPow (β := ℕ) a 2 + 1) * t)‖ ≤ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)
have h : -π * (HPow.hPow (β := ℕ) a 2 + 1) * t ≤ -(π * HPow.hPow (β := ℕ) a 2) * t
Tactic: rw [norm_of_nonneg (exp_pos _).le, exp_le_exp]
-- 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
t : ℝ
ht : 0 < t
⊢ -π * (HPow.hPow (β := ℕ) a 2 + 1) * t ≤ -(π * HPow.hPow (β := ℕ) a 2) * t
have 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
Tactic: nlinarith [pi_pos]
-- 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
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ a * rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t)))
    fun (t : ℝ) ↦ rexp (-(π * HPow.hPow (β := ℕ) a 2) * t)
have 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)
Tactic: simp_rw [mul_div_assoc, ← neg_mul]
-- 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
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ a * (rexp (-π * HPow.hPow (β := ℕ) a 2 * t) / (1 - rexp (-π * t))))
    fun (t : ℝ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * t)
have inr : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * x) / (1 - rexp (-π * x)))
  fun (t : ℝ) ↦ rexp (-π * HPow.hPow (β := ℕ) a 2 * t)
Tactic: apply IsBigO.const_mul_left
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a : ℝ
ha : 0 ≤ a
t : ℝ
n : ℕ
⊢ f_int k a t (Int.ofNat n) = f_nat k a t n
have rw : |(↑(Int.ofNat n) : ℝ) + a| ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑(Int.ofNat n) : ℝ) + a) 2 * t) = f_nat k a t n
Tactic: rw [f_int, f_nat, Int.ofNat_eq_natCast, Int.cast_natCast, abs_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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
⊢ f_int k a t (Int.ofNat n) = f_nat k a t n
have 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)
Tactic: rw [f_int, f_nat, Int.ofNat_eq_natCast, Int.cast_natCast, abs_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ f_int k a t (Int.ofNat n) = f_nat k a t n
have rw₂ : |(↑(↑n : ℤ) : ℝ) + a| ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑(↑n : ℤ) : ℝ) + a) 2 * t) =
  ((↑n : ℝ) + a) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
Tactic: rw [f_int, f_nat, Int.ofNat_eq_natCast, Int.cast_natCast, abs_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ f_int k a t (Int.ofNat n) = f_nat k a t n
have rw₃ : |(↑n : ℝ) + a| ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t) =
  ((↑n : ℝ) + a) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
Tactic: rw [f_int, f_nat, Int.ofNat_eq_natCast, Int.cast_natCast, abs_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ f_int k a t (Int.ofNat n) = f_nat k a t n
have rw₄ : ((↑n : ℝ) + a) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t) =
  ((↑n : ℝ) + a) ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t)
Tactic: rw [f_int, f_nat, Int.ofNat_eq_natCast, Int.cast_natCast, abs_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ (↑(Int.negSucc n) : ℝ) + a = -((↑n : ℝ) + (1 - a))
have push_cast : -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a = -((↑n : ℝ) + (1 - a))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ (↑(Int.negSucc n) : ℝ) + a = -((↑n : ℝ) + (1 - a))
have ring : -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a = -((↑n : ℝ) + (1 - a))
Tactic: { push_cast; ring }
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (hypothesis)
Goal:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n
have this : (↑(Int.negSucc n) : ℝ) + a = -((↑n : ℝ) + (1 - a))
Tactic: have : (Int.negSucc n) + a = -(n + (1 - a)) := by { push_cast; ring }
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
this : (↑(Int.negSucc n) : ℝ) + a = -((↑n : ℝ) + (1 - a))
⊢ 0 ≤ (↑n : ℝ) + (1 - a)
have linarith : (↑n : ℝ) + (1 - a) < 0 → HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (a - 1) + ((↑n : ℝ) + (1 - a) - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
this : (↑(Int.negSucc n) : ℝ) + a = -((↑n : ℝ) + (1 - a))
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n
have rw : |(↑(Int.negSucc n) : ℝ) + a| ^ k * rexp (-π * HPow.hPow (β := ℕ) ((↑(Int.negSucc n) : ℝ) + a) 2 * t) =
  f_nat k (1 - a) t n
Tactic: rw [f_int, f_nat, this, abs_neg, neg_sq, abs_of_nonneg (by linarith)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n
have 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)
Tactic: rw [f_int, f_nat, this, abs_neg, neg_sq, abs_of_nonneg (by linarith)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n
have 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)
Tactic: rw [f_int, f_nat, this, abs_neg, neg_sq, abs_of_nonneg (by linarith)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n
have 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)
Tactic: rw [f_int, f_nat, this, abs_neg, neg_sq, abs_of_nonneg (by linarith)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n
have 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)
Tactic: rw [f_int, f_nat, this, abs_neg, neg_sq, abs_of_nonneg (by linarith)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n
have 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)
Tactic: rw [f_int, f_nat, this, abs_neg, neg_sq, abs_of_nonneg (by linarith)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
⊢ Summable (f_int k a t)
have hf : Summable (α := ℝ) fun (a_1 : ℤ) ↦ ‖f_int k a t a_1‖
Tactic: apply Summable.of_norm
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
⊢ Summable (α := ℝ) fun (a_1 : ℤ) ↦ ‖f_int k a t a_1‖
have 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)
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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
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)
have 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))
Tactic: rcases n with - | m
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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))
⊢ ‖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)
have 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))
Tactic: rcases n with - | m
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ -(↑(m + 1) : ℝ) + a = -((↑m : ℝ) + (1 - a))
have push_cast : -HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + a = -((↑m : ℝ) + (1 - a))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ -(↑(m + 1) : ℝ) + a = -((↑m : ℝ) + (1 - a))
have ring : -HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + a = -((↑m : ℝ) + (1 - a))
Tactic: { push_cast; ring }
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a : UnitAddCircle
t b : ℝ
⊢ Eq (α := ℝ) ((fun (b : ℝ) ↦ (∑' (n : ℤ), f_int k b t n : ℝ)) (b + 1))
    ((fun (b : ℝ) ↦ (∑' (n : ℤ), f_int k b t n : ℝ)) b)
have simp_rw : Eq (α := ℝ) (∑' (n : ℤ), f_int k (b + 1) t n) (∑' (c : ℤ), f_int k b t ((Equiv.addRight 1 : (a : ℤ) → ℤ) c))
Tactic: simp_rw [← (Equiv.addRight (1 : ℤ)).tsum_eq (f := fun n ↦ f_int k b t n)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
t : ℝ
ht : 0 < t
⊢ ∑' (n : ℤ), f_int k a t n = HAdd.hAdd (α := ℝ) (∑' (n : ℕ), f_nat k a t n) (∑' (n : ℕ), f_nat k (1 - a) t n)
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
t : ℝ
ht : 0 < t
n : ℤ
⊢ f_int k a t n = Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) n
have 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)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
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)
⊢ f_int k a t n = Int.rec (motive := fun (x : ℤ) ↦ ℝ) (f_nat k a t) (f_nat k (1 - a) t) n
have 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)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
t : ℝ
ht : 0 < t
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)
have 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)
Tactic: rw [f_int_ofNat _ ha.1]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
k : ℕ
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Icc 0 1) a
t : ℝ
ht : 0 < t
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)
have 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)
Tactic: rw [f_int_negSucc _ ha.2]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
a : UnitAddCircle
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨a, ha, rfl⟩ := a.eq_coe_Ico
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds (goal)
Goal:
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)
have obtain : ∀ (p : ℝ) (hp : 0 < p)
  (hp' :
    IsBigO (E := ℝ) (F := ℝ) atTop (fun (t : ℝ) ↦ F_nat 0 a t - if a = 0 then 1 else 0) fun (t : ℝ) ↦ rexp (-p * t)),
  ∃ (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)
Tactic: obtain ⟨p, hp, hp'⟩ := isBigO_atTop_F_nat_zero_sub ha.1