awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
mpr :
  3 * π * (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖) ≤
    3 * π *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
        rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.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| : ℝ))))

Tactic:
simp_rw [mul_assoc (3 * π)]

Premises used: Real.pi, HMul.hMul, mul_assoc, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ LT.lt (α := ℝ) 0 3

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
mpr :
  HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖ ≤
    HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
      rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.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| : ℝ))))

Tactic:
refine mul_le_mul_of_nonneg_left ?_ (mul_pos (by simp : 0 < (3 : ℝ)) pi_pos).le

Premises used: Real.pi_pos, LT.lt.le, mul_pos, mul_le_mul_of_nonneg_left
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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| : ℝ)))

Tactic:
mul_le_mul_of_nonneg_left ?_ (pow_nonneg (Int.cast_nonneg (abs_nonneg _)) _)

Premises used: pow_nonneg, mul_le_mul_of_nonneg_left
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
mpr : ‖jacobiTheta₂_term n z τ‖ ≤ rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ)))
⊢ 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 ?_ (pow_nonneg (Int.cast_nonneg (abs_nonneg _)) _)

Premises used: pow_nonneg, mul_le_mul_of_nonneg_left
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ)))

Tactic:
norm_jacobiTheta₂_term_le hτ le_rfl le_rfl n

Premises used: norm_jacobiTheta₂_term_le, le_rfl
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ)))

Tactic:
exact norm_jacobiTheta₂_term_le hτ le_rfl le_rfl n

Premises used: norm_jacobiTheta₂_term_le, le_rfl
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
mp : (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) → 0 < τ.im
mpr : 0 < τ.im → Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
⊢ (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) ↔ 0 < τ.im

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
mp :
  (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) → Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
⊢ (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) → 0 < τ.im

Tactic:
rw [← summable_jacobiTheta₂_term_iff (z := z)]

Premises used: summable_jacobiTheta₂_term_iff
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
⊢ (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) → Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ

Tactic:
fun h ↦ (h.norm.mul_left (2 * π)⁻¹).of_norm_bounded_eventually ?_

Premises used: Real.pi, HMul.hMul, Summable.mul_left, Inv.inv, Summable.norm, Summable.of_norm_bounded_eventually, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
mp :
  ∀ (h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ),
    ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term i z τ‖
⊢ (Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ) → Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ

Tactic:
refine fun h ↦ (h.norm.mul_left (2 * π)⁻¹).of_norm_bounded_eventually ?_
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
⊢ ∀ᶠ (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⟩)
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
h₁ : ∀ (n : ℤ) (hn : n ≠ 0), ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term n z τ‖
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term i z τ‖

Tactic:
filter_upwards [this] with n hn
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
h₁ : ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ * ‖jacobiTheta₂_term n z τ‖
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term n z τ‖

Tactic:
rw [jacobiTheta₂'_term, norm_mul, ← mul_assoc]

Premises used: jacobiTheta₂'_term, mul_assoc, norm_mul
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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 τ‖

Tactic:
le_mul_of_one_le_left (norm_nonneg _) ?_

Premises used: le_mul_of_one_le_left, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
h₁ : 1 ≤ (2 * π)⁻¹ * ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ * ‖jacobiTheta₂_term n z τ‖

Tactic:
refine le_mul_of_one_le_left (norm_nonneg _) ?_

Premises used: le_mul_of_one_le_left, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
h₁ : LE.le (α := ℝ) 1 (↑|n| : ℝ)
⊢ 1 ≤ (2 * π)⁻¹ * ‖2 * (↑π : ℂ) * I * (↑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]

Premises used: Int.cast_abs, Real.pi, HMul.hMul, mul_assoc, two_pos, Complex.ofReal_intCast, Real.pi_pos, LT.lt.le, norm_mul, Complex.norm_real, LT.lt.ne', mul_pos, Complex.norm_I, mul_one, Complex.ofReal_ofNat, OfNat.ofNat, inv_mul_cancel₀, one_mul, Real.norm_eq_abs, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
h₁ : 1 ≤ |n|
⊢ LE.le (α := ℝ) 1 (↑|n| : ℝ)

Tactic:
rw [← Int.cast_one, Int.cast_le]

Premises used: Int.cast_le, Int.cast_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ |n|

Tactic:
Int.one_le_abs hn

Premises used: Int.one_le_abs
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ |n|

Tactic:
exact Int.one_le_abs hn

Premises used: Int.one_le_abs
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
⊢ 0 < τ.im → Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ

Tactic:
fun hτ ↦ ((summable_pow_mul_jacobiTheta₂_term_bound
      |z.im| hτ 1).mul_left (2 * π)).of_norm_bounded (fun n ↦ ?_)

Premises used: Real.pi, HMul.hMul, abs, Complex.im, Summable.mul_left, Summable.of_norm_bounded, summable_pow_mul_jacobiTheta₂_term_bound, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
mpr :
  ∀ (hτ : 0 < τ.im) (n : ℤ),
    ‖jacobiTheta₂'_term n z τ‖ ≤
      2 * π *
        (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 1 *
          rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ))))
