Physlib.Mathematics.VariationalCalculus.Basic

Fundamental lemma of the calculus of variations

The key took in variational calculus is: ``` ∀ h, ∫ x, f x * h x = 0 → f = 0 ``` which allows use to go from reasoning about integrals to reasoning about functions.

Overview of variational calculus

The variational calculus API in Physlib is designed to match and formalize the physicists intuition of variational calculus. It is not designed to be a general API for variational calculus.

Within variational caclulus we are interested in function transformations, `F : (X → U) → (Y → V)`. In physics this functional is often of the form `L : (Time → U) → Time → ℝ`, which represents the Lagrangian of a system. We will use this to explain the formalization within this API.

The action is nominally given by $S[u] = \int L(u, t) dt,$ however it is convenient to introduce another function `φ` and define the action as $S[u] = \int φ(t) L(u, t) dt.$ In the end we will set `φ := fun _ => 1`.

We now consider $\frac{\partial}{\partial s} S[u + s * \delta u]$ at `s = 0`, which is the variational derivative of `S` at `u` in the direction `δu`. This is equal to $\int φ(t) * \left. \frac{\partial}{\partial s} L(u + s * \delta u, t)\right|_{s = 0}dt$ Let us denote the function $\delta u,\, t \mapsto \left. \frac{\partial}{\partial s} L(u + s * \delta u, t)\right|_{s = 0}$ as `Lᵤ : (Time → U) → (Time → ℝ)`. Then the variational derivative is $\int φ (t) Lᵤ(δu, t) dt.$

It may then be possible to find a function `Gᵤ : (Time → ℝ) → Time → U` such that $\int φ(t) Lᵤ(δu, t) dt = \int \langle Gᵤ(φ, t), δu(t)\rangle dt$ This is usually done by integration by parts.

We now set `φ := fun _ => 1` and get `grad u := Gᵤ (fun _ => 1)`, which is the variational gradient at `u`. The Euler–Lagrange equations, for example, are then `grad u = 0`.

In our API, the relationship between - `Lᵤ` and `Gᵤ` is captured by the `HasVarAdjoint`. - `L` and `Gᵤ` by `HasVarAdjDeriv`. - `L` and `grad u` by `HasVarGradientAt`.

In practice we assume that `L` has a certain locality property `IsLocalizedFunctionTransform`, which allows us to work with functions `φ` and `δu` which have compact support.

This API assumes that `U` is an inner-product space. This can be considered as the full configuration space, or a local chart thereof.

References

https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/Variational.20Calculus/with/529022834

2 declarations

theorem

Fundamental Lemma of the Calculus of Variations for Continuous Functions

#fundamental_theorem_of_variational_calculus'

Let $Y$ be a finite-dimensional real inner product space and $V$ be a real inner product space. Let $\mu$ be a measure on $Y$ that is finite on compact sets and assigns strictly positive measure to every non-empty open set. If $f: Y \to V$ is a continuous function such that for every test function $g: Y \to V$ (a smooth function with compact support), the integral of their inner product vanishes, i.e., $\int_Y \langle f(x), g(x) \rangle \, d\mu(x) = 0,$ then $f(x) = 0$ for all $x \in Y$ .

theorem

Fundamental Lemma of the Calculus of Variations for Test Functions

#fundamental_theorem_of_variational_calculus

Let $X$ be a measurable space where every open set is measurable, and let $V$ be a real inner product space. Let $\mu$ be a measure on $X$ that is finite on compact sets and assigns strictly positive measure to every non-empty open set. If $f: X \to V$ is a test function (a smooth function with compact support) such that for every test function $g: X \to V$ , the integral of their inner product vanishes: $\int_X \langle f(x), g(x) \rangle \, d\mu(x) = 0,$ then $f(x) = 0$ for all $x \in X$ .