Integral mean value theorem

Stream: mathlib4

[Jeremy Parker]

I had a need for https://en.wikipedia.org/wiki/Mean_value_theorem#Mean_value_theorems_for_definite_integrals
for something I'm working on. It doesn't seem to exist in Mathlib4 though it's not hard to prove. I now want to contribute it to Mathlib, but I'm unsure where to put it.

The proof relies on IntervalIntegral.FundThmCalculus but the statement itself says nothing about derivatives. It also doesn't make sense to put it with the usual derivative MVT.

[Aaron Liu]

We do have both that the function achieves values at least the average (docs#MeasureTheory.exists_average_le) and at most the average (docs#MeasureTheory.exists_le_average) so if you import those you should be done by IVT (docs#mem_range_of_exists_le_of_exists_ge)

[Jeremy Parker]

Are you proposing this for the proof or are you saying that you don't think mathlib needs the classical result for intervalIntegral?

[Aaron Liu]

I'm proposing this for a proof

[Aaron Liu]

we should probably have all the versions

[Aaron Liu]

this proof doesn't seems to use derivatives anywhere

[Jeremy Parker]

Putting those results together as you suggest, it's not too hard to prove
∃ c ∈ uIcc a b, f c = ⨍ (x : ℝ) in a..b, f x

but really I would like to do
∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in a..b, f x
I can do this via exists_deriv_eq_slope, but it's going to be messy trying to do it via exists_le_setAverage because the latter could give one of the interval endpoints

[Jeremy Parker]

In answer to my original question about where to put it, MeasureTheory.Integral.IntervalAverage makes a lot of sense

[Aaron Liu]

Jeremy Parker said:

Putting those results together as you suggest, it's not too hard to prove
∃ c ∈ uIcc a b, f c = ⨍ (x : ℝ) in a..b, f x

but really I would like to do
∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in a..b, f x
I can do this via exists_deriv_eq_slope, but it's going to be messy trying to do it via exists_le_setAverage because the latter could give one of the interval endpoints

You have to use the stronger version which says that the set of values where the function is at least the average has positive measure

[Jeremy Parker]

That works, although it ended up being still quite messy: https://github.com/leanprover-community/mathlib4/pull/29114 I'm sure this can be refined a lot but I'm not yet experienced enough