awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
rw : HPow.hPow (β := ℕ) n 2 = HPow.hPow (α := ℤ) (β := ℕ) (↑n.natAbs : ℤ) 2
⊢ HPow.hPow (β := ℕ) n 2 = (↑(HPow.hPow (β := ℕ) n.natAbs 2) : ℤ)
have rw₁ : HPow.hPow (β := ℕ) n 2 = HPow.hPow (β := ℕ) n 2
Tactic: rw [Nat.cast_pow, Int.natAbs_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (hypothesis)
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ y ^ HPow.hPow (β := ℕ) n 2 ≤ rexp (-π * τ.im) ^ n.natAbs
have this : HPow.hPow (β := ℕ) n 2 = (↑(HPow.hPow (β := ℕ) n.natAbs 2) : ℤ)
Tactic: have : n ^ 2 = (n.natAbs ^ 2 :) := by rw [Nat.cast_pow, Int.natAbs_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this : HPow.hPow (β := ℕ) n 2 = (↑(HPow.hPow (β := ℕ) n.natAbs 2) : ℤ)
⊢ y ^ HPow.hPow (β := ℕ) n 2 ≤ rexp (-π * τ.im) ^ n.natAbs
have refine_2 : y ^ HPow.hPow (β := ℕ) n.natAbs 2 ≤ rexp (-π * τ.im) ^ n.natAbs
Tactic: rw [this, zpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (hypothesis)
Goal:
τ : ℂ
hτ : 0 < τ.im
⊢ HasSum (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
    ((jacobiTheta τ - 1) / 2)
have this : HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n 0 τ) (jacobiTheta₂ 0 τ)
Tactic: have := hasSum_jacobiTheta₂_term 0 hτ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (hypothesis)
Goal:
τ : ℂ
hτ : 0 < τ.im
this : HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n 0 τ) (jacobiTheta₂ 0 τ)
⊢ HasSum (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
    ((jacobiTheta τ - 1) / 2)
have this₁ : HasSum (fun (n : ℤ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)) (jacobiTheta τ)
Tactic: simp_rw [jacobiTheta₂_term, mul_zero, zero_add, ← jacobiTheta_eq_jacobiTheta₂] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (hypothesis)
Goal:
τ : ℂ
hτ : 0 < τ.im
this : HasSum (fun (n : ℤ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)) (jacobiTheta τ)
⊢ HasSum (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
    ((jacobiTheta τ - 1) / 2)
have this₁ : HasSum
  (fun (n : ℕ) ↦
    cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(↑n : ℤ) : ℂ) 2 * τ) +
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-(↑n : ℤ)) : ℂ) 2 * τ))
  (jacobiTheta τ + cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑0 : ℂ) 2 * τ))
Tactic: have := this.nat_add_neg
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (hypothesis)
Goal:
τ : ℂ
hτ : 0 < τ.im
this_1 : HasSum (fun (n : ℤ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)) (jacobiTheta τ)
this :
  HasSum
    (fun (n : ℕ) ↦
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(↑n : ℤ) : ℂ) 2 * τ) +
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-(↑n : ℤ)) : ℂ) 2 * τ))
    (jacobiTheta τ + cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑0 : ℂ) 2 * τ))
⊢ HasSum (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
    ((jacobiTheta τ - 1) / 2)
have this₁ : HasSum
  (fun (n : ℕ) ↦
    cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(↑(n + 1) : ℤ) : ℂ) 2 * τ) +
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-(↑(n + 1) : ℤ)) : ℂ) 2 * τ))
  (jacobiTheta τ + cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑0 : ℂ) 2 * τ) -
    ∑ i ∈ Finset.range 1,
      (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(↑i : ℤ) : ℂ) 2 * τ) +
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-(↑i : ℤ)) : ℂ) 2 * τ)))
Tactic: rw [← hasSum_nat_add_iff' 1] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (hypothesis)
Goal:
τ : ℂ
hτ : 0 < τ.im
this_1 : HasSum (fun (n : ℤ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)) (jacobiTheta τ)
this :
  HasSum
    (fun (n : ℕ) ↦
      cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(↑(n + 1) : ℤ) : ℂ) 2 * τ) +
        cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-(↑(n + 1) : ℤ)) : ℂ) 2 * τ))
    (jacobiTheta τ + cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑0 : ℂ) 2 * τ) -
      ∑ i ∈ Finset.range 1,
        (cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(↑i : ℤ) : ℂ) 2 * τ) +
          cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑(-(↑i : ℤ)) : ℂ) 2 * τ)))
