awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 3 * π * (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖) ≤
    3 * π *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
        rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ))))
have mpr : HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖ ≤
  HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
    rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ)))
Tactic: refine mul_le_mul_of_nonneg_left ?_ (mul_pos (by simp : 0 < (3 : ℝ)) pi_pos).le
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖ ≤
    HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ)))
have mpr : ‖jacobiTheta₂_term n z τ‖ ≤ rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ)))
Tactic: refine mul_le_mul_of_nonneg_left ?_ (pow_nonneg (Int.cast_nonneg (abs_nonneg _)) _)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) ↔ 0 < τ.im
have mp : (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) → 0 < τ.im
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
mp : (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) → 0 < τ.im
⊢ (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) ↔ 0 < τ.im
have mpr : 0 < τ.im → Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) → 0 < τ.im
have mp : (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) → Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
Tactic: rw [← summable_jacobiTheta₂_term_iff (z := z)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) → Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
have mp : ∀ (h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ),
  ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term i z τ‖
Tactic: refine fun h ↦ (h.norm.mul_left (2 * π)⁻¹).of_norm_bounded_eventually ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term i z τ‖
have this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
Tactic: have : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0 :=
      Int.cofinite_eq ▸ (mem_sup.mpr ⟨eventually_ne_atBot 0, eventually_ne_atTop 0⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term i z τ‖
have h₁ : ∀ (n : ℤ) (hn : n ≠ 0), ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term n z τ‖
Tactic: filter_upwards [this] with n hn
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term n z τ‖
have h₁ : ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ * ‖jacobiTheta₂_term n z τ‖
Tactic: rw [jacobiTheta₂'_term, norm_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ * ‖jacobiTheta₂_term n z τ‖
have h₁ : 1 ≤ (2 * π)⁻¹ * ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖
Tactic: refine le_mul_of_one_le_left (norm_nonneg _) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ (2 * π)⁻¹ * ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖
have h₁ : LE.le (α := ℝ) 1 (↑|n| : ℝ)
Tactic: simp_rw [norm_mul, norm_I, norm_real, mul_one, norm_of_nonneg pi_pos.le,
      ← ofReal_ofNat, norm_real, norm_of_nonneg two_pos.le, ← ofReal_intCast, norm_real,
      Real.norm_eq_abs, ← Int.cast_abs, ← mul_assoc _ (2 * π),
      inv_mul_cancel₀ (mul_pos two_pos pi_pos).ne', one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ LE.le (α := ℝ) 1 (↑|n| : ℝ)
have h₁ : 1 ≤ |n|
Tactic: rw [← Int.cast_one, Int.cast_le]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ 0 < τ.im → Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
have mpr : ∀ (hτ : 0 < τ.im) (n : ℤ),
  ‖jacobiTheta₂'_term n z τ‖ ≤
    2 * π *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 1 *
        rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ))))
Tactic: refine fun hτ ↦ ((summable_pow_mul_jacobiTheta₂_term_bound
      |z.im| hτ 1).mul_left (2 * π)).of_norm_bounded (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖jacobiTheta₂'_term n z τ‖ ≤
    2 * π *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 1 *
        rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ))))
have mpr : ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ * ‖jacobiTheta₂_term n z τ‖ ≤
  2 * π * (↑|n| : ℝ) * rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ)))
Tactic: rw [jacobiTheta₂'_term, norm_mul, ← mul_assoc, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ * ‖jacobiTheta₂_term n z τ‖ ≤
    2 * π * (↑|n| : ℝ) * rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ)))
have mpr : ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ = 2 * π * (↑|n| : ℝ)
Tactic: refine mul_le_mul (le_of_eq ?_) (norm_jacobiTheta₂_term_le hτ le_rfl le_rfl n)
      (norm_nonneg _) (by positivity)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ = 2 * π * (↑|n| : ℝ)
