-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
/-- The uniform bound we have given is summable, and remains so after multiplying by any fixed
power of `|n|` (we shall need this for `k = 0, 1, 2`). -/
lemma summable_pow_mul_jacobiTheta₂_term_bound (S : ℝ) {T : ℝ} (hT : 0 < T) (k : ℕ) :
    Summable (fun n : ℤ ↦ (|n| ^ k : ℝ) * Real.exp (-π * (T * n ^ 2 - 2 * S * |n|)))

Proof state:
S T : ℝ
hT : 0 < T
k n : ℕ
⊢ -(-π * (T * ↑n ^ 2 - 2 * S * ↑n) - -1 * ↑n) = ↑n * (π * T * ↑n - (2 * π * S + 1))

Tactic:
ring

Result:
no goals

Proof state:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ (fun x => rexp (-π * (T * ↑x ^ 2 - 2 * S * ↑x))) =O[atTop] fun x => rexp (-1 * ↑x)

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

Result:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto ((fun x => -π * (T * ↑x ^ 2 - 2 * S * ↑x)) - fun x => -1 * ↑x) atTop atBot

Proof state:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto (fun x => -(-π * (T * ↑x ^ 2 - 2 * S * ↑x) - -1 * ↑x)) 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]

Result:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto (fun n => ↑n * (π * T * ↑n - (2 * π * S + 1))) atTop atTop

Proof state:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto (fun n => π * T * ↑n) atTop atTop

Tactic:
exact tendsto_natCast_atTop_atTop.const_mul_atTop (mul_pos pi_pos hT)

Result:
no goals

Proof state:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Summable fun n => ↑n ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑n))

Tactic:
apply summable_of_isBigO_nat (summable_pow_mul_exp_neg_nat_mul k zero_lt_one)

Result:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ (fun n => ↑n ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑n))) =O[atTop] fun n => ↑n ^ k * rexp (-1 * ↑n)

Proof state:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Summable fun n => ↑|n| ^ k * rexp (-π * (T * ↑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]

Result:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Summable fun n => ↑n ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑n))

Proof state:
S T : ℝ
hT : 0 < T
k : ℕ
this : Summable fun n => ↑n ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑n))
⊢ Summable fun n => ↑|n| ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))

Tactic:
apply Summable.of_nat_of_neg <;>
simpa only [Int.cast_neg, neg_sq, abs_neg, Int.cast_natCast, Nat.abs_cast]

Result:
no goals

Proof state:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ (fun n => ↑n ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑n))) =O[atTop] fun n => ↑n ^ k * rexp (-1 * ↑n)

Tactic:
apply IsBigO.mul (isBigO_refl _ _)

Result:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ (fun x => rexp (-π * (T * ↑x ^ 2 - 2 * S * ↑x))) =O[atTop] fun x => rexp (-1 * ↑x)

Proof state:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto ((fun x => -π * (T * ↑x ^ 2 - 2 * S * ↑x)) - fun x => -1 * ↑x) atTop atBot

Tactic:
simp_rw [← tendsto_neg_atTop_iff, Pi.sub_apply]

Result:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto (fun x => -(-π * (T * ↑x ^ 2 - 2 * S * ↑x) - -1 * ↑x)) atTop atTop

Proof state:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto (fun n => ↑n * (π * T * ↑n - (2 * π * S + 1))) atTop atTop

Tactic:
refine tendsto_natCast_atTop_atTop.atTop_mul_atTop₀ (tendsto_atTop_add_const_right _ _ ?_)

Result:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto (fun n => π * T * ↑n) atTop atTop