Shortcut to integration

Stream: mathlib4

[Heather Macbeth]

With the current structure of mathlib, almost all of integration depends on almost all of differentiation, for the following reason:

• the Bochner integral is defined for integrable functions
• integrable functions are defined to be functions in the $L^1$ space
• the theory of $L^p$ space (for general real $p\geq 1$) requires a variety of standard inequalities about the functions $x^p$
• these inequalities are proved from the convexity of the function $x^p$
• the convexity of $x^p$ is proved by checking its second derivative

This is mathematically rather inelegant (because we only need $L^1$ for the integral, and the convexity of the function $x^1$ is trivial). And of course, it also means that the port wouldn't reach the Bochner integral for ages.

[Heather Macbeth]

Here is a picture showing my proposed solution:
measure_theory.integral.bochner.pdf
Namely, give direct elementary proofs of the convexity of $x^p$ (and a few other functions), so no differentiation is required. This brings the length of the chain to the Bochner integral from 108 down to 97, and also cuts the length of the longest chain in mathlib down from 128 to 117. After this change, the longest unported path to the Bochner integral is

  analysis.special_functions.trigonometric.basic
- analysis.special_functions.trigonometric.angle
  analysis.special_functions.complex.arg
  analysis.special_functions.complex.log
  analysis.special_functions.pow.complex
  analysis.special_functions.pow.real
  analysis.special_functions.pow.nnreal
  analysis.special_functions.pow.asymptotics
  analysis.special_functions.pow.continuity
  measure_theory.function.lp_space
  measure_theory.function.lp_order
  measure_theory.function.l1_space
  measure_theory.function.simple_func_dense_lp
  measure_theory.integral.set_to_l1
  measure_theory.integral.bochner

[Heather Macbeth]

A first PR is #19026; this just changes the proofs, saving the file structure reorganization for a second PR.

There is a bit of a cost to this change (400 lines of very technical inequality proofs replacing 150 lines of differentiation, and changes to two already-ported files), but I think it is worth it to let us port integration and differentiation in parallel rather than in sequence.

[Moritz Doll]

Sounds good to me. Have you checked whether it is worth it splitting measure_theory.function.l1_space into a file that does all the has_finite_integral and integrable stuff and one that relates it to the L^1 space? it looks to me that this might cut down a bit of the dependency tree as well

[Heather Macbeth]

integrable is $L^1$ by definition, right? So I don't think that works.

[Moritz Doll]

docs#measure_theory.integrable says something different

[Moritz Doll]

the problem might be that the Bochner integral is for elements in L^1, so it does not help for what you want to do.

[Moritz Doll]

but if one just wants to use integrable, it feels like overkill to have all the L^p things automatically imported.

[Heather Macbeth]

What files use integrable but not integral?

[Moritz Doll]

Ah, now I understand the issue: simple functions are not used directly to define the integral, but are considered as a additive subgroup of L^1 and this is probably so that one gets continuity of the integral right away.

[Ruben Van de Velde]

Would your proposal involve restoring the original proofs after the port

[Mario Carneiro]

I hope not

[Rémy Degenne]

Nice! This is a change I started doing two years ago but did not finish because I lost the courage to keep up with the conflicts that kept accumulating because other people were changing files in that area. See the old discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20long.20pole.20in.20mathlib . This is where the isolation of derivation in files with names *_deriv originates (exp vs exp_deriv, etc).
In summary, I think this change is a good idea :)

[Heather Macbeth]

Thanks for digging up that thread, I was sure we had discussed this all before but couldn't find it. Not much has changed in 2 years it seems!

[Scott Morrison]

I think this is a great change. It's mildly sad to be giving low-level proofs of things we can do slickly with more development. But the plus side here is every single build of mathlib ever in the future being significantly faster.

Potentially we could even add some documentation, or even a file with a bunch of examples, preserving the original proofs so that people can still see the slick way to do it.

[Eric Wieser]

Does this actually reduce the total build time on finitely-parallel machines?

[Eric Wieser]

The "long pole" conversation was optimizing for infinite parallelism!

[Scott Morrison]

It's so hard to get good answers about the finitely-parallel case... I once wrote some programs to try to estimate this, but it wasn't particularly convincing. Anyway, I have lots of cores. :-)

[Scott Morrison]

I've hit merge on #19026.

[Heather Macbeth]

I still like 2021-Heather's idea to avoid needing $x^p$ at all for the Bochner integral:

Heather Macbeth said:

Another possibility is

• define [Lp_class f g] where f and g are a pair of inverse functions from ℝ≥0∞ to itself satisfying ... some list of properties
• define Lp_space to take (f : ℝ≥0∞ → ℝ≥0∞) (g : ℝ≥0∞ → ℝ≥0∞) [Lp_class f g] rather than p
• check that [Lp_class id id] and define $L^1$ to be Lp_space id id
• much later in the hierarchy, check that [Lp_class (λ x, x ^ p) (λ x, x ^ (1 / p))]

[Heather Macbeth]

but for the record, here is 2021-Scott's response:

Scott Morrison said:

Hmm, I feel like this is too far a compromise. Mathlib compiling fast is nice, and I don't mind changing from one mathematically plausible definition to another to achieve this, but [Lp_class] doesn't really have a leg to stand on mathematically. :-)

[Yaël Dillies]

As a bonus, does that by any chance give us a strictly greater generality than $L^p$ (maybe if we generalize Lp_class further)?

[Eric Wieser]

A silver lining I was seeing to this proof lengthening: it seems more likely that these new proofs (or at least, the helper lemmas they needed) generalize to weirder situations than the old ones did

[Heather Macbeth]

#19031 is the PR for the split.

[Heather Macbeth]

The build failed on this PR with a timeout but I don't really understand why -- it passed CI on an up-to-date master.

[Heather Macbeth]

The timeout is on docs#measure_theory.Lp.simple_func.normed_space

/-- If `E` is a normed space, `Lp.simple_func E p μ` is a normed space. Not declared as an
instance as it is (as of writing) used only in the construction of the Bochner integral. -/
protected def normed_space [fact (1 ≤ p)] : normed_space 𝕜 (Lp.simple_func E p μ) :=
⟨ λc f, by { rw [add_subgroup.coe_norm, add_subgroup.coe_norm, coe_smul, norm_smul] } ⟩

[Scott Morrison]

I pushed a merge with master, just in case...

[Jeremy Tan]

Everything now passes @Scott Morrison

[Mauricio Collares]

Hot take: Using the second derivative test is shorter but kind of mathematically inelegant, not just inconvenient for the porting effort. When I think of classic measure theory textbooks (e.g. papa Rudin) I can't imagine them using the second derivative test so early (if at all).

[Heather Macbeth]

I agree (although this is probably still a minority view).