⊢ 0 < τ.im → Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂'_term x z τ

Tactic:
refine fun hτ ↦ ((summable_pow_mul_jacobiTheta₂_term_bound
      |z.im| hτ 1).mul_left (2 * π)).of_norm_bounded (fun n ↦ ?_)

Premises used: Real.pi, HMul.hMul, abs, Complex.im, Summable.mul_left, Summable.of_norm_bounded, summable_pow_mul_jacobiTheta₂_term_bound, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
mpr :
  ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ * ‖jacobiTheta₂_term n z τ‖ ≤
    2 * π * (↑|n| : ℝ) * rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ)))
⊢ ‖jacobiTheta₂'_term n z τ‖ ≤
    2 * π *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 1 *
        rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ))))

Tactic:
rw [jacobiTheta₂'_term, norm_mul, ← mul_assoc, pow_one]

Premises used: jacobiTheta₂'_term, mul_assoc, norm_mul, pow_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 0 ≤ 2 * π * (↑|n| : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
mpr : ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ = 2 * π * (↑|n| : ℝ)
⊢ ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ * ‖jacobiTheta₂_term n z τ‖ ≤
    2 * π * (↑|n| : ℝ) * rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ)))

Tactic:
refine mul_le_mul (le_of_eq ?_) (norm_jacobiTheta₂_term_le hτ le_rfl le_rfl n)
      (norm_nonneg _) (by positivity)

Premises used: norm_jacobiTheta₂_term_le, le_rfl, mul_le_mul, le_of_eq, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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| : ℝ)
mpr₅ : 2 * π * |(↑n : ℝ)| = 2 * π * (↑|n| : ℝ)
⊢ ‖2 * (↑π : ℂ) * I * (↑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]

Premises used: Int.cast_abs, Real.pi_pos, LT.lt.le, norm_mul, Complex.norm_of_nonneg, Complex.norm_I, mul_one, Complex.norm_two, Complex.norm_intCast
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term n z τ) (jacobiTheta₂ z τ)

Tactic:
((summable_jacobiTheta₂_term_iff z τ).mpr hτ).hasSum

Premises used: Iff.mpr, jacobiTheta₂, Summable.hasSum, summable_jacobiTheta₂_term_iff
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ HasSum (fun (n : ℤ) ↦ jacobiTheta₂_term_fderiv n z τ) (jacobiTheta₂_fderiv z τ)

Tactic:
((summable_jacobiTheta₂_term_fderiv_iff z τ).mpr hτ).hasSum

Premises used: Iff.mpr, summable_jacobiTheta₂_term_fderiv_iff, Summable.hasSum, jacobiTheta₂_fderiv
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
⊢ HasSum (fun (n : ℤ) ↦ jacobiTheta₂'_term n z τ) (jacobiTheta₂' z τ)

