Physlib Documentation

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

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 #

source
theorem fundamental_theorem_of_variational_calculus' {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] {Y : Type u_1} [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [FiniteDimensional ℝ Y] [MeasurableSpace Y] {f : Y → V} (μ : MeasureTheory.Measure Y) [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.IsOpenPosMeasure] [OpensMeasurableSpace Y] (hf : Continuous f) (hg : ∀ (g : Y → V), IsTestFunction g → ∫ (x : Y), inner ℝ (f x) (g x) ∂μ = 0) :
f = 0

A version of fundamental_theorem_of_variational_calculus' for Continuous f. The proof uses assumption that source of f is finite-dimensional inner-product space, so that a bump function with compact support exists via ContDiffBump.hasCompactSupport from Analysis.Calculus.BumpFunction.Basic.

The proof is by contradiction, assume that there is x₀ such that f x₀ ≠ 0 then one construct construct g test function supported on the neighborhood of x₀ such that ⟪f x, g x⟫ ≥ 0 and ⟪f x, g x⟫ > 0 on a neighborhood of x₀.

Using Y for the theorem below to make use of bump functions in InnerProductSpaces. Y is a finite dimensional measurable space over ℝ with (standard) inner product.

source
theorem fundamental_theorem_of_variational_calculus {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] {f : X → V} (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.IsOpenPosMeasure] [OpensMeasurableSpace X] (hf : IsTestFunction f) (hg : ∀ (g : X → V), IsTestFunction g → ∫ (x : X), inner ℝ (f x) (g x) ∂μ = 0) :
f = 0