awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℤ
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * T + -(2 * S * (↑|n| : ℝ)) ≤
    HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im + HMul.hMul (α := ℝ) 2 (↑n : ℝ) * z.im
have refine : -(2 * S * (↑|n| : ℝ)) ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ) * z.im
Tactic: refine add_le_add (mul_le_mul le_rfl hτ hT.le (sq_nonneg _)) ?_
-- 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 : ℤ
⊢ -(2 * S * (↑|n| : ℝ)) ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ) * z.im
have rw : (↑|n| : ℝ) * -S ≤ (↑n : ℝ) * z.im
Tactic: rw [← mul_neg, mul_assoc, mul_assoc, mul_le_mul_iff_right₀ two_pos, mul_comm, neg_mul, ← mul_neg]
-- 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 : ℤ
⊢ (↑|n| : ℝ) * -S ≤ (↑n : ℝ) * z.im
have refine : (↑|n| : ℝ) * -S ≤ -|(↑n : ℝ) * z.im|
Tactic: refine le_trans ?_ (neg_abs_le _)
-- 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 : ℤ
⊢ (↑|n| : ℝ) * -S ≤ -|(↑n : ℝ) * z.im|
have rw : |(↑n : ℝ)| * |z.im| ≤ |(↑n : ℝ)| * S
Tactic: rw [mul_neg, neg_le_neg_iff, abs_mul, Int.cast_abs]
-- 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 τ‖ ≤
    2 * π * (↑|n| : ℝ) * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
have rw : ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ * ‖jacobiTheta₂_term n z τ‖ ≤
  2 * π * (↑|n| : ℝ) * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
Tactic: rw [jacobiTheta₂'_term, norm_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 : ℤ
⊢ ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ * ‖jacobiTheta₂_term n z τ‖ ≤
    2 * π * (↑|n| : ℝ) * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
have refine : ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ = 2 * π * (↑|n| : ℝ)
Tactic: refine mul_le_mul (le_of_eq ?_) (norm_jacobiTheta₂_term_le hT hz hτ n)
    (norm_nonneg _) (by positivity)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
this :
  Summable (α := ℝ) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑n : ℝ)))
⊢ Summable (α := ℝ) fun (n : ℤ) ↦
    HPow.hPow (α := ℝ) (↑|n| : ℝ) k * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
have hf₁ : Summable (α := ℝ) fun (n : ℕ) ↦
  HPow.hPow (α := ℝ) (↑|(↑n : ℤ)| : ℝ) k *
    rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 - 2 * S * (↑|(↑n : ℤ)| : ℝ)))
Tactic: apply Summable.of_nat_of_neg
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
this :
  Summable (α := ℝ) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑n : ℝ)))
hf₁ :
  Summable (α := ℝ) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑|(↑n : ℤ)| : ℝ) k *
      rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑(↑n : ℤ) : ℝ) 2 - 2 * S * (↑|(↑n : ℤ)| : ℝ)))
⊢ Summable (α := ℝ) fun (n : ℤ) ↦
    HPow.hPow (α := ℝ) (↑|n| : ℝ) k * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
have hf₂ : Summable (α := ℝ) fun (n : ℕ) ↦
  HPow.hPow (α := ℝ) (↑|(-(↑n : ℤ))| : ℝ) k *
    rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑(-(↑n : ℤ)) : ℝ) 2 - 2 * S * (↑|(-(↑n : ℤ))| : ℝ)))
Tactic: apply Summable.of_nat_of_neg
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Summable (α := ℝ) fun (n : ℤ) ↦
    HPow.hPow (α := ℝ) (↑|n| : ℝ) k * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))
have suffices : Summable (α := ℝ) fun (n : ℕ) ↦
  HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑n : ℝ)))
Tactic: suffices Summable (fun n : ℕ ↦ (n ^ k : ℝ) * Real.exp (-π * (T * n ^ 2 - 2 * S * n))) by
    apply Summable.of_nat_of_neg <;>
    simpa only [Int.cast_neg, neg_sq, abs_neg, Int.cast_natCast, Nat.abs_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑n : ℝ)))
have apply : IsBigO (E := ℝ) (F := ℝ) atTop
  (fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑n : ℝ))))
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (HMul.hMul (α := ℝ) (-1) (↑n : ℝ))
Tactic: apply summable_of_isBigO_nat (summable_pow_mul_exp_neg_nat_mul k zero_lt_one)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑n : ℝ))))
    fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (HMul.hMul (α := ℝ) (-1) (↑n : ℝ))
