awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
⊢ ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖

Tactic:
have hns (a : ℂ) (f : (ℂ × ℂ) →L[ℂ] ℂ) : ‖a • f‖ = ‖a‖ * ‖f‖ := norm_smul a f
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ 3 = HAdd.hAdd (α := ℝ) 2 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
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)
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ ≤ 3 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖

Tactic:
rw [jacobiTheta₂_term_fderiv, jacobiTheta₂_term, hns,
    mul_comm _ ‖cexp _‖, (by norm_num : (3 : ℝ) = 2 + 1), add_mul, add_mul]

Premises used: add_mul, Norm.norm, jacobiTheta₂_term, jacobiTheta₂_term_fderiv, mul_comm, Complex.exp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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)

Tactic:
mul_le_mul_of_nonneg_left ((norm_add_le _ _).trans (add_le_add ?_ ?_)) (norm_nonneg _)

Premises used: add_le_add, norm_add_le, LE.le.trans, mul_le_mul_of_nonneg_left, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
refine_1 :
  ‖HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) (ContinuousLinearMap.fst ℂ ℂ ℂ)‖ ≤
    2 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
refine_2 :
  ‖HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)
        (ContinuousLinearMap.snd ℂ ℂ ℂ)‖ ≤
    1 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
⊢ ‖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:
refine mul_le_mul_of_nonneg_left ((norm_add_le _ _).trans (add_le_add ?_ ?_)) (norm_nonneg _)

Premises used: add_le_add, norm_add_le, LE.le.trans, mul_le_mul_of_nonneg_left, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
refine_1 :
  2 * π * (↑|n| : ℝ) * Norm.norm (E := ℂ × ℂ →L[ℂ] ℂ) (ContinuousLinearMap.fst ℂ ℂ ℂ) ≤
    2 * π * (↑(HPow.hPow (β := ℕ) |n| 2) : ℝ)
⊢ ‖HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) (ContinuousLinearMap.fst ℂ ℂ ℂ)‖ ≤
    2 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2

Tactic:
simp_rw [hns, norm_mul, ← ofReal_ofNat, ← ofReal_intCast,
      norm_real, norm_of_nonneg zero_le_two, Real.norm_of_nonneg pi_pos.le, norm_I, mul_one,
      Real.norm_eq_abs, ← Int.cast_abs, ← Int.cast_pow]

Premises used: Int.cast_abs, Int.cast_pow, Complex.ofReal_intCast, Real.pi_pos, LT.lt.le, norm_mul, Complex.norm_real, Complex.norm_I, zero_le_two, mul_one, Complex.ofReal_ofNat, Real.norm_eq_abs, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
h₁ : 0 ≤ 2 * π * (↑|n| : ℝ)
refine_1 : 2 * π * (↑|n| : ℝ) * 1 ≤ 2 * π * (↑(HPow.hPow (β := ℕ) |n| 2) : ℝ)
refine_1₁ : 2 * π * (↑|n| : ℝ) ≤ 2 * π * (↑(HPow.hPow (β := ℕ) |n| 2) : ℝ)
refine_1₂ refine_1₃ : 2 * π * (↑|n| : ℝ) ≤ 2 * π * (↑|n| : ℝ)
⊢ 2 * π * (↑|n| : ℝ) * Norm.norm (E := ℂ × ℂ →L[ℂ] ℂ) (ContinuousLinearMap.fst ℂ ℂ ℂ) ≤
    2 * π * (↑(HPow.hPow (β := ℕ) |n| 2) : ℝ)

Tactic:
grw [ContinuousLinearMap.norm_fst_le, mul_one, ← Int.le_self_sq]

Premises used: ContinuousLinearMap.norm_fst_le, Int.le_self_sq, mul_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
refine_2 :
  π * HPow.hPow (α := ℝ) (β := ℕ) |(↑n : ℝ)| 2 * Norm.norm (E := ℂ × ℂ →L[ℂ] ℂ) (ContinuousLinearMap.snd ℂ ℂ ℂ) ≤
    π * HPow.hPow (α := ℝ) (β := ℕ) |(↑n : ℝ)| 2
⊢ ‖HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)
        (ContinuousLinearMap.snd ℂ ℂ ℂ)‖ ≤
    1 * π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2

Tactic:
simp_rw [hns, norm_mul, one_mul, norm_I, mul_one,
      norm_real, norm_of_nonneg pi_pos.le, ← ofReal_intCast, ← ofReal_pow, norm_real,
      Real.norm_eq_abs, Int.cast_abs, abs_pow]

Premises used: Int.cast_abs, Complex.ofReal_intCast, Real.pi_pos, LT.lt.le, norm_mul, Complex.norm_real, Complex.norm_I, mul_one, Complex.ofReal_pow, one_mul, Real.norm_eq_abs, abs_pow, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
refine_2 : Norm.norm (E := ℂ × ℂ →L[ℂ] ℂ) (ContinuousLinearMap.snd ℂ ℂ ℂ) ≤ 1
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) |(↑n : ℝ)| 2 * Norm.norm (E := ℂ × ℂ →L[ℂ] ℂ) (ContinuousLinearMap.snd ℂ ℂ ℂ) ≤
    π * HPow.hPow (α := ℝ) (β := ℕ) |(↑n : ℝ)| 2

