F_int — Mathlib

English

If a ∈ Icc(0,1) and t > 0, then F_int(k,a,t) equals F_nat(k,a,t) + F_nat(k,1−a,t).

Русский

При a ∈ Icc(0,1) и t>0 выполняется F_int(k,a,t) = F_nat(k,a,t) + F_nat(k,1−a,t).

LaTeX

$$$F_{int}(k,\bar a, t) = F_{nat}(k,\bar a, t) + F_{nat}(k,1-\bar a, t).$$$

Lean4

/-- The sum to be bounded (`ℤ` version). -/
def F_int (k : ℕ) (a : UnitAddCircle) (t : ℝ) : ℝ :=
  (show Function.Periodic (fun b ↦ ∑' (n : ℤ), f_int k b t n) 1
        by
        intro b
        simp_rw [← (Equiv.addRight (1 : ℤ)).tsum_eq (f := fun n ↦ f_int k b t n)]
        simp only [f_int, ← add_assoc, add_comm, Equiv.coe_addRight, Int.cast_add, Int.cast_one]).lift
    a

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