-- Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean
theorem norm_jacobiTheta_sub_one_le {τ : ℂ} (hτ : 0 < im τ) :
    ‖jacobiTheta τ - 1‖ ≤ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)

Proof state:
τ : ℂ
hτ : 0 < τ.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ ‖jacobiTheta τ - 1‖ = 2 * ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖

Tactic:
rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hτ), norm_mul, Complex.norm_two]

Result:
no goals

Proof state:
τ : ℂ
hτ : 0 < τ.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
⊢ 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 _)]

Result:
τ : ℂ
hτ : 0 < τ.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
⊢ HasSum (HPow.hPow (rexp (-π * τ.im))) (1 - rexp (-π * τ.im))⁻¹

Proof state:
τ : ℂ
hτ : 0 < τ.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)

Tactic:
rw [div_mul_comm, mul_comm]

Result:
no goals

Proof state:
τ : ℂ
hτ : 0 < τ.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]

Result:
τ : ℂ
hτ : 0 < τ.im
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))

Proof state:
τ : ℂ
hτ : 0 < τ.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ 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τ)

Result:
τ : ℂ
hτ : 0 < τ.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
s : HasSum (fun n => rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))

Proof state:
τ : ℂ
hτ : 0 < τ.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑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 * (↑n + 1) ^ 2 * τ)‖
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))

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

Result:
no goals

Proof state:
τ : ℂ
hτ : 0 < τ.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
s : HasSum (fun n => rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))

Tactic:
have aux : Summable fun n : ℕ => ‖cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ :=
  .of_nonneg_of_le (fun n => norm_nonneg _) this s.summable

Result:
τ : ℂ
hτ : 0 < τ.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑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 * (↑n + 1) ^ 2 * τ)‖
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))

Proof state:
τ : ℂ
hτ : 0 < τ.im
⊢ ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)

Tactic:
intro n

Result:
τ : ℂ
hτ : 0 < τ.im
n : ℕ
⊢ ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)

Proof state:
τ : ℂ
hτ : 0 < τ.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑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τ)

Result:
no goals

Proof state:
τ : ℂ
hτ : 0 < τ.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ 2 * ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))

Tactic:
gcongr

Result:
no goals

Proof state:
τ : ℂ
hτ : 0 < τ.im
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))

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)

Result:
τ : ℂ
hτ : 0 < τ.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))

Proof state:
τ : ℂ
hτ : 0 < τ.im
n : ℕ
⊢ ‖cexp (↑π * I * (↑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)

Result:
no goals

Proof state:
τ : ℂ
hτ : 0 < τ.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ ‖jacobiTheta τ - 1‖ ≤ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)

Tactic:
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]

Result:
no goals