Zulip Chat Archive

Stream: maths

Topic: Question about Parametric Integrals


Max Bobbin (Jun 06 2022 at 14:20):

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 (Jun 06 2022 at 14:25):

You might link to the exact proof you mean

Max Bobbin (Jun 06 2022 at 14:33):

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

Patrick Massot (Jun 06 2022 at 15:15):

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

Patrick Massot (Jun 06 2022 at 15:16):

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

Max Bobbin (Jun 06 2022 at 17:13):

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 (Jun 06 2022 at 17:38):

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


Last updated: Dec 20 2023 at 11:08 UTC