awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
suffices :
  Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ ‖jacobiTheta τ - 1‖ ≤ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)

Tactic:
suffices ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ ≤
      rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) by
    calc
      ‖jacobiTheta τ - 1‖ = ↑2 * ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ := by
        rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hτ), norm_mul, Complex.norm_two]
      _ ≤ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) := by gcongr
      _ = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) := by rw [div_mul_comm, mul_comm]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
n : ℕ
⊢ ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)

Tactic:
simpa only [Int.cast_add, Int.cast_one] using norm_exp_mul_sq_le hτ (n + 1)

Premises used: norm_exp_mul_sq_le, Int.cast_add, Nat.cast, HAdd.hAdd, OfNat.ofNat, Int.cast_one
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
⊢ ∀ (n : ℕ),
    ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)

Tactic:
have : ∀ n : ℕ, ‖cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1) := by
    intro n
    simpa only [Int.cast_add, Int.cast_one] using norm_exp_mul_sq_le hτ (n + 1)
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℕ),
    ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
simp_rw : HasSum (HPow.hPow (rexp (-π * τ.im))) (1 - rexp (-π * τ.im))⁻¹
⊢ HasSum (fun (n : ℕ) ↦ rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))

Tactic:
simp_rw [pow_succ', div_eq_mul_inv, hasSum_mul_left_iff (Real.exp_ne_zero _)]

Premises used: hasSum_mul_left_iff, div_eq_mul_inv, pow_succ', Real.exp_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℕ),
    ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
⊢ HasSum (HPow.hPow (rexp (-π * τ.im))) (1 - rexp (-π * τ.im))⁻¹

Tactic:
hasSum_geometric_of_lt_one (exp_pos (-π * τ.im)).le
      (exp_lt_one_iff.mpr <| mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hτ)

Premises used: Iff.mpr, mul_neg_of_neg_of_pos, Real.pi, HMul.hMul, Complex.im, Real.pi_pos, LT.lt.le, neg_lt_zero, Real.exp_lt_one_iff, Neg.neg, hasSum_geometric_of_lt_one, Real.exp_pos
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℕ),
    ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
⊢ HasSum (HPow.hPow (rexp (-π * τ.im))) (1 - rexp (-π * τ.im))⁻¹

Tactic:
exact hasSum_geometric_of_lt_one (exp_pos (-π * τ.im)).le
      (exp_lt_one_iff.mpr <| mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hτ)

Premises used: Iff.mpr, mul_neg_of_neg_of_pos, Real.pi, HMul.hMul, Complex.im, Real.pi_pos, LT.lt.le, neg_lt_zero, Real.exp_lt_one_iff, Neg.neg, hasSum_geometric_of_lt_one, Real.exp_pos
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℕ),
    ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
⊢ HasSum (fun (n : ℕ) ↦ rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))

Tactic:
have s : HasSum (fun n : ℕ =>
      rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) := by
    simp_rw [pow_succ', div_eq_mul_inv, hasSum_mul_left_iff (Real.exp_ne_zero _)]
    exact hasSum_geometric_of_lt_one (exp_pos (-π * τ.im)).le
      (exp_lt_one_iff.mpr <| mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hτ)
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℕ),
    ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
s : HasSum (fun (n : ℕ) ↦ rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖

Tactic:
have aux : Summable fun n : ℕ => ‖cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ :=
    .of_nonneg_of_le (fun n => norm_nonneg _) this s.summable
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℕ),
    ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
s : HasSum (fun (n : ℕ) ↦ rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))
aux : Summable (α := ℝ) fun (n : ℕ) ↦ ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖
⊢ Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))

Tactic:
(norm_tsum_le_tsum_norm aux).trans ((aux.tsum_mono s.summable this).trans_eq s.tsum_eq)

Premises used: LE.le.trans_eq, HasSum.summable, HasSum.tsum_eq, norm_tsum_le_tsum_norm, LE.le.trans, Summable.tsum_mono
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℕ),
    ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
