1. Physlib
  2. Mathematics
  3. VariationalCalculus
  4. HasVarGradient
Imports
/- Copyright (c) 2025 Tomas Skrivan. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Tomas Skrivan, Joseph Tooby-Smith -/ module public import Physlib.Mathematics.VariationalCalculus.HasVarAdjDeriv

Variational gradient

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

@[expose] public section

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
inductive HasVarGradientAt (F : (X → U) → (X → ℝ)) (grad : X → U) (u : X → U) : Prop | intro (F') (hF' : HasVarAdjDerivAt F F' u) (hgrad : grad = F' (fun _ => 1))
All goals completed! 🐙X:Type u_1inst✝⁸:NormedAddCommGroup Xinst✝⁷:NormedSpace ℝ Xinst✝⁶:MeasureSpace XU:Type u_2inst✝⁵:NormedAddCommGroup Uinst✝⁴:NormedSpace ℝ Uinst✝³:InnerProductSpace' ℝ Uι:Typeinst✝²:Fintype ιF:ι → (X → U) → X → ℝgrad:ι → X → Uu:X → Uhu:ContDiff ℝ ∞ uinst✝¹:OpensMeasurableSpace Xinst✝:IsFiniteMeasureOnCompacts volumeh:∀ (i : ι), HasVarGradientAt (F i) (grad i) uP:(ι : Type) → [Fintype ι] → Prop := fun ι [Fintype ι] => ∀ (F : ι → (X → U) → X → ℝ) (F' : ι → X → U) (u : X → U), ContDiff ℝ ∞ u → (∀ (i : ι), HasVarGradientAt (F i) (F' i) u) → HasVarGradientAt (fun φ x => ∑ i, F i φ x) (∑ i, F' i) uhp:P ι⊢ HasVarGradientAt (fun v x => ∑ i, F i v x) (∑ i, grad i) u All goals completed! 🐙All goals completed! 🐙@[inherit_doc varGradient] macro "δ" u:term ", " "∫ " x:term ", " b:term : term => `(varGradient (fun $u $x => $b))@[inherit_doc varGradient] macro "δ" "(" u:term " := " u':term ")" ", " "∫ " x:term ", " b:term : term => `(varGradient (fun $u $x => $b) $u')All goals completed! 🐙