Question about Parametric Integrals

Stream: maths

[Max Bobbin]

I was looking over the parametric integral proof in the mathlib library and I was confused about the neighborhood part. The proof relates the derivative around a neighborhood of x0. I wanted to make sure that it doesn't limit the relation to a specific x0, but to all possible x0 in x.

[Ruben Van de Velde]

You might link to the exact proof you mean

[Max Bobbin]

https://leanprover-community.github.io/mathlib_docs/analysis/calculus/parametric_integral.html#has_deriv_at_integral_of_dominated_loc_of_deriv_le

[Patrick Massot]

The docstring has a copy-paste typo: you should replace "interval" by "ball". Otherwise I don't understand what you find confusing.

[Patrick Massot]

I don't know what you mean by "the derivative around a neighborhood of x0" or "all possible x0 in x".

[Max Bobbin]

Apologies, not exactly sure how to word it. I guess what I am confused about is why the proof specifies a derivative around x0 rather than it being the derivative for all x

[Max Bobbin]

Actually, I think I may have figured it out. I think what I need is better expressed from the sphere eversion project