s : HasSum (fun (n : ℕ) ↦ rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))
aux : Summable (α := ℝ) fun (n : ℕ) ↦ ‖cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)‖
⊢ Norm.norm (E := ℂ) (∑' (n : ℕ), cexp ((↑π : ℂ) * I * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 * τ)) ≤
    rexp (-π * τ.im) / (1 - rexp (-π * τ.im))

Tactic:
exact (norm_tsum_le_tsum_norm aux).trans ((aux.tsum_mono s.summable this).trans_eq s.tsum_eq)

Premises used: LE.le.trans_eq, HasSum.summable, HasSum.tsum_eq, norm_tsum_le_tsum_norm, LE.le.trans, Summable.tsum_mono
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
simp_rw : ∃ (c : ℝ) (a : ℝ), ∀ b ≥ a, ∀ (a : ℂ), a.im = b → ‖jacobiTheta a - 1‖ ≤ c * ‖rexp (-π * a.im)‖
⊢ IsBigO (E := ℂ) (F := ℝ) (comap im atTop) (fun (τ : ℂ) ↦ jacobiTheta τ - 1) fun (τ : ℂ) ↦ rexp (-π * τ.im)

Tactic:
simp_rw [IsBigO, IsBigOWith, Filter.eventually_comap, Filter.eventually_atTop]

Premises used: Asymptotics.IsBigOWith, Asymptotics.IsBigO, Filter.eventually_comap, Filter.eventually_atTop
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
⊢ ∃ (c : ℝ) (a : ℝ), ∀ b ≥ a, ∀ (a : ℂ), a.im = b → ‖jacobiTheta a - 1‖ ≤ c * ‖rexp (-π * a.im)‖

Tactic:
⟨2 / (1 - rexp (-(π * 1))), 1, fun y hy τ hτ =>
    (norm_jacobiTheta_sub_one_le (hτ.symm ▸ zero_lt_one.trans_le hy : 0 < im τ)).trans ?_⟩

Premises used: Real.pi, HMul.hMul, HSub.hSub, Eq.rec, HDiv.hDiv, norm_jacobiTheta_sub_one_le, Real.exp, zero_lt_one, LT.lt.trans_le, Exists.intro, LE.le.trans, OfNat.ofNat, Eq.symm, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
refine :
  ∀ (y : ℝ) (hy : y ≥ 1) (τ : ℂ) (hτ : τ.im = y),
    2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) ≤ 2 / (1 - rexp (-(π * 1))) * ‖rexp (-π * τ.im)‖
⊢ ∃ (c : ℝ) (a : ℝ), ∀ b ≥ a, ∀ (a : ℂ), a.im = b → ‖jacobiTheta a - 1‖ ≤ c * ‖rexp (-π * a.im)‖

Tactic:
refine ⟨2 / (1 - rexp (-(π * 1))), 1, fun y hy τ hτ =>
    (norm_jacobiTheta_sub_one_le (hτ.symm ▸ zero_lt_one.trans_le hy : 0 < im τ)).trans ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
y : ℝ
hy : y ≥ 1
τ : ℂ
hτ : τ.im = y
rw : 2 / (1 - rexp (-(π * y))) * rexp (-(π * y)) ≤ 2 / (1 - rexp (-(π * 1))) * rexp (-(π * y))
⊢ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) ≤ 2 / (1 - rexp (-(π * 1))) * ‖rexp (-π * τ.im)‖

Tactic:
rw [Real.norm_eq_abs, Real.abs_exp, hτ, neg_mul]

Premises used: neg_mul, Real.norm_eq_abs, Real.abs_exp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
y : ℝ
hy : y ≥ 1
τ : ℂ
hτ : τ.im = y
hbc : 0 < 1 - rexp (-(π * 1))
⊢ 2 / (1 - rexp (-(π * y))) * rexp (-(π * y)) ≤ 2 / (1 - rexp (-(π * 1))) * rexp (-(π * y))

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
y : ℝ
hy : y ≥ 1
τ : ℂ
hτ : τ.im = y
⊢ 0 < 1 - rexp (-(π * 1))

Tactic:
simp [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
simp_rw : DifferentiableAt ℂ (jacobiTheta₂ 0) τ
⊢ DifferentiableAt ℂ jacobiTheta τ

Tactic:
simp_rw [funext jacobiTheta_eq_jacobiTheta₂]

Premises used: funext, jacobiTheta_eq_jacobiTheta₂
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
⊢ DifferentiableAt ℂ (jacobiTheta₂ 0) τ

Tactic:
differentiableAt_jacobiTheta₂_snd 0 hτ

Premises used: differentiableAt_jacobiTheta₂_snd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
⊢ DifferentiableAt ℂ (jacobiTheta₂ 0) τ

Tactic:
exact differentiableAt_jacobiTheta₂_snd 0 hτ

Premises used: differentiableAt_jacobiTheta₂_snd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
Goal:
τ : ℂ
hτ : 0 < τ.im
⊢ ContinuousAt jacobiTheta τ

Tactic:
(differentiableAt_jacobiTheta hτ).continuousAt

Premises used: DifferentiableAt.continuousAt, differentiableAt_jacobiTheta
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
f : ℂ × ℂ → ℂ :=
  fun (p : ℂ × ℂ) ↦ 2 * (↑π : ℂ) * I * (↑n : ℂ) * p.1 + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * p.2
suffices :
  HasFDerivAt f
    (HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
      HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)
        (ContinuousLinearMap.snd ℂ ℂ ℂ))
    (z, τ)
⊢ HasFDerivAt (fun (p : ℂ × ℂ) ↦ jacobiTheta₂_term n p.1 p.2) (jacobiTheta₂_term_fderiv n z τ) (z, τ)

