Taylor with integral form of the remainder

Stream: mathlib4

[Yizheng Zhu]

I cannot find Taylor's theorem with integral form of the remainder yet, with either C(k+1) assumption or the stronger k-th derivative absolutely continuous assumption. So I want to fill the gap.

Because absolute continuity of functions are not in Mathlib yet (as far as I can tell), my plan is to put absolute continuity of functions in Mathlib.MeasureTheory.Function, add relevant theorems in Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus and Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts, and finally prove Taylor with both versions of assumptions in Mathlib.Analysis.Calculus.Taylor.

Suggestions are welcome.

[Kenny Lau]

@Yizheng Zhu UniformContinuous

[Etienne Marion]

This is not the same as absolute continuity

[Kenny Lau]

right; and there's no absolute continuity in mathlib?

[Sébastien Gouëzel]

@Yizheng Zhu, if you define absolute continuity, it's probably a good idea to put it in its own file where you would also develop the theory (like proving that Lipschitz functions are absolutely continuous, for instance): it's probably too big to fit naturally in another file.

[Yizheng Zhu]

Sébastien Gouëzel said:

Yizheng Zhu, if you define absolute continuity, it's probably a good idea to put it in its own file where you would also develop the theory (like proving that Lipschitz functions are absolutely continuous, for instance): it's probably too big to fit naturally in another file.

Yes. I plan to create a folder Mathlib/MeasureTheory/Function/AbsolutelyContinuous with files like Basic.lean etc. The integral part will probably be in a file like AbsCont.lean in the existing folder Mathlib/MeasureTheory/Integral/IntervalIntegral.

[Bingyu Xia]

I did something related to absolutely continuous functions in
https://github.com/BryceT233/two-basic-results-on-absolutely-continuous-functions/tree/main
where I am using the antiderivative of a Lebesgue integrable function as a quick definition for absolutely continuous functions

[Yizheng Zhu]

Bingyu Xia said:

I did something related to absolutely continuous functions in
https://github.com/BryceT233/two-basic-results-on-absolutely-continuous-functions/tree/main
where I am using the antiderivative of a Lebesgue integrable function as a quick definition for absolutely continuous functions

Thanks! This is the interval version of Lebesgue Differentiation Theorem that I actually need for proving FTC (in the form ∫ f' = f) from the ε-δ definition of absolute continuous. It really helps.

Edit: However, I think I will use VitaliFamily.ae_tendsto_average instead. The path from this version should be shorter.

[Yizheng Zhu]

I find that mathlib4 is missing a basic lemma: If f is monotone on [a, b], then f' is integrable on [a, b]. Proved using Fatou. Only then can we replace monotone with BV and finally absolutely continuous.

[Sébastien Gouëzel]

We have docs#intervalIntegral.integrableOn_deriv_right_of_nonneg proving that if the derivative is nonnegative then it is integrable. It's essentially the same as your lemma but phrased just a little bit differently. (See also the neighboring lemmas for results of the same flavor).

[Sébastien Gouëzel]

(With docs#HasDerivWithinAt.nonneg_of_monotoneOn, one can deduce the nonnegativity of the derivative from monotonicity)

[Sébastien Gouëzel]

The version I'm giving, though, assumes that f is differentiable everywhere. If it's only integrable almost everywhere (i.e., if you assume monotonicity but no differentiability), then another argument is indeed needed.

[Yizheng Zhu]

The absolutely continuous part is in PR 29092.