have apply : IsBigO (E := ℝ) (F := ℝ) atTop
  (fun (x : ℕ) ↦ rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)))) fun (x : ℕ) ↦
  rexp (HMul.hMul (α := ℝ) (-1) (↑x : ℝ))
Tactic: apply IsBigO.mul (isBigO_refl _ _)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (x : ℕ) ↦ rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)))) fun (x : ℕ) ↦
    rexp (HMul.hMul (α := ℝ) (-1) (↑x : ℝ))
have refine : Tendsto
  (HSub.hSub (α := ℕ → ℝ) (fun (x : ℕ) ↦ -π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)))
    fun (x : ℕ) ↦ HMul.hMul (α := ℝ) (-1) (↑x : ℝ))
  atTop atBot
Tactic: refine Real.isBigO_exp_comp_exp_comp.mpr (Tendsto.isBoundedUnder_le_atBot ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto
    (HSub.hSub (α := ℕ → ℝ) (fun (x : ℕ) ↦ -π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)))
      fun (x : ℕ) ↦ HMul.hMul (α := ℝ) (-1) (↑x : ℝ))
    atTop atBot
have simp_rw : Tendsto (β := ℝ)
  (fun (x : ℕ) ↦
    -(-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)) - HMul.hMul (α := ℝ) (-1) (↑x : ℝ)))
  atTop atTop
Tactic: simp_rw [← tendsto_neg_atTop_iff, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
| Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      -(-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)) - HMul.hMul (α := ℝ) (-1) (↑x : ℝ)))
    atTop atTop
have h : ∀ (n : ℕ), -(-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑n : ℝ)) - HMul.hMul (α := ℝ) (-1) (↑n : ℝ))
Tactic: enter [1, n]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
S T : ℝ
hT : 0 < T
k n : ℕ
| -(-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑n : ℝ)) - HMul.hMul (α := ℝ) (-1) (↑n : ℝ))
have h : (↑n : ℝ) * (π * T * (↑n : ℝ) - (2 * π * S + 1))
Tactic: rw [show -(-π * (T * n ^ 2 - 2 * S * n) - -1 * n) = n * (π * T * n - (2 * π * S + 1)) by ring]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
| Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      -(-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)) - HMul.hMul (α := ℝ) (-1) (↑x : ℝ)))
    atTop atTop
have h : ∀ (n : ℕ), (↑n : ℝ) * (π * T * (↑n : ℝ) - (2 * π * S + 1))
Tactic: enter [1, n]
    rw [show -(-π * (T * n ^ 2 - 2 * S * n) - -1 * n) = n * (π * T * n - (2 * π * S + 1)) by ring]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      -(-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)) - HMul.hMul (α := ℝ) (-1) (↑x : ℝ)))
    atTop atTop
have conv : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) * (π * T * (↑n : ℝ) - (2 * π * S + 1))) atTop atTop
Tactic: conv =>
    enter [1, n]
    rw [show -(-π * (T * n ^ 2 - 2 * S * n) - -1 * n) = n * (π * T * n - (2 * π * S + 1)) by ring]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) * (π * T * (↑n : ℝ) - (2 * π * S + 1))) atTop atTop
have refine : Tendsto (β := ℝ) (fun (n : ℕ) ↦ π * T * (↑n : ℝ)) atTop atTop
Tactic: refine tendsto_natCast_atTop_atTop.atTop_mul_atTop₀ (tendsto_atTop_add_const_right _ _ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
⊢ (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ) ↔ 0 < τ.im
have refine_1 : ∀ (hτ : 0 < τ.im), Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
Tactic: refine Iff.symm ⟨fun hτ ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
refine_1 : ∀ (hτ : 0 < τ.im), Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
⊢ (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ) ↔ 0 < τ.im
have refine_2 : ∀ (h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ), 0 < τ.im
Tactic: refine Iff.symm ⟨fun hτ ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
have refine_1 : ∀ (i : ℤ),
  ‖jacobiTheta₂_term i z τ‖ ≤
    HPow.hPow (α := ℝ) (β := ℕ) (↑|i| : ℝ) 0 *
      rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 - 2 * |z.im| * (↑|i| : ℝ)))
