Variational gradient

Definition of variational gradient that allows for formal treatement of variational calculus as used in physics textbooks.

inductive HasVarGradientAt {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] (F : (X → U) → X → ℝ) (grad u : X → U) : Prop

Function grad is variational gradient of functional S at point u.

This formalizes the notion of variational gradient δS/δu of a functional S at a point u.

However, it is not defined for a functional S : (X → U) → ℝ but rather for the function S' : (X → U) → (X → ℝ) which is related to the usual functional as S u = ∫ x, S' (u x) x ∂μ. For example for action integral, S u = ∫ t, L (u t) (deriv u t) we have S' u t = L (u t) (deriv u t). Working with S' rather than with S allows us to ignore certain technicalities with integrability.

Examples:

Euler-Lagrange equations:

δ/δx ∫ L(x,ẋ) dt = ∂L/∂ x - d/dt (∂L/∂ẋ)

can be expressed as

HasVarGradientAt
  (fun u t => L (u t) (deriv u t))
  (fun t =>
    deriv (L · (deriv u t)) ((u t))
    -
    deriv (fun t' => deriv (L (u t') ·) (deriv u t')) t)
  u

Laplace equation is variational gradient of Dirichlet energy:

δ/δu ∫ 1/2*‖∇u‖² = - Δu

can be expressed as

HasVarGradientAt
  (fun u t => 1/2 * deriv u t^2)
  (fun t => - deriv (deriv u) t)
  u

• intro {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] {F : (X → U) → X → ℝ} {grad u : X → U} (F' : (X → ℝ) → X → U) (hF' : HasVarAdjDerivAt F F' u) (hgrad : grad = F' fun (x : X) => 1) : HasVarGradientAt F grad u

noncomputable def varGradient {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] (F : (X → U) → X → ℝ) (u : X → U) : X → U

The variational gradient of a function F : (X → U) → (X → ℝ) evaulated at a function u : X → U.

This not defined defined for a functional S : (X → U) → ℝ but rather for the function F : (X → U) → (X → ℝ) which is the integrand of the functional S u = ∫ x, F (u x) x ∂μ. For example for action integral, S u = ∫ t, L (u t) (deriv u t) we have S' u t = L (u t) (deriv u t).

On functions F : (X → U) → (X → ℝ) which do not have a variational gradient, this function is defined to give 0.

Equations

• varGradient F u = if h : ∃ (grad : X → U), HasVarGradientAt F grad u then Classical.choose h else 0

def «termδ_,∫_,_» : Lean.ParserDescr

The variational gradient of a function F : (X → U) → (X → ℝ) evaulated at a function u : X → U.

This not defined defined for a functional S : (X → U) → ℝ but rather for the function F : (X → U) → (X → ℝ) which is the integrand of the functional S u = ∫ x, F (u x) x ∂μ. For example for action integral, S u = ∫ t, L (u t) (deriv u t) we have S' u t = L (u t) (deriv u t).

On functions F : (X → U) → (X → ℝ) which do not have a variational gradient, this function is defined to give 0.

Equations

• One or more equations did not get rendered due to their size.

def «termδ(_:=_),∫_,_» : Lean.ParserDescr

The variational gradient of a function F : (X → U) → (X → ℝ) evaulated at a function u : X → U.

This not defined defined for a functional S : (X → U) → ℝ but rather for the function F : (X → U) → (X → ℝ) which is the integrand of the functional S u = ∫ x, F (u x) x ∂μ. For example for action integral, S u = ∫ t, L (u t) (deriv u t) we have S' u t = L (u t) (deriv u t).

On functions F : (X → U) → (X → ℝ) which do not have a variational gradient, this function is defined to give 0.

Equations

• One or more equations did not get rendered due to their size.

theorem HasVarGradientAt.unique {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] [MeasureTheory.MeasureSpace X] [OpensMeasurableSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] [MeasureTheory.volume.IsOpenPosMeasure] {S' : (X → U) → X → ℝ} {grad grad' u : X → U} (h : HasVarGradientAt S' grad u) (h' : HasVarGradientAt S' grad' u) : grad = grad'

theorem HasVarGradientAt.varGradient {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [FiniteDimensional ℝ X] [MeasureTheory.MeasureSpace X] [OpensMeasurableSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] [MeasureTheory.volume.IsOpenPosMeasure] (F : (X → U) → X → ℝ) (grad u : X → U) (hF : HasVarGradientAt F grad u) : varGradient F u = grad