Definition of Sequence Add and Mul instances in 6.1

Stream: Analysis I

[Rado Kirov]

I was struggling to prove:

theorem Sequence.add_idx (a b:Sequence) (n:ℤ) :
  (a + b) n = a n + b n := by

and it dawned on me that the definition in https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_6_1.lean#L383-L388

instance Sequence.inst_add : Add Sequence where
  add a b := {
    m := max a.m b.m
    seq n := if n ≥ max a.m b.m then a n + b n else 0
    vanish n hn := by rw [lt_iff_not_ge] at hn; simp [hn]
  }

is a bit annoying to use, and actually makes my theorem incorrect without some extra hypothesis about the index n. So I just changed the definition to

instance Sequence.inst_add : Add Sequence where
  add a b := {
    m := min a.m b.m
    seq n := a n + b n
    vanish n hn := by
      rw [lt_iff_not_ge] at hn
      simp at hn
      rw [a.vanish n hn.1, b.vanish n hn.2]
      rw [add_zero]
  }

which makes the initial theorem definitionally true. As far as I can tell there are no bad reprecussions in rest of 6.1. So would that be an acceptable change? AFAIKT the book just assumes addition is only done when the start indices align.

Also I tried to look what we did in Chapter 5, but there is slight difference there that we didn't overload + on sequence, but instead just worked with N -> R functions that we cast to Sequences, like

https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_5_3.lean#L120-L121

so we never actually did instance instance Sequence.inst_add : Add Sequence in chapter 5,

[Terence Tao]

This looks like a good change to me: make the main operation + as definitionally simple as possible, and push the difficulty to the verifying of propositional side conditions, which have much less impact on other formalization tasks due to propositional equivalence.

[Rado Kirov]

Sounds good, will send a PR tonight

[Rado Kirov]

https://github.com/teorth/analysis/pull/379