F_int_eq_of_mem_Icc — Mathlib

English

F_int is the periodic extension over the integer lattice of the sum ∑' f_int(k, b, t, n) in n, parameterized by a on a circle.

Русский

F_int — периодическое продолжение по целой решётке суммы ∑' f_int(k,b,t,n) по параметру b на окружности.

LaTeX

$$$F_{int}(k, a, t) = \left( \sum_{n \in \mathbb{Z}} f_{int}(k, a, t, n) \right)_{\text{periodic}}.$$$

Lean4

theorem F_int_eq_of_mem_Icc (k : ℕ) {a : ℝ} (ha : a ∈ Icc 0 1) {t : ℝ} (ht : 0 < t) :
    F_int k a t = (F_nat k a t) + (F_nat k (1 - a) t) :=
  by
  simp only [F_int, F_nat, Function.Periodic.lift_coe]
  convert ((summable_f_nat k a ht).hasSum.int_rec (summable_f_nat k (1 - a) ht).hasSum).tsum_eq using 3 with n
  cases n
  · rw [f_int_ofNat _ ha.1]
  · rw [f_int_negSucc _ ha.2]

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