⊢ HasSum (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
    ((jacobiTheta τ - 1) / 2)
have this₁ : HasSum (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ) * 2)
  (jacobiTheta τ - 1)
Tactic: simp_rw [Finset.sum_range_one, Int.cast_neg, Int.cast_natCast, Nat.cast_zero, neg_zero,
    Int.cast_zero, sq (0 : ℂ), mul_zero, zero_mul, neg_sq, ← mul_two,
    Complex.exp_zero, add_sub_assoc, (by norm_num : (1 : ℂ) - 1 * 2 = -1), ← sub_eq_add_neg,
    Nat.cast_add, Nat.cast_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
this_1 : HasSum (fun (n : ℤ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ) * 2)
    (jacobiTheta τ - 1)
⊢ HasSum (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
    ((jacobiTheta τ - 1) / 2)
have h : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
  fun (i : ℕ) ↦ cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) 2 * τ) * 2 / 2
Tactic: convert! this.div_const 2 using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
⊢ jacobiTheta τ =
    1 +
      HMul.hMul (α := ℂ) 2 (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
have rw : jacobiTheta τ = 1 + 2 * ((jacobiTheta τ - 1) / 2)
Tactic: rw [(hasSum_nat_jacobiTheta hτ).tsum_eq, mul_div_cancel₀ _ (two_ne_zero' ℂ), ← add_sub_assoc,
    add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
rw : jacobiTheta τ = 1 + 2 * ((jacobiTheta τ - 1) / 2)
⊢ jacobiTheta τ =
    1 +
      HMul.hMul (α := ℂ) 2 (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
have rw₁ : jacobiTheta τ = 1 + (jacobiTheta τ - 1)
Tactic: rw [(hasSum_nat_jacobiTheta hτ).tsum_eq, mul_div_cancel₀ _ (two_ne_zero' ℂ), ← add_sub_assoc,
    add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
rw : jacobiTheta τ = 1 + 2 * ((jacobiTheta τ - 1) / 2)
rw₁ : jacobiTheta τ = 1 + (jacobiTheta τ - 1)
⊢ jacobiTheta τ =
    1 +
      HMul.hMul (α := ℂ) 2 (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
have rw₂ : jacobiTheta τ = 1 + jacobiTheta τ - 1
Tactic: rw [(hasSum_nat_jacobiTheta hτ).tsum_eq, mul_div_cancel₀ _ (two_ne_zero' ℂ), ← add_sub_assoc,
    add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
rw : jacobiTheta τ = 1 + 2 * ((jacobiTheta τ - 1) / 2)
rw₁ : jacobiTheta τ = 1 + (jacobiTheta τ - 1)
rw₂ : jacobiTheta τ = 1 + jacobiTheta τ - 1
⊢ jacobiTheta τ =
    1 +
      HMul.hMul (α := ℂ) 2 (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
have rw₃ : jacobiTheta τ = jacobiTheta τ
Tactic: rw [(hasSum_nat_jacobiTheta hτ).tsum_eq, mul_div_cancel₀ _ (two_ne_zero' ℂ), ← add_sub_assoc,
    add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ ‖jacobiTheta τ - 1‖ =
    2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
have rw : ‖HMul.hMul (α := ℂ) 2 (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))‖ =
  2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
Tactic: rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hτ), norm_mul, Complex.norm_two]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
rw :
  ‖HMul.hMul (α := ℂ) 2 (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))‖ =
    2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
⊢ ‖jacobiTheta τ - 1‖ =
    2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
have rw₁ : Norm.norm (E := ℂ) 2 *
    Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) =
  2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
Tactic: rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hτ), norm_mul, Complex.norm_two]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
rw :
  ‖HMul.hMul (α := ℂ) 2 (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))‖ =
    2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
rw₁ :
  Norm.norm (E := ℂ) 2 *
      Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) =
    2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
⊢ ‖jacobiTheta τ - 1‖ =
    2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
have rw₂ : 2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) =
  2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
Tactic: rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hτ), norm_mul, Complex.norm_two]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ 2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))
have ha : LE.le (α := ℝ) 0 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)
have rw : 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) = rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) * 2
Tactic: rw [div_mul_comm, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
rw : 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) = rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) * 2
⊢ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)
have rw₁ : rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) * 2 = rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) * 2
Tactic: rw [div_mul_comm, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ ‖jacobiTheta τ - 1‖ ≤ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)
have τ₁ : ‖jacobiTheta τ - 1‖ =
  2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