Tactic: refine (summable_pow_mul_jacobiTheta₂_term_bound |im z| hτ 0).of_norm_bounded ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
⊢ 0 < τ.im
have refine_2 : ∀ (hτ : τ.im ≤ 0), False
Tactic: by_contra! hτ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ : τ.im ≤ 0
⊢ False
have refine_2 : ∀ (hτ : τ.im < 0), False
Tactic: rcases lt_or_eq_of_le hτ with hτ | hτ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ : τ.im ≤ 0
refine_2 : ∀ (hτ : τ.im < 0), False
⊢ False
have refine_2₁ : ∀ (hτ : τ.im = 0), False
Tactic: rcases lt_or_eq_of_le hτ with hτ | hτ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖jacobiTheta₂_term (↑n : ℤ) z τ‖) atTop atTop
⊢ False
have h₁ : Tendsto (fun (x : ℕ) ↦ Norm.norm (E := ℂ) (((fun (x : ℤ) ↦ jacobiTheta₂_term x z τ) ∘ fun (a : ℕ) ↦ (↑a : ℤ)) x)) atTop
  (𝓝 (Norm.norm (E := ℂ) 0))
Tactic: replace h := (h.comp_injective (fun a b ↦ Int.ofNat_inj.mp)).tendsto_atTop_zero.norm
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
⊢ False
have refine_2 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖jacobiTheta₂_term (↑n : ℤ) z τ‖) atTop atTop
Tactic: suffices Tendsto (fun n : ℕ ↦ ‖jacobiTheta₂_term ↑n z τ‖) atTop atTop by
        replace h := (h.comp_injective (fun a b ↦ Int.ofNat_inj.mp)).tendsto_atTop_zero.norm
        exact atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop _) this)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖jacobiTheta₂_term (↑n : ℤ) z τ‖) atTop atTop
have refine_2 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im))
  atTop atTop
Tactic: simp only [norm_jacobiTheta₂_term, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
| Tendsto (β := ℝ) (fun (n : ℕ) ↦ rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im))
    atTop atTop
have h₁ : ∀ (n : ℕ), rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im)
Tactic: enter [1, n]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
n : ℕ
| rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im)
have h₁ : rexp ((↑n : ℝ) * ((↑n : ℝ) * (-π * τ.im) - 2 * π * z.im))
Tactic: rw [show -π * n ^ 2 * τ.im - 2 * π * n * z.im =
              n * (n * (-π * τ.im) - 2 * π * z.im) by ring]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
| Tendsto (β := ℝ) (fun (n : ℕ) ↦ rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im))
    atTop atTop
have h₁ : ∀ (n : ℕ), rexp ((↑n : ℝ) * ((↑n : ℝ) * (-π * τ.im) - 2 * π * z.im))
Tactic: enter [1, n]
        rw [show -π * n ^ 2 * τ.im - 2 * π * n * z.im =
              n * (n * (-π * τ.im) - 2 * π * z.im) by ring]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im))
    atTop atTop
have refine_2 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ rexp ((↑n : ℝ) * ((↑n : ℝ) * (-π * τ.im) - 2 * π * z.im))) atTop atTop
Tactic: conv =>
        enter [1, n]
        rw [show -π * n ^ 2 * τ.im - 2 * π * n * z.im =
              n * (n * (-π * τ.im) - 2 * π * z.im) by ring]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im < 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ rexp ((↑n : ℝ) * ((↑n : ℝ) * (-π * τ.im) - 2 * π * z.im))) atTop atTop