Tactic:
apply mul_le_of_le_one_right (mul_nonneg pi_pos.le (pow_nonneg (abs_nonneg _) _))

Premises used: mul_nonneg, pow_nonneg, mul_le_of_le_one_right, Real.pi_pos, LT.lt.le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ Norm.norm (E := ℂ × ℂ →L[ℂ] ℂ) (ContinuousLinearMap.snd ℂ ℂ ℂ) ≤ 1

Tactic:
ContinuousLinearMap.norm_snd_le ..

Premises used: ContinuousLinearMap.norm_snd_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ Norm.norm (E := ℂ × ℂ →L[ℂ] ℂ) (ContinuousLinearMap.snd ℂ ℂ ℂ) ≤ 1

Tactic:
exact ContinuousLinearMap.norm_snd_le ..

Premises used: ContinuousLinearMap.norm_snd_le
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
⊢ Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

Tactic:
(ContinuousLinearMap.le_opNorm _ _).trans ?_

Premises used: ContinuousLinearMap.le_opNorm, LE.le.trans
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
refine : ‖jacobiTheta₂_term_fderiv n z τ‖ * Norm.norm (E := ℂ × ℂ) (0, 1) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

Tactic:
refine (ContinuousLinearMap.le_opNorm _ _).trans ?_

Premises used: ContinuousLinearMap.le_opNorm, LE.le.trans
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
simp_rw :
  ‖jacobiTheta₂_term_fderiv n z τ‖ * max (Norm.norm (E := ℂ) 0) (Norm.norm (E := ℂ) 1) ≤
    ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw₁ : ‖jacobiTheta₂_term_fderiv n z τ‖ * max (Norm.norm (E := ℂ) 0) 1 ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw₂ : ‖jacobiTheta₂_term_fderiv n z τ‖ * max 0 1 ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw₃ : ‖jacobiTheta₂_term_fderiv n z τ‖ * 1 ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw₄ : ‖jacobiTheta₂_term_fderiv n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ * Norm.norm (E := ℂ × ℂ) (0, 1) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

Tactic:
simp_rw [Prod.norm_def, norm_one, norm_zero, max_eq_right zero_le_one, mul_one, le_refl]

Premises used: le_refl, norm_zero, NormOneClass.norm_one, zero_le_one, Prod.norm_def, max_eq_right, mul_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
⊢ Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

Tactic:
have : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖ := by
    refine (ContinuousLinearMap.le_opNorm _ _).trans ?_
    simp_rw [Prod.norm_def, norm_one, norm_zero, max_eq_right zero_le_one, mul_one, le_refl]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
this :
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

Tactic:
le_trans ?_ this

Premises used: le_trans
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
this :
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
refine :
  π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖ ≤
    Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ)
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

Tactic:
refine le_trans ?_ this

Premises used: le_trans
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
this :
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw :
  ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
      (π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2) ≤
    ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
      (‖(↑π : ℂ)‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖)
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖ ≤
    Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ)

Tactic:
simp_rw [jacobiTheta₂_term_fderiv, jacobiTheta₂_term, ContinuousLinearMap.coe_smul',
    Pi.smul_apply, ContinuousLinearMap.add_apply, ContinuousLinearMap.coe_smul',
    ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', Pi.smul_apply, smul_zero, zero_add,
    smul_eq_mul, mul_one, mul_comm _ ‖cexp _‖, norm_mul]

Premises used: Norm.norm, ContinuousLinearMap.coe_smul', jacobiTheta₂_term, smul_zero, jacobiTheta₂_term_fderiv, ContinuousLinearMap.add_apply, norm_mul, zero_add, mul_comm, Complex.exp, ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', smul_eq_mul, mul_one, Pi.smul_apply
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
this :
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
      (π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2) ≤
    ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
      (‖(↑π : ℂ)‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖)

Tactic:
mul_le_mul_of_nonneg_left (le_of_eq ?_) (norm_nonneg _)

Premises used: le_of_eq, mul_le_mul_of_nonneg_left, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
this :
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
refine : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖(↑π : ℂ)‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
⊢ ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
      (π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2) ≤
    ‖cexp (2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ)‖ *
      (‖(↑π : ℂ)‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖)

Tactic:
refine mul_le_mul_of_nonneg_left (le_of_eq ?_) (norm_nonneg _)

Premises used: le_of_eq, mul_le_mul_of_nonneg_left, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
this :
  Norm.norm (E := ℂ) ((jacobiTheta₂_term_fderiv n z τ : (a : ℂ × ℂ) → ℂ) (0, 1) : ℂ) ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
