Integer-linear-form HasSum statements are closed under addition
ProvedRhinViola.integerLinearFormHasSumAddclosurehas-suminteger-linear-formrhin-viola
If two convergent series have sums in the integer lattice Z + Z alpha, then their termwise sum also has a sum in Z + Z alpha, with the two integer coefficients added.
Preamble
import Mathlib.Tactic
Formal statement
theorem RhinViola.integerLinearFormHasSumAdd
(α : ℝ) (f g : ℕ → ℝ) (z₁ z₂ c₁ c₂ : ℤ)
(hf : HasSum f ((z₁ : ℝ) + (c₁ : ℝ) * α))
(hg : HasSum g ((z₂ : ℝ) + (c₂ : ℝ) * α)) :
HasSum (fun k : ℕ => f k + g k)
(((z₁ + z₂ : ℤ) : ℝ) + (((c₁ + c₂ : ℤ) : ℝ) * α)) := by sorrySource
Elementary closure property used in the arithmetic assembly of the Rhin-Viola linear forms.