Math question about 5.3.10

Stream: Analysis I

[Li Xuanji]

I have a math question about the first part of 5.3.10, which requires us to prove that the product of two Cauchy sequences is Cauchy:

theorem Sequence.IsCauchy.mul {a b:ℕ → ℚ}  (ha: (a:Sequence).IsCauchy) (hb: (b:Sequence).IsCauchy) :
    (a * b:Sequence).IsCauchy := by sorry

I formalized a proof, but I suspect it's not what the textbook intended. I followed this proof, in particular the relevant proof state right before the calc block is

K : ℚ
h5 : K > 0
h6 : ∀ (n : ℕ), |a n| ≤ K ∧ |b n| ≤ K
ε : ℚ
hε : ε > 0
ha : |a n - a m| ≤ ε / (2 * K)
hb : |b n - b m| ≤ ε / (2 * K)
⊢ |a n * b n - a m * b m| ≤ ε

If I apply 4.3.7 like the hint suggests - and I assume I'd apply 4.3.7h - I'd get that |a n * b n - a m * b m| ≤ ε / (2 * K) * K + ε / (2 * K) * K + ε / (2 * K) * ε / (2 * K). More generally if the RHS of ha/hb are linear in ε, the upper bound provided by 4.3.7 always has a quadratic term, so [upper bound] ≤ ε is not true. This isn't insurmountable, e.g. something like min(1, ε/4K) would probably work, but it seems to be a pretty long route (even working informally) - am I missing a trick?

[Terence Tao]

You can try the trick of adding and subtracting an intermediate term to write a n * b n - a m * b m as, e.g., a n * (b n - b m) + (a n - a m) * b m.

[Li Xuanji]

Yeah, that was my proof. I guess the intended solution was to use 4.3.7(g) while I was too fixated on using 4.3.7(h)

If you translate that trick into the 4.3.7 setup, it seems to provide a different (more useful?) bound than 4.3.7(h)

-- 4.3.7h, as stated
theorem close_mul_mul {ε δ x y z w:ℚ} (hε: ε ≥ 0) (hxy: ε.Close x y) (hzw: δ.Close z w) :
    (ε*|z|+δ*|x|+ε*δ).Close (x * z) (y * w) := by sorry

-- new theorem
theorem close_mul_mul' {ε δ x y z w:ℚ} (hxy: ε.Close x y) (hzw: δ.Close z w) :
    (ε*|z|+δ*|y|).Close (x * z) (y * w) := by sorry

[Terence Tao]

It might be worth submitting a PR to include this additional theorem, with a comment that it is not from textbook but also useful (one can also add a link to this thread in that comment).