-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
lemma summable_f_nat (k : ℕ) (a : ℝ) {t : ℝ} (ht : 0 < t) : Summable (f_nat k a t)

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)‖ ≤
    ((fun i => ↑|i| ^ k * rexp (-π * (t * ↑i ^ 2 - 2 * (|a| * t) * ↑|i|)) * rexp (-π * a ^ 2 * t)) ∘ Nat.cast) n

Tactic:
simp_rw [mul_assoc, Function.comp_apply, ← Real.exp_add, norm_mul, norm_pow, Int.cast_abs,
  Int.cast_natCast, norm_eq_abs, Nat.abs_cast, abs_exp]

Result:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ ↑n ^ k * rexp (-π * ((↑n + a) ^ 2 * t)) ≤ ↑n ^ k * rexp (-π * (t * ↑n ^ 2 - 2 * (|a| * (t * ↑n))) + -π * (a ^ 2 * t))

Proof state:
case h.hab
k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n => ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
n : ℕ
hn : ⌈|a|⌉₊ ≤ n
⊢ |↑n + a| ≤ ↑n + ↑n

Tactic:
exact (abs_add_le ..).trans (add_le_add (Nat.abs_cast _).le (Nat.ceil_le.mp hn))

Result:
no goals

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ ↑n ^ k * rexp (-π * ((↑n + a) ^ 2 * t)) ≤ ↑n ^ k * rexp (-π * (t * ↑n ^ 2 - 2 * (|a| * (t * ↑n))) + -π * (a ^ 2 * t))

Tactic:
refine mul_le_mul_of_nonneg_left ?_ (pow_nonneg (Nat.cast_nonneg _) _)

Result:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ rexp (-π * ((↑n + a) ^ 2 * t)) ≤ rexp (-π * (t * ↑n ^ 2 - 2 * (|a| * (t * ↑n))) + -π * (a ^ 2 * t))

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ 0 ≤ π * t * ↑n * (|a| + a) * 2

Tactic:
refine mul_nonneg (mul_nonneg (by positivity) ?_) two_pos.le

Result:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ 0 ≤ |a| + a

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ 0 ≤ π * t * ↑n

Tactic:
positivity

Result:
no goals

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n => ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
⊢ Summable (f_nat k a t)

Tactic:
apply (this.mul_left (2 ^ k)).of_norm_bounded_eventually_nat

Result:
k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n => ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
⊢ ∀ᶠ (i : ℕ) in atTop, ‖f_nat k a t i‖ ≤ 2 ^ k * (↑i ^ k * rexp (-π * (↑i + a) ^ 2 * t))

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ 0 ≤ |a| + a

Tactic:
rw [← neg_le_iff_add_nonneg]

Result:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ -a ≤ |a|

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n => ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
⊢ ∀ᶠ (i : ℕ) in atTop, |↑i + a| ^ k ≤ (↑i + ↑i) ^ k

Tactic:
filter_upwards [eventually_ge_atTop (Nat.ceil |a|)] with n hn

Result:
case h
k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n => ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
n : ℕ
hn : ⌈|a|⌉₊ ≤ n
⊢ |↑n + a| ^ k ≤ (↑n + ↑n) ^ k

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n => ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
⊢ ∀ᶠ (i : ℕ) in atTop, ‖f_nat k a t i‖ ≤ 2 ^ k * (↑i ^ k * rexp (-π * (↑i + a) ^ 2 * t))

Tactic:
simp_rw [← mul_assoc, f_nat, norm_mul, norm_eq_abs, abs_exp,
  mul_le_mul_iff_of_pos_right (exp_pos _), ← mul_pow, abs_pow, two_mul]

Result:
k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n => ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
⊢ ∀ᶠ (i : ℕ) in atTop, |↑i + a| ^ k ≤ (↑i + ↑i) ^ k

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ rexp (-π * ((↑n + a) ^ 2 * t)) ≤ rexp (-π * (t * ↑n ^ 2 - 2 * (|a| * (t * ↑n))) + -π * (a ^ 2 * t))

Tactic:
rw [exp_le_exp, ← sub_nonneg]

Result:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ 0 ≤ -π * (t * ↑n ^ 2 - 2 * (|a| * (t * ↑n))) + -π * (a ^ 2 * t) - -π * ((↑n + a) ^ 2 * t)

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ 0 ≤ -π * (t * ↑n ^ 2 - 2 * (|a| * (t * ↑n))) + -π * (a ^ 2 * t) - -π * ((↑n + a) ^ 2 * t)

Tactic:
rw [show -π * (t * n ^ 2 - 2 * (|a| * (t * n))) + -π * (a ^ 2 * t) - -π * ((n + a) ^ 2 * t)
     = π * t * n * (|a| + a) * 2 by ring]

Result:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ 0 ≤ π * t * ↑n * (|a| + a) * 2

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ -π * (t * ↑n ^ 2 - 2 * (|a| * (t * ↑n))) + -π * (a ^ 2 * t) - -π * ((↑n + a) ^ 2 * t) = π * t * ↑n * (|a| + a) * 2

Tactic:
ring

Result:
no goals

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
⊢ Summable (f_nat k a t)

Tactic:
have : Summable fun n : ℕ ↦ n ^ k * exp (-π * (n + a) ^ 2 * t) := by
  refine (((summable_pow_mul_jacobiTheta₂_term_bound (|a| * t) ht k).mul_right
    (rexp (-π * a ^ 2 * t))).comp_injective Nat.cast_injective).of_norm_bounded _ (fun n ↦ ?_)
  simp_rw [mul_assoc, Function.comp_apply, ← Real.exp_add, norm_mul, norm_pow, Int.cast_abs,
    Int.cast_natCast, norm_eq_abs, Nat.abs_cast, abs_exp]
  refine mul_le_mul_of_nonneg_left ?_ (pow_nonneg (Nat.cast_nonneg _) _)
  rw [exp_le_exp, ← sub_nonneg]
  rw [show -π * (t * n ^ 2 - 2 * (|a| * (t * n))) + -π * (a ^ 2 * t) - -π * ((n + a) ^ 2 * t)
       = π * t * n * (|a| + a) * 2 by ring]
  refine mul_nonneg (mul_nonneg (by positivity) ?_) two_pos.le
  rw [← neg_le_iff_add_nonneg]
  apply neg_le_abs

Result:
k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n => ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
⊢ Summable (f_nat k a t)

Proof state:
case h
k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n => ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
n : ℕ
hn : ⌈|a|⌉₊ ≤ n
⊢ |↑n + a| ^ k ≤ (↑n + ↑n) ^ k

Tactic:
gcongr

Result:
case h.hab
k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n => ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
n : ℕ
hn : ⌈|a|⌉₊ ≤ n
⊢ |↑n + a| ≤ ↑n + ↑n

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
⊢ Summable fun n => ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)

Tactic:
refine (((summable_pow_mul_jacobiTheta₂_term_bound (|a| * t) ht k).mul_right
  (rexp (-π * a ^ 2 * t))).comp_injective Nat.cast_injective).of_norm_bounded _ (fun n ↦ ?_)

Result:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)‖ ≤
    ((fun i => ↑|i| ^ k * rexp (-π * (t * ↑i ^ 2 - 2 * (|a| * t) * ↑|i|)) * rexp (-π * a ^ 2 * t)) ∘ Nat.cast) n

Proof state:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ -a ≤ |a|

Tactic:
apply neg_le_abs

Result:
no goals