Tactic:
suffices HasFDerivAt f ((2 * π * I * n) • (ContinuousLinearMap.fst ℂ ℂ ℂ)
    + (π * I * n ^ 2) • (ContinuousLinearMap.snd ℂ ℂ ℂ)) (z, τ) from this.cexp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
f : ℂ × ℂ → ℂ :=
  fun (p : ℂ × ℂ) ↦ 2 * (↑π : ℂ) * I * (↑n : ℂ) * p.1 + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * p.2
⊢ HasFDerivAt f
    (HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
      HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)
        (ContinuousLinearMap.snd ℂ ℂ ℂ))
    (z, τ)

Tactic:
(hasFDerivAt_fst.const_mul _).add (hasFDerivAt_snd.const_mul _)

Premises used: HasFDerivAt.add, setOf, HasFDerivAt.const_mul
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
f : ℂ × ℂ → ℂ :=
  fun (p : ℂ × ℂ) ↦ 2 * (↑π : ℂ) * I * (↑n : ℂ) * p.1 + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * p.2
⊢ HasFDerivAt f
    (HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (2 * (↑π : ℂ) * I * (↑n : ℂ)) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
      HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) ((↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)
        (ContinuousLinearMap.snd ℂ ℂ ℂ))
    (z, τ)

Tactic:
exact (hasFDerivAt_fst.const_mul _).add (hasFDerivAt_snd.const_mul _)

Premises used: HasFDerivAt.add
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
push_cast :
  2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ =
    (↑π : ℂ) * HMul.hMul (α := ℂ) 2 (↑n : ℂ) * z * I + (↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ * I
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ =
    (↑(π * HMul.hMul (α := ℝ) 2 (↑n : ℝ)) : ℂ) * z * I + (↑(π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2) : ℂ) * τ * I

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
⊢ 2 * (↑π : ℂ) * I * (↑n : ℂ) * z + (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ =
    (↑π : ℂ) * HMul.hMul (α := ℂ) 2 (↑n : ℂ) * z * I + (↑π : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * τ * I

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
rw :
  rexp (-(π * HMul.hMul (α := ℝ) 2 (↑n : ℝ) * z.im) + -(π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im)) =
    rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im)
⊢ ‖jacobiTheta₂_term n z τ‖ = rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im)

Tactic:
rw [jacobiTheta₂_term, Complex.norm_exp, (by push_cast; ring :
    (2 * π : ℂ) * I * n * z + π * I * n ^ 2 * τ = (π * (2 * n) :) * z * I + (π * n ^ 2 :) * τ * I),
    add_re, mul_I_re, im_ofReal_mul, mul_I_re, im_ofReal_mul]

Premises used: jacobiTheta₂_term, Complex.add_re, Complex.mul_I_re, Complex.norm_exp, Complex.im_ofReal_mul
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
n : ℤ
z τ : ℂ
⊢ rexp (-(π * HMul.hMul (α := ℝ) 2 (↑n : ℝ) * z.im) + -(π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im)) =
    rexp (-π * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im - 2 * π * (↑n : ℝ) * z.im)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
simp_rw :
  HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * T + -(2 * S * (↑|n| : ℝ)) ≤
    HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im + HMul.hMul (α := ℝ) 2 (↑n : ℝ) * z.im
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑|n| : ℝ)))

Tactic:
simp_rw [norm_jacobiTheta₂_term, Real.exp_le_exp, sub_eq_add_neg, neg_mul, ← neg_add,
    neg_le_neg_iff, mul_comm (2 : ℝ), mul_assoc π, ← mul_add, mul_le_mul_iff_right₀ pi_pos,
    mul_comm T, mul_comm S]

Premises used: Real.pi, mul_assoc, sub_eq_add_neg, norm_jacobiTheta₂_term, neg_add, Real.pi_pos, Real.exp_le_exp, mul_comm, mul_add, neg_mul, OfNat.ofNat, neg_le_neg_iff, mul_le_mul_iff_right₀
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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

Tactic:
add_le_add (mul_le_mul le_rfl hτ hT.le (sq_nonneg _)) ?_

Premises used: le_rfl, add_le_add, LT.lt.le, mul_le_mul, sq_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
refine : -(2 * S * (↑|n| : ℝ)) ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ) * z.im
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * T + -(2 * S * (↑|n| : ℝ)) ≤
    HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * τ.im + HMul.hMul (α := ℝ) 2 (↑n : ℝ) * z.im

Tactic:
refine add_le_add (mul_le_mul le_rfl hτ hT.le (sq_nonneg _)) ?_

Premises used: le_rfl, add_le_add, LT.lt.le, mul_le_mul, sq_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
rw : (↑|n| : ℝ) * -S ≤ (↑n : ℝ) * z.im
⊢ -(2 * S * (↑|n| : ℝ)) ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ) * z.im

