Putting arithmetical (+-≥≤2+2=4) lemmas into a separate file

Stream: Carleson

[Evgenia Karunus]

In Chapter 7 (probably in other chapters too?) there are a lot of lemmas/haves of the following form have size_of_D (h: 100 < D) : (100 + 4 * D ^ -2 + 8⁻¹ * D ^ -3) * D ^ -1 < 2 := by ....
These are purely arithmetical, and they don't rely on any definitions.
They are kind of bulky, so the proof itself becomes less readable and takes long to compile.

Because these lemmas don't rely on any definitions they feel like services/utils in normal programming, so I get a feeling these should be kept in a separate file, say Arithmetics.lean. We already have lemma hundred_lt_realD : 100 < D, lemma twentyfive_le_realD : 25 < D, lemma eight_le_realD: 8 < D, etc. in Defs.lean, so we could use Defs.lean for such lemmas, however we also have real definitions in Defs.lean, so a new arithmetics-specific file would probably be better.

Is it alright if I create this file and start putting such lemmas there?

Benefits:

• will make proofs less bulky without adding excessive lemmas to the search space (all theorems in this file can be excluded from in-editor/semantic search)
• will enable reuse of such calculations, pretty sure I'm just not noticing when they are repeated now

[Floris van Doorn]

Yes, putting these in a separate file sounds good. Please do that reorganization.

It might also be nice to investigate to what extend polyrith can help with such inequalities. I think polyrith is probably unable to deal with negative exponents, but after multiplying both sides of the goal with D ^ 4 (and multiplying out parentheses?) then polyrith might work, if the inequality is on the reals?

(cc @Heather Macbeth)