Physlib.Mathematics.Calculus.ParametricIntegration
Parametric Integration
In this module we give some lemmas around parametric integration in Lean. These extend some lemmas in Mathlib, and give them in a more physics-friendly way.
6 declarations
Fréchet differentiability of for functions
Let and be real normed spaces. Let be a function such that the uncurried function is of class . For any , the parametric integral is Fréchet differentiable at , and its Fréchet derivative is given by , where denotes the Fréchet derivative of the map at .
Let and be normed spaces and be a function such that the uncurried map is continuously differentiable (). For any point and any vector , the Fréchet derivative of the parametric integral at applied to the vector is equal to the integral of the Fréchet derivative of at applied to : where denotes the Fréchet derivative.
Fréchet Derivative of equals
Let and be real normed spaces. Let be a function such that the map is continuously differentiable (). Then the Fréchet derivative of the function mapping to the integral is equal to the function mapping to the integral of the partial Fréchet derivative .
The parametric integral of a function is
Let and be normed spaces over . If a function is (first-order continuously differentiable) as a function of its joint arguments, then the function defined by the parametric interval integral is also .
The parametric integral of a function is
Let be a finite-dimensional real vector space and be a normed space. For any natural number , if a function is such that the uncurried function is of class , then the function is also of class on .
smoothness of parametric interval integrals from smoothness of the integrand
Let be a finite-dimensional, proper, real normed space, and let be a natural number. If a function (represented here in its uncurried form ) is smooth, then the parametric integral function is also smooth.