Tactic:
rw [← mul_neg, mul_assoc, mul_assoc, mul_le_mul_iff_right₀ two_pos, mul_comm, neg_mul, ← mul_neg]

Premises used: mul_assoc, two_pos, mul_comm, neg_mul, mul_neg, mul_le_mul_iff_right₀
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ (↑|n| : ℝ) * -S ≤ (↑n : ℝ) * z.im

Tactic:
le_trans ?_ (neg_abs_le _)

Premises used: neg_abs_le, le_trans
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
refine : (↑|n| : ℝ) * -S ≤ -|(↑n : ℝ) * z.im|
⊢ (↑|n| : ℝ) * -S ≤ (↑n : ℝ) * z.im

Tactic:
refine le_trans ?_ (neg_abs_le _)

Premises used: neg_abs_le, le_trans
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
rw : |(↑n : ℝ)| * |z.im| ≤ |(↑n : ℝ)| * S
⊢ (↑|n| : ℝ) * -S ≤ -|(↑n : ℝ) * z.im|

Tactic:
rw [mul_neg, neg_le_neg_iff, abs_mul, Int.cast_abs]

Premises used: Int.cast_abs, abs_mul, mul_neg, neg_le_neg_iff
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ |(↑n : ℝ)| * |z.im| ≤ |(↑n : ℝ)| * S

Tactic:
mul_le_mul_of_nonneg_left hz (abs_nonneg _)

Premises used: mul_le_mul_of_nonneg_left, abs_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ |(↑n : ℝ)| * |z.im| ≤ |(↑n : ℝ)| * S

Tactic:
exact mul_le_mul_of_nonneg_left hz (abs_nonneg _)

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

Tactic:
rw [jacobiTheta₂'_term, norm_mul]

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

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

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

Premises used: norm_jacobiTheta₂_term_le, mul_le_mul, le_of_eq, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ‖2 * (↑π : ℂ) * I * (↑n : ℂ)‖ = 2 * π * (↑|n| : ℝ)

Tactic:
simp only [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:
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 : ℤ)| : ℝ)))
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| : ℝ)))

Tactic:
apply Summable.of_nat_of_neg

Premises used: Summable.of_nat_of_neg
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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 : ℤ)| : ℝ)))

Tactic:
simpa only [Int.cast_neg, neg_sq, abs_neg, Int.cast_natCast, Nat.abs_cast]

Premises used: Int.cast_neg, Int.cast_natCast, abs_neg, Nat.abs_cast, neg_sq
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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 : ℤ))| : ℝ)))

Tactic:
simpa only [Int.cast_neg, neg_sq, abs_neg, Int.cast_natCast, Nat.abs_cast]

Premises used: Int.cast_neg, Int.cast_natCast, abs_neg, Nat.abs_cast, neg_sq
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
suffices :
  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| : ℝ)))

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]
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
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 : ℝ))
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    HPow.hPow (α := ℝ) (↑n : ℝ) k * rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 - 2 * S * (↑n : ℝ)))

Tactic:
apply summable_of_isBigO_nat (summable_pow_mul_exp_neg_nat_mul k zero_lt_one)

Premises used: zero_lt_one, Real.summable_pow_mul_exp_neg_nat_mul, summable_of_isBigO_nat
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
apply :
  IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (x : ℕ) ↦ rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)))) fun (x : ℕ) ↦
    rexp (HMul.hMul (α := ℝ) (-1) (↑x : ℝ))
⊢ 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 IsBigO.mul (isBigO_refl _ _)

Premises used: Asymptotics.IsBigO.mul
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
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 : ℝ))

Tactic:
Real.isBigO_exp_comp_exp_comp.mpr (Tendsto.isBoundedUnder_le_atBot ?_)

Premises used: Iff.mpr, Filter.Tendsto.isBoundedUnder_le_atBot, Real.isBigO_exp_comp_exp_comp
-- Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
Goal:
S T : ℝ
hT : 0 < T
k : ℕ
refine :
  Tendsto
    (HSub.hSub (α := ℕ → ℝ) (fun (x : ℕ) ↦ -π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)))
      fun (x : ℕ) ↦ HMul.hMul (α := ℝ) (-1) (↑x : ℝ))
    atTop atBot
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (x : ℕ) ↦ rexp (-π * (T * HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2 - 2 * S * (↑x : ℝ)))) fun (x : ℕ) ↦
    rexp (HMul.hMul (α := ℝ) (-1) (↑x : ℝ))

Tactic:
refine Real.isBigO_exp_comp_exp_comp.mpr (Tendsto.isBoundedUnder_le_atBot ?_)

Premises used: Iff.mpr, Filter.Tendsto.isBoundedUnder_le_atBot, Real.isBigO_exp_comp_exp_comp