How many lines for mathematical meaningless generalizations

Stream: mathlib4

[Moritz Doll]

I have a situation where (as a side product of other results) I can reduce a theorem by 180 lines if I assume that the codomain is a Banach space and not just a normed space. As a mathematician, I never deal with non-complete normed spaces, but obviously mathlib works a bit different and imposing an assumption when unused is not great. However, I think there is a very valid question on how much code we want to have for generalizing in ways that realistically never come up.

[Yury G. Kudryashov]

What's the theorem? In many cases, you can compose your function with the embedding into the completion, and get one result from the other.

[Moritz Doll]

docs#tendsto_integral_exp_inner_smul_cocompact

[Moritz Doll]

Yeah, that might work in this case

[Yury G. Kudryashov]

BTW, if E is not a complete space, then the integral is 0 by definition, right?

[Yury G. Kudryashov]

MeasureTheory.integral_def

[Moritz Doll]

ah, this is how little I care about non-complete spaces that I did not know that :sweat_smile:

[Moritz Doll]

Thanks Yury!

[Kevin Buzzard]

Regarding "realistically never come up" -- what you mean is "realistically never come up in your experience". I developed the module topology in mathlib and was very careful to make sure that the results which worked for semirings were proved for semirings (some things worked, but not all). I was careful to separate them out even though it was more work at my end and in my application I never used semirings ever (and have even ranted in the past about how they are a pointless typeclass). And then about six months ago I got an email from someone in Japan who was looking for this exact theory of topologies on modules over the tropical semiring and apparently what I'd done was exactly what they needed. So never say never!

[Ruben Van de Velde]

And if the more general result already is in mathlib, I wouldn't propose a change to shorten and weaken it without a strong motivation