Physlib

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

theorem

Fréchet differentiability of 01F(x,t)dt\int_0^1 F(x, t) \, dt for C1C^1 functions FF

Let MM and NN be real normed spaces. Let F:MRNF: M \to \mathbb{R} \to N be a function such that the uncurried function (x,t)F(x,t)(x, t) \mapsto F(x, t) is of class C1C^1. For any x0Mx_0 \in M, the parametric integral x01F(x,t)dtx \mapsto \int_0^1 F(x, t) \, dt is Fréchet differentiable at x0x_0, and its Fréchet derivative is given by 01DxF(x0,t)dt\int_0^1 \text{D}_x F(x_0, t) \, dt, where DxF(x0,t)\text{D}_x F(x_0, t) denotes the Fréchet derivative of the map xF(x,t)x \mapsto F(x, t) at x0x_0.

theorem

D(01F(x,t)dt)(x0)v=01(DxF(x0,t)v)dtD \left( \int_0^1 F(x, t) \, dt \right) (x_0) v = \int_0^1 \left( D_x F(x_0, t) v \right) \, dt

Let MM and NN be normed spaces and F:MRNF : M \to \mathbb{R} \to N be a function such that the uncurried map (x,t)F(x,t)(x, t) \mapsto F(x, t) is continuously differentiable (C1C^1). For any point x0Mx_0 \in M and any vector vMv \in M, the Fréchet derivative of the parametric integral x01F(x,t)dtx \mapsto \int_0^1 F(x, t) \, dt at x0x_0 applied to the vector vv is equal to the integral of the Fréchet derivative of xF(x,t)x \mapsto F(x, t) at x0x_0 applied to vv: D(01F(x,t)dt)(x0)v=01(DxF(x0,t)v)dt D \left( \int_0^1 F(x, t) \, dt \right) (x_0) v = \int_0^1 \left( D_x F(x_0, t) v \right) \, dt where DD denotes the Fréchet derivative.

theorem

Fréchet Derivative of 01F(x,t)dt\int_0^1 F(x, t) dt equals 01DxF(x,t)dt\int_0^1 \text{D}_x F(x, t) dt

Let MM and NN be real normed spaces. Let F:M×RNF : M \times \mathbb{R} \to N be a function such that the map (x,t)F(x,t)(x, t) \mapsto F(x, t) is continuously differentiable (C1C^1). Then the Fréchet derivative of the function mapping xMx \in M to the integral 01F(x,t)dt\int_0^1 F(x, t) \, dt is equal to the function mapping xx to the integral of the partial Fréchet derivative 01DxF(x,t)dt\int_0^1 \text{D}_x F(x, t) \, dt.

theorem

The parametric integral of a C1C^1 function is C1C^1

Let MM and NN be normed spaces over R\mathbb{R}. If a function F:M×RNF: M \times \mathbb{R} \to N is C1C^1 (first-order continuously differentiable) as a function of its joint arguments, then the function g:MNg: M \to N defined by the parametric interval integral g(x)=01F(x,t)dtg(x) = \int_{0}^{1} F(x, t) \, dt is also C1C^1.

theorem

The parametric integral of a Cn+1C^{n+1} function is Cn+1C^{n+1}

Let MM be a finite-dimensional real vector space and NN be a normed space. For any natural number nn, if a function F:M×RNF: M \times \mathbb{R} \to N is such that the uncurried function (x,t)F(x,t)(x, t) \mapsto F(x, t) is of class Cn+1C^{n+1}, then the function x01F(x,t)dtx \mapsto \int_{0}^{1} F(x, t) \, dt is also of class Cn+1C^{n+1} on MM.

theorem

CnC^n smoothness of parametric interval integrals from CnC^n smoothness of the integrand

Let MM be a finite-dimensional, proper, real normed space, and let nn be a natural number. If a function F:M×RNF: M \times \mathbb{R} \to N (represented here in its uncurried form F\text{↿}F) is CnC^n smooth, then the parametric integral function x01F(x,t)dtx \mapsto \int_0^1 F(x, t) \, dt is also CnC^n smooth.