-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
lemma F_nat_one_le {a : ℝ} (ha : 0 ≤ a) {t : ℝ} (ht : 0 < t) :
    ‖F_nat 1 a t‖ ≤ rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2
      + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))

Proof state:
case h.e'_5.h
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ a * rexp (-π * (↑n + a ^ 2) * t) = a * rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ n

Tactic:
rw [← Real.exp_nat_mul, mul_assoc _ (exp _), ← Real.exp_add]

Result:
case h.e'_5.h
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ a * rexp (-π * (↑n + a ^ 2) * t) = a * rexp (-π * a ^ 2 * t + ↑n * (-π * t))

Proof state:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ ‖F_nat 1 a t‖ ≤
    rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))

Tactic:
refine tsum_of_norm_bounded ?_ (f_le_g_nat 1 ha ht)

Result:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (g_nat 1 a t)
    (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))

Proof state:
case h.e'_5.h
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
n : ℕ
⊢ ↑n * rexp (-π * (↑n + a ^ 2) * t) = ↑n * rexp (↑n * (-π * t) + -π * a ^ 2 * t)

Tactic:
ring_nf

Result:
no goals

Proof state:
case h.e'_5.h
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ a * rexp (-π * (↑n + a ^ 2) * t) = a * rexp (-π * a ^ 2 * t + ↑n * (-π * t))

Tactic:
ring_nf

Result:
no goals

Proof state:
case h.e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ (fun b => ↑b * rexp (-π * (↑b + a ^ 2) * t)) = fun i => rexp (-π * a ^ 2 * t) * (↑i * rexp (-π * t) ^ i)

Tactic:
ext1 n

Result:
case h.e'_5.h
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
n : ℕ
⊢ ↑n * rexp (-π * (↑n + a ^ 2) * t) = rexp (-π * a ^ 2 * t) * (↑n * rexp (-π * t) ^ n)

Proof state:
case h.e'_6
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 =
    rexp (-π * a ^ 2 * t) * (rexp (-π * t) / (1 - rexp (-π * t)) ^ 2)

Tactic:
rw [mul_add, add_mul, mul_one, exp_add, mul_div_assoc]

Result:
no goals

Proof state:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun n => (↑n + a) ^ 1 * rexp (-π * (↑n + a ^ 2) * t))
    (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))

Tactic:
simp_rw [pow_one, add_mul]

Result:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun n => ↑n * rexp (-π * (↑n + a ^ 2) * t) + a * rexp (-π * (↑n + a ^ 2) * t))
    (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))

Proof state:
case hg
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun b => a * rexp (-π * (↑b + a ^ 2) * t)) (a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))

Tactic:
convert (hasSum_geometric_of_lt_one (exp_pos _).le <| exp_lt_aux ht).mul_left _ using 1

Result:
case h.e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ (fun b => a * rexp (-π * (↑b + a ^ 2) * t)) = fun i => a * rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ i

Proof state:
case hf
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun b => ↑b * rexp (-π * (↑b + a ^ 2) * t)) (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2)

Tactic:
have h0' : ‖rexp (-π * t)‖ < 1 := by
  simpa only [norm_eq_abs, abs_exp] using exp_lt_aux ht

Result:
case hf
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ HasSum (fun b => ↑b * rexp (-π * (↑b + a ^ 2) * t)) (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2)

Proof state:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (g_nat 1 a t)
    (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))

Tactic:
unfold g_nat

Result:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun n => (↑n + a) ^ 1 * rexp (-π * (↑n + a ^ 2) * t))
    (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))

Proof state:
case h.e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ (fun b => a * rexp (-π * (↑b + a ^ 2) * t)) = fun i => a * rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ i

Tactic:
ext1 n

Result:
case h.e'_5.h
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ a * rexp (-π * (↑n + a ^ 2) * t) = a * rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ n

Proof state:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun n => ↑n * rexp (-π * (↑n + a ^ 2) * t) + a * rexp (-π * (↑n + a ^ 2) * t))
    (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))

Tactic:
apply HasSum.add

Result:
case hf
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun b => ↑b * rexp (-π * (↑b + a ^ 2) * t)) (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2)

case hg
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun b => a * rexp (-π * (↑b + a ^ 2) * t)) (a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))

Proof state:
case hf
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ HasSum (fun b => ↑b * rexp (-π * (↑b + a ^ 2) * t)) (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2)

Tactic:
convert (hasSum_coe_mul_geometric_of_norm_lt_one h0').mul_left (exp (-π * a ^ 2 * t)) using 1

Result:
case h.e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ (fun b => ↑b * rexp (-π * (↑b + a ^ 2) * t)) = fun i => rexp (-π * a ^ 2 * t) * (↑i * rexp (-π * t) ^ i)

case h.e'_6
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 =
    rexp (-π * a ^ 2 * t) * (rexp (-π * t) / (1 - rexp (-π * t)) ^ 2)

Proof state:
case h.e'_5.h
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
n : ℕ
⊢ ↑n * rexp (-π * (↑n + a ^ 2) * t) = rexp (-π * a ^ 2 * t) * (↑n * rexp (-π * t) ^ n)

Tactic:
rw [mul_comm (exp _), ← Real.exp_nat_mul, mul_assoc (n : ℝ), ← Real.exp_add]

Result:
case h.e'_5.h
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
n : ℕ
⊢ ↑n * rexp (-π * (↑n + a ^ 2) * t) = ↑n * rexp (↑n * (-π * t) + -π * a ^ 2 * t)

Proof state:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ ‖rexp (-π * t)‖ < 1

Tactic:
simpa only [norm_eq_abs, abs_exp] using exp_lt_aux ht

Result:
no goals