simp_rw : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖π‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
simp_rw₁ : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = π * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
simp_rw₂ : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = π * 1 * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
simp_rw₃ : π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = π * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
simp_rw₄ : π * HPow.hPow (α := ℝ) (β := ℕ) |(↑n : ℝ)| 2 = π * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
simp_rw₅ : π * HPow.hPow (β := ℕ) (Norm.norm (E := ℂ) (↑n : ℂ)) 2 = π * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖
⊢ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 = ‖(↑π : ℂ)‖ * ‖I‖ * ‖HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2‖

Tactic:
simp_rw [norm_real, norm_of_nonneg pi_pos.le, norm_I, mul_one,
    Int.cast_abs, ← norm_intCast, norm_pow]

Premises used: Int.cast_abs, norm_pow, Real.pi_pos, LT.lt.le, Complex.norm_real, Complex.norm_I, mul_one, Complex.norm_intCast, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
mp : (Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ) → 0 < τ.im
mpr : 0 < τ.im → Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
⊢ (Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ) ↔ 0 < τ.im

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
mp :
  (Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ) →
    Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ
⊢ (Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv 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 τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
⊢ Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖

Tactic:
have := h.norm
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
⊢ Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ

Tactic:
this.of_norm_bounded_eventually ?_

Premises used: Summable.of_norm_bounded_eventually
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
mp : ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ ‖jacobiTheta₂_term_fderiv i z τ‖
⊢ Summable (α := ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term x z τ

Tactic:
refine this.of_norm_bounded_eventually ?_

Premises used: Summable.of_norm_bounded_eventually
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv 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 (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
h₁ : ∀ (n : ℤ) (hn : n ≠ 0), ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ ∀ᶠ (i : ℤ) in cofinite, ‖jacobiTheta₂_term i z τ‖ ≤ ‖jacobiTheta₂_term_fderiv i z τ‖

Tactic:
filter_upwards [this] with n hn
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

Tactic:
le_trans ?_ (norm_jacobiTheta₂_term_fderiv_ge n z τ)

Premises used: norm_jacobiTheta₂_term_fderiv_ge, le_trans
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
h₁ : ‖jacobiTheta₂_term n z τ‖ ≤ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

Tactic:
refine le_trans ?_ (norm_jacobiTheta₂_term_fderiv_ge n z τ)

Premises used: norm_jacobiTheta₂_term_fderiv_ge, le_trans
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
h₁ : 1 ≤ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 * ‖jacobiTheta₂_term n z τ‖

Tactic:
apply 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 (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2

Tactic:
one_le_pi_div_two.trans (mul_le_mul_of_nonneg_left ?_ pi_pos.le)

Premises used: Real.pi_pos, LT.lt.le, Real.one_le_pi_div_two, LE.le.trans, mul_le_mul_of_nonneg_left
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
h₁ : 2⁻¹ ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
⊢ 1 ≤ π * HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2

Tactic:
refine one_le_pi_div_two.trans (mul_le_mul_of_nonneg_left ?_ pi_pos.le)

Premises used: Real.pi_pos, LT.lt.le, Real.one_le_pi_div_two, LE.le.trans, mul_le_mul_of_nonneg_left
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ LE.le (α := ℝ) 2⁻¹ 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
h₁ : 1 ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2
⊢ 2⁻¹ ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2

Tactic:
refine (by norm_num : 2⁻¹ ≤ (1 : ℝ)).trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
h₁ : 1 ≤ |n|
⊢ 1 ≤ HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2

Tactic:
rw [one_le_sq_iff_one_le_abs, ← Int.cast_abs, abs_abs, ← Int.cast_one, Int.cast_le]

Premises used: Int.cast_abs, Int.cast_le, one_le_sq_iff_one_le_abs, abs_abs, Int.cast_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
z τ : ℂ
h : Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv 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 (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ
this_1 : Summable (α := ℝ) fun (x : ℤ) ↦ ‖jacobiTheta₂_term_fderiv 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 τ : ℂ
hτ : 0 < τ.im
⊢ Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ

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

Premises used: Real.pi, HMul.hMul, abs, Complex.im, setOf, 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
mpr :
  ∀ (n : ℤ),
    ‖jacobiTheta₂_term_fderiv n z τ‖ ≤
      3 * π *
        (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
          rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ))))
⊢ Summable (α := ℂ × ℂ →L[ℂ] ℂ) fun (x : ℤ) ↦ jacobiTheta₂_term_fderiv x z τ

Tactic:
refine ((summable_pow_mul_jacobiTheta₂_term_bound
      |z.im| hτ 2).mul_left (3 * π)).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 : ℤ
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ ≤
    3 * π *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
        rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ))))

Tactic:
(norm_jacobiTheta₂_term_fderiv_le n z τ).trans
      (?_ : 3 * π * |n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ _)

Premises used: LE.le.trans, norm_jacobiTheta₂_term_fderiv_le
-- 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| : ℝ))))
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ ≤
    3 * π *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑|n| : ℝ) 2 *
        rexp (-π * (τ.im * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * |z.im| * (↑|n| : ℝ))))

Tactic:
refine (norm_jacobiTheta₂_term_fderiv_le n z τ).trans
      (?_ : 3 * π * |n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ _)

Premises used: LE.le.trans, norm_jacobiTheta₂_term_fderiv_le