have refine_2 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑n : ℝ) * (-π * τ.im) - 2 * π * z.im) atTop atTop
Tactic: refine tendsto_exp_atTop.comp (tendsto_natCast_atTop_atTop.atTop_mul_atTop₀ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
⊢ False
have h₁ : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))
Tactic: simp_rw [← summable_norm_iff (E := ℂ), norm_jacobiTheta₂_term, hτ, mul_zero, zero_sub] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))
⊢ False
have refine_2 : ∀ (hz : z.im < 0), False
Tactic: rcases lt_trichotomy (im z) 0 with hz | hz | hz
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))
refine_2 : ∀ (hz : z.im < 0), False
⊢ False
have refine_2₁ : ∀ (hz : z.im = 0), False
Tactic: rcases lt_trichotomy (im z) 0 with hz | hz | hz
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))
refine_2 : ∀ (hz : z.im < 0), False
refine_2₁ : ∀ (hz : z.im = 0), False
⊢ False
have refine_2₂ : ∀ (hz : 0 < z.im), False
Tactic: rcases lt_trichotomy (im z) 0 with hz | hz | hz
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))
hz : z.im < 0
⊢ False
have h₁ : Tendsto (α := ℕ) (β := ℝ) ((fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) ∘ fun (a : ℕ) ↦ (↑a : ℤ)) atTop (𝓝 0)
Tactic: replace h := (h.comp_injective (fun a b ↦ Int.ofNat_inj.mp)).tendsto_atTop_zero
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (α := ℕ) (β := ℝ) ((fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) ∘ fun (a : ℕ) ↦ (↑a : ℤ)) atTop (𝓝 0)
⊢ False
have h₁ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop (𝓝 0)
Tactic: simp_rw [Function.comp_def, Int.cast_natCast] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop (𝓝 0)
⊢ False
have refine_2 : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop atTop
Tactic: refine atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop 0) ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop atTop
have refine_2 : Tendsto (β := ℝ) (fun (x : ℕ) ↦ -(2 * π * (↑x : ℝ) * z.im)) atTop atTop
Tactic: refine tendsto_exp_atTop.comp ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ -(2 * π * (↑x : ℝ) * z.im)) atTop atTop
have refine_2 : Tendsto (β := ℝ) (fun (x : ℕ) ↦ 2 * (π * ((↑x : ℝ) * z.im))) atTop atBot
Tactic: simp only [tendsto_neg_atTop_iff, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ 2 * (π * ((↑x : ℝ) * z.im))) atTop atBot
have refine_2 : Tendsto (β := ℝ) (fun (x : ℕ) ↦ π * ((↑x : ℝ) * z.im)) atTop atBot
Tactic: apply Filter.Tendsto.const_mul_atBot two_pos
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))
hz : z.im = 0
⊢ False
have refine_2 : ∀ (h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))), False
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))
hz : 0 < z.im
⊢ False
have this : Function.Injective (β := ℤ) fun (x : ℕ) ↦ -(↑x : ℤ)
Tactic: have : ((-↑·) : ℕ → ℤ).Injective := fun _ _ ↦ by simp only [neg_inj, Nat.cast_inj, imp_self]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
h : Summable (α := ℝ) fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))
hz : 0 < z.im
this : Function.Injective (β := ℤ) fun (x : ℕ) ↦ -(↑x : ℤ)
⊢ False
have h₁ : Tendsto (α := ℕ) (β := ℝ) ((fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) ∘ fun (x : ℕ) ↦ -(↑x : ℤ)) atTop (𝓝 0)
Tactic: replace h := (h.comp_injective this).tendsto_atTop_zero
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : 0 < z.im
this : Function.Injective (β := ℤ) fun (x : ℕ) ↦ -(↑x : ℤ)
h : Tendsto (α := ℕ) (β := ℝ) ((fun (x : ℤ) ↦ rexp (-(2 * π * (↑x : ℝ) * z.im))) ∘ fun (x : ℕ) ↦ -(↑x : ℤ)) atTop (𝓝 0)
⊢ False
have h₁ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (2 * π * (↑x : ℝ) * z.im)) atTop (𝓝 0)
Tactic: simp_rw [Function.comp_def, Int.cast_neg, Int.cast_natCast, mul_neg, neg_mul, neg_neg] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
z τ : ℂ
hτ_1 : τ.im ≤ 0
hτ : τ.im = 0
hz : 0 < z.im
this : Function.Injective (β := ℤ) fun (x : ℕ) ↦ -(↑x : ℤ)
h : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (2 * π * (↑x : ℝ) * z.im)) atTop (𝓝 0)
⊢ False
have refine_2 : Tendsto (β := ℝ) (fun (x : ℕ) ↦ rexp (2 * π * (↑x : ℝ) * z.im)) atTop atTop
Tactic: refine atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop 0) ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (hypothesis)
Goal:
n : ℤ
z τ : ℂ
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ ≤ 3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖
have hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
Tactic: have hns (a : ℂ) (f : (ℂ × ℂ) →L[ℂ] ℂ) : ‖a • f‖ = ‖a‖ * ‖f‖ := norm_smul a f
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ ≤ 3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖
have rw : ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
    ‖HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
        HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)
          (ContinuousLinearMap.snd ℂ ℂ ℂ)‖ ≤
  ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
    (2 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 + 1 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2)
Tactic: rw [jacobiTheta₂_term_fderiv, jacobiTheta₂_term, hns,
    mul_comm _ ‖cexp _‖, (by norm_num : (3 : ℝ) = 2 + 1), add_mul, add_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable (goal)
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
      ‖HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
          HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)
            (ContinuousLinearMap.snd ℂ ℂ ℂ)‖ ≤
    ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
      (2 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 + 1 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2)
have refine_1 : ‖HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) (ContinuousLinearMap.fst ℂ ℂ ℂ)‖ ≤
  2 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
Tactic: refine mul_le_mul_of_nonneg_left ((norm_add_le _ _).trans (add_le_add ?_ ?_)) (norm_nonneg _)