Tactic: calc
      ‖jacobiTheta τ - 1‖ = ↑2 * ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ := by
        rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hτ), norm_mul, Complex.norm_two]
      _ ≤ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) := by gcongr
      _ = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) := by rw [div_mul_comm, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
τ₁ :
  ‖jacobiTheta τ - 1‖ =
    2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
⊢ ‖jacobiTheta τ - 1‖ ≤ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)
have τ₂ : 2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
  2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))
Tactic: calc
      ‖jacobiTheta τ - 1‖ = ↑2 * ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ := by
        rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hτ), norm_mul, Complex.norm_two]
      _ ≤ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) := by gcongr
      _ = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) := by rw [div_mul_comm, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
τ₁ :
  ‖jacobiTheta τ - 1‖ =
    2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ))
τ₂ :
  2 * Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))
⊢ ‖jacobiTheta τ - 1‖ ≤ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)
have τ₃ : 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)
Tactic: calc
      ‖jacobiTheta τ - 1‖ = ↑2 * ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ := by
        rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hτ), norm_mul, Complex.norm_two]
      _ ≤ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) := by gcongr
      _ = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) := by rw [div_mul_comm, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
⊢ ‖jacobiTheta τ - 1‖ ≤ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)
have suffices : Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
  rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
Tactic: suffices ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ ≤
      rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) by
    calc
      ‖jacobiTheta τ - 1‖ = ↑2 * ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ := by
        rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hτ), norm_mul, Complex.norm_two]
      _ ≤ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) := by gcongr
      _ = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) := by rw [div_mul_comm, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (hypothesis)
Goal:
τ : ℂ
hτ : 0 < τ.im
⊢ Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
have this : ∀ (n : ℕ), ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
Tactic: have : ∀ n : ℕ, ‖cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1) := by
    intro n
    simpa only [Int.cast_add, Int.cast_one] using norm_exp_mul_sq_le hτ (n + 1)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℕ),
    ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
⊢ HasSum (fun (n : ℕ) ↦ rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))
have simp_rw : HasSum (HPow.hPow (rexp (-π * τ.im))) (1 - rexp (-π * τ.im))⁻¹
Tactic: simp_rw [pow_succ', div_eq_mul_inv, hasSum_mul_left_iff (Real.exp_ne_zero _)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (hypothesis)
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℕ),
    ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
⊢ Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
have s : HasSum (fun (n : ℕ) ↦ rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))
Tactic: have s : HasSum (fun n : ℕ =>
      rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) := by
    simp_rw [pow_succ', div_eq_mul_inv, hasSum_mul_left_iff (Real.exp_ne_zero _)]
    exact hasSum_geometric_of_lt_one (exp_pos (-π * τ.im)).le
      (exp_lt_one_iff.mpr <| mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hτ)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (hypothesis)
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℕ),
    ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
s : HasSum (fun (n : ℕ) ↦ rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))
⊢ Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
have aux : Summable (α := ℝ) fun (n : ℕ) ↦ ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖
Tactic: have aux : Summable fun n : ℕ => ‖cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ :=
    .of_nonneg_of_le (fun n => norm_nonneg _) this s.summable
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
⊢ IsBigO (E := ℂ) (F := ℝ) (comap im atTop) (fun (τ : ℂ) ↦ jacobiTheta τ - 1) fun (τ : ℂ) ↦ rexp (-π * τ.im)
have simp_rw : ∃ (c : ℝ) (a : ℝ), ∀ b ≥ a, ∀ (a : ℂ), a.im = b → ‖jacobiTheta a - 1‖ ≤ c * ‖rexp (-π * a.im)‖
Tactic: simp_rw [IsBigO, IsBigOWith, Filter.eventually_comap, Filter.eventually_atTop]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
⊢ ∃ (c : ℝ) (a : ℝ), ∀ b ≥ a, ∀ (a : ℂ), a.im = b → ‖jacobiTheta a - 1‖ ≤ c * ‖rexp (-π * a.im)‖
have refine : ∀ (y : ℝ) (hy : y ≥ 1) (τ : ℂ) (hτ : τ.im = y),
  2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) ≤ 2 / (1 - rexp (-(π * 1))) * ‖rexp (-π * τ.im)‖
