F_nat_zero_le — Mathlib

English

If a ≥ 0 and t > 0, then the norm of F_nat(0, a, t) is bounded above by the geometric-series bound rexp(-π a^2 t) / (1 - rexp(-π t)).

Русский

Если a≥0 и t>0, то ||F_nat(0,a,t)|| ≤ e^{-π a^2 t} / (1 - e^{-π t}).

LaTeX

$$$\|F_{nat}(0,a,t)\| \le \dfrac{e^{-\pi a^{2} t}}{1 - e^{-\pi t}}.$$$

Lean4

theorem F_nat_zero_le {a : ℝ} (ha : 0 ≤ a) {t : ℝ} (ht : 0 < t) :
    ‖F_nat 0 a t‖ ≤ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)) :=
  by
  refine tsum_of_norm_bounded ?_ (f_le_g_nat 0 ha ht)
  convert (hasSum_geometric_of_lt_one (exp_pos _).le <| exp_lt_aux ht).mul_left _ using 1
  ext1 n
  simp only [g_nat]
  rw [← Real.exp_nat_mul, ← Real.exp_add]
  ring_nf

Похожие утверждения