splitting up measure_theory.integral.interval_integral

Stream: general

[David Loeffler]

The file measure_theory.integral.interval_integral is about 2800 lines long, one of the top ten longest in the library; this makes it very unwieldy to work on, and it will be still worse to port. It splits almost exactly into two 1400-line chunks: the first half is definitions and elementary properties of interval integrals; the second half is variants of the Fundamental Theorem of Calculus. Would anyone object to splitting it into two files interval_integral and fund_thm_calculus?

[David Loeffler]

(I have made PR #18898 for this.)

[Yaël Dillies]

I'm happy with the split but in general it would be nice for people not to wake up to a library-changing decision having happened in their sleep :grinning:

[Mario Carneiro]

then you should sleep less :stuck_out_tongue:

[Eric Wieser]

I agree with @Yaël Dillies' sentiment but I don't think it a file split is particularly "library changing". If someone decided to unbundle all of the algebra morphisms overnight I'd be a little less happy!

[Yaël Dillies]

Yeah absolutely! This is a "in general" remark.

[David Loeffler]

I agree with @Yaël Dillies' sentiment but I don't think it a file split is particularly "library changing"

Quite – this split has essentially no repercussions elsewhere in the library, just fixing a few imports so they point at the right half.

There are a few other super-long files which are still un-ported, but I don't know if they would divide up as neatly as that one did:

    3256   src/analysis/calculus/fderiv.lean
    3088   src/measure_theory/function/lp_space.lean
    3065   src/measure_theory/integral/lebesgue.lean
    2888   src/analysis/calculus/cont_diff.lean

[Scott Morrison]

@David Loeffler if you or others would nevertheless like to try splitting any of those four I'd be very much in favour!

[David Loeffler]

#18904 gets measure_theory/integral/lebesgue.lean down from 3000 lines to 2000, by moving the stuff in the simple_func namespace to a new file.

[Scott Morrison]

@David Loeffler, looks great. I've delegated, so please merge if CI is green.