Tactic: refine ⟨2 / (1 - rexp (-(π * 1))), 1, fun y hy τ hτ =>
    (norm_jacobiTheta_sub_one_le (hτ.symm ▸ zero_lt_one.trans_le hy : 0 < im τ)).trans ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
y : ℝ
hy : y ≥ 1
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) ≤ 2 / (1 - rexp (-(π * 1))) * ‖rexp (-π * τ.im)‖
have rw : 2 / (1 - rexp (-(π * y))) * rexp (-(π * y)) ≤ 2 / (1 - rexp (-(π * 1))) * rexp (-(π * y))
Tactic: rw [Real.norm_eq_abs, Real.abs_exp, hτ, neg_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
y : ℝ
hy : y ≥ 1
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-(π * y))) * rexp (-(π * y)) ≤ 2 / (1 - rexp (-(π * 1))) * rexp (-(π * y))
have hbc : 0 < 1 - rexp (-(π * 1))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable (goal)
Goal:
τ : ℂ
hτ : 0 < τ.im
⊢ DifferentiableAt ℂ jacobiTheta τ
have simp_rw : DifferentiableAt ℂ (jacobiTheta₂ 0) τ
Tactic: simp_rw [funext jacobiTheta_eq_jacobiTheta₂]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
f : ℂ × ℂ → ℂ :=
  fun (p : ℂ × ℂ) ↦ 2 * (↑π : ℂ) * I * (↑n : ℂ) * p.1 + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * p.2
⊢ HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2) (jacobiTheta₂_term_fderiv n z τ) (z, τ)
have suffices : HasFDerivAt f
  (HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
    HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)
      (ContinuousLinearMap.snd ℂ ℂ ℂ))
  (z, τ)
Tactic: suffices HasFDerivAt f ((2 * π * I * n) • (ContinuousLinearMap.fst ℂ ℂ ℂ)
    + (π * I * n ^ 2) • (ContinuousLinearMap.snd ℂ ℂ ℂ)) (z, τ) from this.cexp
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ =
    (↑(π * HMul.hMul (α := ℝ) 2 (↑n : ℝ)) : ℂ) * z * I + (↑(π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2) : ℂ) * τ * I
have push_cast : 2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ =
  (↑π : ℂ) * HMul.hMul (α := ℂ) 2 (↑n : ℂ) * z * I + (↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ * I
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
⊢ ‖jacobiTheta₂_term n z τ‖ = rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im)
have rw : rexp (-(π * HMul.hMul (α := ℝ) 2 (↑n : ℝ) * z.im) + -(π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im)) =
  rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im)
Tactic: rw [jacobiTheta₂_term, Complex.norm_exp, (by push_cast; ring :
    (2 * π : ℂ) * I * n * z + π * I * n ^ 2 * τ = (π * (2 * n) :) * z * I + (π * n ^ 2 :) * τ * I),
    add_re, mul_I_re, im_ofReal_mul, mul_I_re, im_ofReal_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
have simp_rw : HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * T + -(2 * S * (↑|n| : ℝ)) ≤
  HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im + HMul.hMul (α := ℝ) 2 (↑n : ℝ) * z.im
Tactic: simp_rw [norm_jacobiTheta₂_term, Real.exp_le_exp, sub_eq_add_neg, neg_mul, ← neg_add,
    neg_le_neg_iff, mul_comm (2 : ℝ), mul_assoc π, ← mul_add, mul_le_mul_iff_right₀ pi_pos,
    mul_comm T, mul_comm S]