English
For a ≥ 0 and t > 0, F_nat(1, a, t) is bounded by a sum of two geometric-type terms, with explicit coefficients involving a and t.
Русский
Для a ≥ 0 и t > 0 имеется оценка F_nat(1,a,t) на сумму двух геометрических-подобных выражений, зависящих от a и t.
LaTeX
$$$\|F_{nat}(1,a,t)\| \le \dfrac{e^{-\pi (a^2+1)t}}{(1-e^{-\pi t})^2} + \dfrac{a e^{-\pi a^2 t}}{1 - e^{-\pi t}}.$$$
Lean4
theorem 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)) :=
by
refine tsum_of_norm_bounded ?_ (f_le_g_nat 1 ha ht)
unfold g_nat
simp_rw [pow_one, add_mul]
apply HasSum.add
· have h0' : ‖rexp (-π * t)‖ < 1 := by simpa only [norm_eq_abs, abs_exp] using exp_lt_aux ht
convert (hasSum_coe_mul_geometric_of_norm_lt_one h0').mul_left (exp (-π * a ^ 2 * t)) using 1
· ext1 n
rw [mul_comm (exp _), ← Real.exp_nat_mul, mul_assoc (n : ℝ), ← Real.exp_add]
ring_nf
· rw [mul_add, add_mul, mul_one, exp_add, mul_div_assoc]
· convert (hasSum_geometric_of_lt_one (exp_pos _).le <| exp_lt_aux ht).mul_left _ using 1
ext1 n
rw [← Real.exp_nat_mul, mul_assoc _ (exp _), ← Real.exp_add]
ring_nf