have mpr : Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * ‖I‖ * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
Tactic: simp_rw [norm_mul, Complex.norm_two, norm_I, Complex.norm_of_nonneg pi_pos.le,
      norm_intCast, mul_one, Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
mpr : Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * ‖I‖ * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
⊢ ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ = 2 * π * (↑|n| : ℝ)
have mpr₁ : 2 * ‖(↑π : ℂ)‖ * ‖I‖ * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
Tactic: simp_rw [norm_mul, Complex.norm_two, norm_I, Complex.norm_of_nonneg pi_pos.le,
      norm_intCast, mul_one, Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
mpr : Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * ‖I‖ * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
mpr₁ : 2 * ‖(↑π : ℂ)‖ * ‖I‖ * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
⊢ ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ = 2 * π * (↑|n| : ℝ)
have mpr₂ : 2 * ‖(↑π : ℂ)‖ * 1 * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
Tactic: simp_rw [norm_mul, Complex.norm_two, norm_I, Complex.norm_of_nonneg pi_pos.le,
      norm_intCast, mul_one, Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
mpr : Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * ‖I‖ * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
mpr₁ : 2 * ‖(↑π : ℂ)‖ * ‖I‖ * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
mpr₂ : 2 * ‖(↑π : ℂ)‖ * 1 * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
⊢ ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ = 2 * π * (↑|n| : ℝ)
have mpr₃ : 2 * π * 1 * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
Tactic: simp_rw [norm_mul, Complex.norm_two, norm_I, Complex.norm_of_nonneg pi_pos.le,
      norm_intCast, mul_one, Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
mpr : Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * ‖I‖ * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
mpr₁ : 2 * ‖(↑π : ℂ)‖ * ‖I‖ * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
mpr₂ : 2 * ‖(↑π : ℂ)‖ * 1 * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
mpr₃ : 2 * π * 1 * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
⊢ ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ = 2 * π * (↑|n| : ℝ)
have mpr₄ : 2 * π * 1 * |(↑n : ℝ)| = 2 * π * (↑|n| : ℝ)
Tactic: simp_rw [norm_mul, Complex.norm_two, norm_I, Complex.norm_of_nonneg pi_pos.le,
      norm_intCast, mul_one, Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
mpr : Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * ‖I‖ * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
mpr₁ : 2 * ‖(↑π : ℂ)‖ * ‖I‖ * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
mpr₂ : 2 * ‖(↑π : ℂ)‖ * 1 * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
mpr₃ : 2 * π * 1 * Norm.norm (E := ℂ) (↑n : ℂ) = 2 * π * (↑|n| : ℝ)
mpr₄ : 2 * π * 1 * |(↑n : ℝ)| = 2 * π * (↑|n| : ℝ)
⊢ ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ = 2 * π * (↑|n| : ℝ)
have mpr₅ : 2 * π * |(↑n : ℝ)| = 2 * π * (↑|n| : ℝ)
Tactic: simp_rw [norm_mul, Complex.norm_two, norm_I, Complex.norm_of_nonneg pi_pos.le,
      norm_intCast, mul_one, Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂ z τ = 0
have h : ¬Summable (α := ℂ) fun (b : ℤ) ↦ jacobiTheta₂_term b z τ
Tactic: apply tsum_eq_zero_of_not_summable
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬Summable (α := ℂ) fun (b : ℤ) ↦ jacobiTheta₂_term b z τ
have h : ¬0 < τ.im
Tactic: rw [summable_jacobiTheta₂_term_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂_fderiv z τ = 0
have h : ¬Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (b : ℤ) ↦ jacobiTheta₂_term_fderiv b z τ
Tactic: apply tsum_eq_zero_of_not_summable
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (b : ℤ) ↦ jacobiTheta₂_term_fderiv b z τ
have h : ¬0 < τ.im
Tactic: rw [summable_jacobiTheta₂_term_fderiv_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂' z τ = 0
have h : ¬Summable (α := ℂ) fun (b : ℤ) ↦ jacobiTheta₂'_term b z τ
Tactic: apply tsum_eq_zero_of_not_summable
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬Summable (α := ℂ) fun (b : ℤ) ↦ jacobiTheta₂'_term b z τ
have h : ¬0 < τ.im
Tactic: rw [summable_jacobiTheta₂'_term_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
have obtain : ∀ (T : ℝ) (hT : 0 < T) (hτ' : T < τ.im),
  HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
Tactic: obtain ⟨T, hT, hτ'⟩ := exists_between hτ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
⊢ HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
have obtain : ∀ (S : ℝ) (hz : |z.im| < S), HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
Tactic: obtain ⟨S, hz⟩ := exists_gt |im z|
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
⊢ IsOpen V
have refine : IsOpen (X := ℂ) {v : ℂ | T < v.im}
Tactic: refine ((_root_.continuous_abs.comp continuous_im).isOpen_preimage _ isOpen_Iio).prod ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
⊢ HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
have hVo : IsOpen V
Tactic: have hVo : IsOpen V := by
    refine ((_root_.continuous_abs.comp continuous_im).isOpen_preimage _ isOpen_Iio).prod ?_
    exact continuous_im.isOpen_preimage _ isOpen_Ioi
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
⊢ HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
have hVmem : (z, τ) ∈ V
Tactic: have hVmem : (z, τ) ∈ V := ⟨hz, hτ'⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
⊢ IsPreconnected V
have refine : Convex ℝ (E := ℂ) {u : ℂ | |u.im| < S}
Tactic: refine (Convex.isPreconnected ?_).prod (convex_halfSpace_im_gt T).isPreconnected
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
⊢ HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
have hVp : IsPreconnected V
Tactic: have hVp : IsPreconnected V := by
    refine (Convex.isPreconnected ?_).prod (convex_halfSpace_im_gt T).isPreconnected
    simpa only [abs_lt] using (convex_halfSpace_im_gt _).inter (convex_halfSpace_im_lt _)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
⊢ HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
have hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
Tactic: have hf (n : ℤ) : ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p :=
    fun p _ ↦ hasFDerivAt_jacobiTheta₂_term n p.1 p.2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
⊢ ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
have refine : ∀ (n : ℤ) (p : ℂ × ℂ) (hp : p ∈ V),
  3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n p.1 p.2‖ ≤ u n
Tactic: refine fun n p hp ↦ (norm_jacobiTheta₂_term_fderiv_le n p.1 p.2).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
n : ℤ
p : ℂ × ℂ
hp : p ∈ V
⊢ 3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n p.1 p.2‖ ≤ u n
have refine : ‖jacobiTheta₂_term n p.1 p.2‖ ≤ rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
Tactic: refine mul_le_mul_of_nonneg_left ?_ (by positivity)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
⊢ HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
have hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
Tactic: have hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n := by
    refine fun n p hp ↦ (norm_jacobiTheta₂_term_fderiv_le n p.1 p.2).trans ?_
    refine mul_le_mul_of_nonneg_left ?_ (by positivity)
    exact norm_jacobiTheta₂_term_le hT (le_of_lt hp.1) (le_of_lt hp.2) n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
⊢ Summable u
have simp_rw : Summable (α := ℝ) fun (n : ℤ) ↦
  3 * π *
    (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ))))
Tactic: simp_rw [u, mul_assoc (3 * π)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
⊢ HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
have hu_sum : Summable u
Tactic: have hu_sum : Summable u := by
    simp_rw [u, mul_assoc (3 * π)]
    exact (summable_pow_mul_jacobiTheta₂_term_bound S hT 2).mul_left _
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ f n (z, τ)
have refine : ∀ (i : ℤ),
  ‖f i (z, τ)‖ ≤
    HPow.hPow (α := ℝ) (β := ℕ) (↑|i| : ℝ) 0 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 - 2 * S * (↑|i| : ℝ)))
Tactic: refine (summable_pow_mul_jacobiTheta₂_term_bound S hT 0).of_norm_bounded ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := SProd.sprod (α := Set ℂ) (β := Set ℂ) {u : ℂ | |u.im| < S} {v : ℂ | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun (n : ℤ) (p : ℂ × ℂ) ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ :=
  fun (n : ℤ) ↦
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
⊢ HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
have hf_sum : Summable (α := ℂ) fun (n : ℤ) ↦ f n (z, τ)
Tactic: have hf_sum : Summable fun n : ℤ ↦ f n (z, τ) := by
    refine (summable_pow_mul_jacobiTheta₂_term_bound S hT 0).of_norm_bounded ?_
    simpa only [pow_zero, one_mul] using norm_jacobiTheta₂_term_le hT hz.le hτ'.le
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
  { toFun := fun (f : ℂ × ℂ →L[ℂ] ℂ) ↦ (f : (a : ℂ × ℂ) → ℂ) (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasDerivAt (fun (x : ℂ) ↦ jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
have step1 : HasSum (α := ℂ) (fun (n : ℤ) ↦ ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ))
  ((jacobiTheta₂_fderiv z τ : (a : ℂ × ℂ) → ℂ) (1, 0) : ℂ)
Tactic: have step1 : HasSum (fun n ↦ (jacobiTheta₂_term_fderiv n z τ) (1, 0))
      ((jacobiTheta₂_fderiv z τ) (1, 0)) := by
    apply eval_fst_CLM.hasSum (hasSum_jacobiTheta₂_term_fderiv z hτ)