Tactic:
((summable_jacobiTheta₂'_term_iff z τ).mpr hτ).hasSum

Premises used: Iff.mpr, Summable.hasSum, jacobiTheta₂', summable_jacobiTheta₂'_term_iff
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
h : ¬Summable (α := ℂ) fun (b : ℤ) ↦ jacobiTheta₂_term b z τ
⊢ jacobiTheta₂ z τ = 0

Tactic:
apply tsum_eq_zero_of_not_summable

Premises used: tsum_eq_zero_of_not_summable
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
h : ¬0 < τ.im
⊢ ¬Summable (α := ℂ) fun (b : ℤ) ↦ jacobiTheta₂_term b z τ

Tactic:
rw [summable_jacobiTheta₂_term_iff]

Premises used: summable_jacobiTheta₂_term_iff
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬0 < τ.im

Tactic:
not_lt.mpr hτ

Premises used: Iff.mpr, not_lt
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬0 < τ.im

Tactic:
exact not_lt.mpr hτ

Premises used: Iff.mpr, not_lt
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
h : ¬Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (b : ℤ) ↦ jacobiTheta₂_term_fderiv b z τ
⊢ jacobiTheta₂_fderiv z τ = 0

Tactic:
apply tsum_eq_zero_of_not_summable

Premises used: tsum_eq_zero_of_not_summable
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
h : ¬0 < τ.im
⊢ ¬Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (b : ℤ) ↦ jacobiTheta₂_term_fderiv b z τ

Tactic:
rw [summable_jacobiTheta₂_term_fderiv_iff]

Premises used: summable_jacobiTheta₂_term_fderiv_iff
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
h : ¬Summable (α := ℂ) fun (b : ℤ) ↦ jacobiTheta₂'_term b z τ
⊢ jacobiTheta₂' z τ = 0

Tactic:
apply tsum_eq_zero_of_not_summable

Premises used: tsum_eq_zero_of_not_summable
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : τ.im ≤ 0
h : ¬0 < τ.im
⊢ ¬Summable (α := ℂ) fun (b : ℤ) ↦ jacobiTheta₂'_term b z τ

Tactic:
rw [summable_jacobiTheta₂'_term_iff]

Premises used: summable_jacobiTheta₂'_term_iff
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
obtain :
  ∀ (T : ℝ) (hT : 0 < T) (hτ' : T < τ.im),
    HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
⊢ HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

Tactic:
obtain ⟨T, hT, hτ'⟩ := exists_between hτ

Premises used: exists_between
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
obtain :
  ∀ (S : ℝ) (hz : |z.im| < S), HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
⊢ HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

Tactic:
obtain ⟨S, hz⟩ := exists_gt |im z|

Premises used: abs, Complex.im, NoMaxOrder.exists_gt
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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

Tactic:
((_root_.continuous_abs.comp continuous_im).isOpen_preimage _ isOpen_Iio).prod ?_

Premises used: abs, Set.Mem, Continuous.comp, setOf, isOpen_Iio, Set.preimage, continuous_abs, Set.Iio, Continuous.isOpen_preimage, Complex.continuous_im, IsOpen.prod
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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}
refine : IsOpen (X := ℂ) {v : ℂ | T < v.im}
⊢ IsOpen V

Tactic:
refine ((_root_.continuous_abs.comp continuous_im).isOpen_preimage _ isOpen_Iio).prod ?_

Premises used: Continuous.comp, isOpen_Iio, continuous_abs, Continuous.isOpen_preimage, Complex.continuous_im, IsOpen.prod
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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 (X := ℂ) {v : ℂ | T < v.im}

Tactic:
continuous_im.isOpen_preimage _ isOpen_Ioi

Premises used: Set.Mem, setOf, isOpen_Ioi, Set.preimage, Continuous.isOpen_preimage, Complex.continuous_im
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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 (X := ℂ) {v : ℂ | T < v.im}

Tactic:
exact continuous_im.isOpen_preimage _ isOpen_Ioi

Premises used: isOpen_Ioi, Continuous.isOpen_preimage, Complex.continuous_im
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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

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
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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
⊢ (z, τ) ∈ V

Tactic:
have hVmem : (z, τ) ∈ V := ⟨hz, hτ'⟩
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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

Tactic:
(Convex.isPreconnected ?_).prod (convex_halfSpace_im_gt T).isPreconnected

Premises used: convex_halfSpace_im_gt, IsPreconnected.prod, Convex.isPreconnected
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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
refine : Convex ℝ (E := ℂ) {u : ℂ | |u.im| < S}
⊢ IsPreconnected V

Tactic:
refine (Convex.isPreconnected ?_).prod (convex_halfSpace_im_gt T).isPreconnected

Premises used: convex_halfSpace_im_gt, IsPreconnected.prod, Convex.isPreconnected
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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
⊢ Convex ℝ (E := ℂ) {u : ℂ | |u.im| < S}

Tactic:
simpa only [abs_lt] using (convex_halfSpace_im_gt _).inter (convex_halfSpace_im_lt _)

Premises used: convex_halfSpace_im_gt, convex_halfSpace_im_lt, Convex.inter, abs_lt
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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

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 _)
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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
⊢ ∀ (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
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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

Tactic:
fun n p hp ↦ (norm_jacobiTheta₂_term_fderiv_le n p.1 p.2).trans ?_

Premises used: Prod.fst, LE.le.trans, Prod.snd, norm_jacobiTheta₂_term_fderiv_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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| : ℝ)))
refine :
  ∀ (n : ℤ) (p : ℂ × ℂ) (hp : p ∈ V),
    3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n p.1 p.2‖ ≤ u n
⊢ ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n

Tactic:
refine fun n p hp ↦ (norm_jacobiTheta₂_term_fderiv_le n p.1 p.2).trans ?_

Premises used: LE.le.trans, norm_jacobiTheta₂_term_fderiv_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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
⊢ 0 ≤ 3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2

Tactic:
positivity