Some additional theorems for proving ex5.5.4

Stream: Analysis I

[Rado Kirov]

To prove example 5.5.4 I proved some additional theorems that might be general enough to be worth adding to the text:

theorem Sequence.IsCauchy.abs {a:ℕ → ℚ} (ha: (a:Sequence).IsCauchy):
  ((|a| : ℕ → ℚ) : Sequence).IsCauchy := by sorry

theorem Real.LIM_abs {a:ℕ → ℚ} (ha: (a:Sequence).IsCauchy): |LIM a| = LIM |a| := by sorry

/-- variant of Real.LIM_of_le' where inequality only holds after some N -/
theorem Real.LIM_of_le' {x:Real} {a:ℕ → ℚ} (hcauchy: (a:Sequence).IsCauchy) (h: ∃ N, ∀ n ≥ N, a n ≤ x) :
    LIM a ≤ x := by sorry

Should I send a PR adding them in previous chapters? With sorries or with proofs?

Actually, I couldn't prove Real.LIM_abs myself (the other ones are easy) because I don't fully understand all the Quotient APIs used, and all other versions LIM_* were proved in the text, so I can use some help with proving that.

[Terence Tao]

Sure, these are reasonable helper lemmas to add (together with their proofs) to the file.

For Real.LIM_abs, one may first need a helper lemma that LIM a = LIM b implies LIM |a| = LIM |b|, and then one should split based on whether (LIM a).isPos, (LIM a).isNeg, or LIM a = 0 (or alternatively whether LIM a > 0, LIM a < 0, or LIM a = 0).

[Rado Kirov]

Thanks for the hints. Once I moved away from trying to use lift\2 which I don't understand, I got it down to two helper theorems with sorries, which feel doable.

theorem Sequence.abs_equiv_pos {a:ℕ → ℚ} (ha: (a: Sequence).IsCauchy)
  (hlim: LIM a > 0) : Sequence.Equiv a |a| := by
  -- by limit means a n eventually > 0, so |a n| = a n eventually
  sorry

theorem Sequence.abs_eq {a b:ℕ → ℚ}: LIM a = LIM b → LIM |a| = LIM |b| := by sorry

[Terence Tao]

You can use the second theorem to prove the first, by writing the positive quantity LIM a as LIM b for some b that is bounded away from zero (so in particular b = |b|).

[Rado Kirov]

I see now what you meant in the previous comment. Ended up just proving

theorem Real.LIM.abs_eq_pos {a: ℕ → ℚ} (h: LIM a > 0): LIM a = LIM |a|

by using theorem Real.LIM.abs_eq and using that directly in the |LIM a| = LIM |a| proof. That way I got rid of all mentions of equiv, which is a layer below LIM statements.

I think @Dan Abramov had a similar observation, but doing math in Lean makes it very clear that one of the crucial skills in writing math proofs is figuring out the right level to work in for a given proof. Generally one starts at L - 1 and staying there keeps the proof short. But once stuck there is siren call of one more unfold to get to L - 2. Things start to get messier, and in theory there should be enough APIs to never need to do that, but in practice sometimes unfolding deeper is needed - basically to find the missing API and potentially extract it when done and clean up.

It is very similar to software refactoring in regular programming, but much harder as every factored out definition needs to come with API (lemmas to work with). In theory there should be tools to help with this (AI driven now), but I wouldn't say its much of a solved problem in software engineering, so super clever refactoring for Lean is even further.

[Rado Kirov]

The final list of helper lemmas

theorem Sequence.IsCauchy.abs {a:ℕ → ℚ} (ha: (a:Sequence).IsCauchy):
  ((|a| : ℕ → ℚ) : Sequence).IsCauchy

theorem Real.LIM.abs_eq {a b:ℕ → ℚ}
    (ha: (a: Sequence).IsCauchy) (hb: (b: Sequence).IsCauchy)
    (h: LIM a = LIM b): LIM |a| = LIM |b|

theorem Real.LIM.abs_eq_pos {a: ℕ → ℚ} (h: LIM a > 0) (ha: (a:Sequence).IsCauchy)
    : LIM a = LIM |a|

theorem Real.LIM_abs {a:ℕ → ℚ} (ha: (a:Sequence).IsCauchy): |LIM a| = LIM |a|

theorem Real.LIM_of_le' {x:Real} {a:ℕ → ℚ} (hcauchy: (a:Sequence).IsCauchy) (h: ∃ N, ∀ n ≥ N, a n ≤ x) :
    LIM a ≤ x