uniqueness of variational gradient

Author: lecopivo

PhysLean/Mathematics/VariationalCalculus/Basic.lean

@@ -0,0 +1,52 @@
+/-
+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
+-/
+import Mathlib.MeasureTheory.Integral.Bochner.Basic
+import PhysLean.Mathematics.VariationalCalculus.IsTestFunction
+/-!
+
+# 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. There are
+
+-/
+
+open MeasureTheory InnerProductSpace
+
+variable
+  {X} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
+  {V} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
+
+lemma fundamental_theorem_of_variational_calculus {f : X → V}
+    (μ : Measure X)  [IsFiniteMeasureOnCompacts μ] [μ.IsOpenPosMeasure]
+    [OpensMeasurableSpace X]
+    (hf : IsTestFunction f) (hg : ∀ g, IsTestFunction g → ∫ x, ⟪f x, g x⟫_ℝ ∂μ = 0) :
+    f = 0 := by
+  have hf' := hg f hf
+  rw [MeasureTheory.integral_eq_zero_iff_of_nonneg] at hf'
+  · rw [Continuous.ae_eq_iff_eq] at hf'
+    · funext x
+      have hf'' := congrFun hf' x
+      simpa using hf''
+    · have hf : Continuous f := hf.smooth.continuous
+      fun_prop
+    · fun_prop
+  · intro x
+    simp
+    exact real_inner_self_nonneg
+  · apply IsTestFunction.integrable
+    exact IsTestFunction.inner hf hf
+
+
+-- The assumption `IsTestFunction f` can be weakened to `Continuous f`
+proof_wanted fundamental_theorem_of_variational_calculus' {f : X → V}
+  (μ : Measure X)  [IsFiniteMeasureOnCompacts μ] [μ.IsOpenPosMeasure]
+  [OpensMeasurableSpace X]
+  (hf : Continuous f) (hg : ∀ g, IsTestFunction g → ∫ x, ⟪f x, g x⟫_ℝ ∂μ = 0) :
+    f = 0

PhysLean/Mathematics/VariationalCalculus/HasVarAdjoint.lean

@@ -3,10 +3,10 @@ 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
 -/
-import Mathlib.Algebra.Lie.OfAssociative
 import Mathlib.MeasureTheory.Integral.IntegralEqImproper
-import PhysLean.Mathematics.VariationalCalculus.IsTestFunction
+import PhysLean.Mathematics.VariationalCalculus.Basic
 /-!
+
 # Variational adjoint
 
 Definition of adjoint of linear function between function spaces. It is inspired by the definition
@@ -15,6 +15,7 @@ https://en.wikipedia.org/wiki/Distribution_(mathematics) under 'Preliminaries: T
 operator' but we require that the adjoint is function between test functions too.
 
 The key results are:
+  - variational adjoint is unique on test functions
   - variational adjoint of identity is identity, `HasVarAdjoint.id`
   - variational adjoint of composition is composition of adjoint in reverse order,
     `HasVarAdjoint.comp`
@@ -55,6 +56,16 @@ structure HasVarAdjoint
   adjoint : ∀ φ ψ, IsTestFunction φ → IsTestFunction ψ →
     ∫ x, ⟪F φ x, ψ x⟫_ℝ ∂μ = ∫ x, ⟪φ x, F' ψ x⟫_ℝ ∂μ
 
+structure HasVarDual
+    (F : (X → U) → ℝ) (F' : X → U) (μ : Measure X := by volume_tac) where
+  adjoint : ∀ φ, IsTestFunction φ →
+    F φ = ∫ x, ⟪F' x, φ x⟫_ℝ ∂μ
+
+structure HasVarDual'
+    (F : X → U) (F' : (X → U) → ℝ) (μ : Measure X := by volume_tac) where
+  adjoint : ∀ φ, IsTestFunction φ →
+    ∫ x, ⟪F x, φ x⟫_ℝ ∂μ = F' φ
+
 namespace HasVarAdjoint
 
 variable {μ : Measure X}
@@ -74,16 +85,16 @@ lemma comp {F : (X → V) → (X → W)} {G : (X → U) → (X → V)} {F' G'}
     rw [hG.adjoint _ _ hφ (hF.test_fun_preserving' _ hψ)]
 
 protected lemma deriv :
-    HasVarAdjoint (fun φ : ℝ → ℝ => deriv φ) (fun φ => - deriv φ) where
-  test_fun_preserving _ hφ := by
+    HasVarAdjoint (fun φ : ℝ → ℝ => deriv φ) (fun φ x => - deriv φ x) where
+  test_fun_preserving  _ hφ := by
     have ⟨h,h'⟩ := hφ
     constructor
     · fun_prop
     · exact HasCompactSupport.deriv h'
   test_fun_preserving' _ hφ := by
     have ⟨h,h'⟩ := hφ
     constructor
-    · eta_expand; dsimp; fun_prop
+    · fun_prop
     · apply HasCompactSupport.neg'
       apply HasCompactSupport.deriv h'
   adjoint φ ψ hφ hψ := by
@@ -131,6 +142,44 @@ lemma congr_adjoint {F : (X → U) → (X → V)} {G' : (X → V) → (X → U)}
     rw [h' ψ hψ]
     exact h.adjoint φ ψ hφ hψ
 
+/-- Variational adjoint is unique only when applied to test functions. -/
+lemma unique {F : (X → U) → (X → V)} {F' G'  : (X → V) → (X → U)}
+    {μ : Measure X} [IsFiniteMeasureOnCompacts μ] [μ.IsOpenPosMeasure]
+    [OpensMeasurableSpace X] (hF' : HasVarAdjoint F F' μ) (hG' : HasVarAdjoint F G' μ)  :
+    ∀ φ, IsTestFunction φ → F' φ = G' φ := by
+  obtain ⟨F_preserve_test, F'_preserve_test, F'_adjoint⟩ := hF'
+  obtain ⟨F_preserve_test, G'_preserve_test, G'_adjoint⟩ := hG'
+  intro φ hφ
+  rw [← zero_add (G' φ)]
+  rw [← sub_eq_iff_eq_add]
+  change (F' - G') φ = 0
+  apply fundamental_theorem_of_variational_calculus μ
+  · simp
+    apply IsTestFunction.sub
+    · exact F'_preserve_test φ hφ
+    · exact G'_preserve_test φ hφ
+  · intro ψ hψ
+    simp [inner_sub_left]
+    rw [MeasureTheory.integral_sub]
+    · conv_lhs =>
+        enter [2, 2, a]
+        rw [← inner_conj_symm]
+      conv_lhs =>
+        enter [1, 2, a]
+        rw [← inner_conj_symm]
+      simp
+      rw [← F'_adjoint ψ φ hψ hφ]
+      rw [G'_adjoint ψ φ hψ hφ]
+      simp
+    · apply IsTestFunction.integrable
+      apply IsTestFunction.inner
+      · exact F'_preserve_test φ hφ
+      · exact hψ
+    · apply IsTestFunction.integrable
+      apply IsTestFunction.inner
+      · exact G'_preserve_test φ hφ
+      · exact hψ
+
 lemma neg {F : (X → U) → (X → V)} {F' : (X → V) → (X → U)}
     {μ : Measure X}
     (hF : HasVarAdjoint F F' μ) :

PhysLean/Mathematics/VariationalCalculus/HasVarGradient.lean

@@ -5,6 +5,7 @@ Authors: Tomas Skrivan, Joseph Tooby-Smith
 -/
 import PhysLean.Mathematics.VariationalCalculus.HasVarAdjoint
 import Mathlib.Tactic.FunProp.Differentiable
+import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
 /-!
 
 # Variational gradient
@@ -61,16 +62,84 @@ HasVarGradientAt
 inductive HasVarGradientAt (S' : (X → U) → (X → ℝ)) (grad : X → U) (u : X → U)
     (μ : Measure X := by volume_tac) : Prop
   | intro (F')
-      (adjoint : HasVarAdjoint (fun δu t => deriv (fun s : ℝ => S' (u + s • δu) t) 0) F' μ)
-      (eq : F' (fun _ => 1) = grad)
+      (diff : ∀ δu x, IsTestFunction δu →
+        Differentiable ℝ (fun s : ℝ => S' (fun x' => u x' + s • δu x') x))
+      (adjoint : HasVarAdjoint (fun δu x => deriv (fun s : ℝ => S' (u + s • δu) x) 0) F' μ)
+      /- This condition is effectivelly saying that `F' (fun _ => 1) = grad` but `F'` is not
+      guaranteed to produce meaningful result for `fun _ => 1` as it is not test function.
+      Therefore we require that it is possible to glue `grad` together by  -/
+      (eq : ∀ (x : X), ∃ D : Set X,
+        x ∈ D ∧ IsCompact D
+        ∧
+        ∀ (φ : X → ℝ), IsTestFunction φ → (∀ x ∈ D, φ x = 1) → F' φ x = grad x)
+
+
+lemma HasVarGradientAt.unique
+    {X : Type*} [NormedAddCommGroup X] [InnerProductSpace ℝ X]
+    [FiniteDimensional ℝ X] [MeasurableSpace X]
+    {S' : (X → U) → (X → ℝ)} {grad grad' : X → U} {u : X → U} {μ : Measure X}
+    [IsFiniteMeasureOnCompacts μ] [μ.IsOpenPosMeasure] [OpensMeasurableSpace X]
+    (h : HasVarGradientAt S' grad u μ) (h' : HasVarGradientAt S' grad' u μ) :
+    grad = grad' := by
+
+  obtain ⟨F,_,hF,eq⟩ := h
+  obtain ⟨G,_,hG,eq'⟩ := h'
+  funext x
+  obtain ⟨D,hm,hD,hgrad⟩ := eq x
+  obtain ⟨D',_,hD',hgrad'⟩ := eq' x
+
+  -- prepare test function that is one on `D ∪ D'`
+  let r := sSup ((fun x => ‖x‖) '' (D ∪ D'))
+  have : 0 ≤ r := by
+    obtain ⟨x, h1, h2, h3⟩ := IsCompact.exists_sSup_image_eq_and_ge (s :=  D ∪ D')
+      (IsCompact.union hD hD') (Set.Nonempty.inl (Set.nonempty_of_mem hm))
+      (f := fun x => ‖x‖) (by fun_prop)
+    unfold r
+    apply le_of_le_of_eq  (b := ‖x‖)
+    · exact norm_nonneg x
+    · rw [← h2]
+
+  let φ : ContDiffBump (0 : X) := {
+    rIn := r + 1,
+    rOut := r + 2,
+    rIn_pos := by linarith,
+    rIn_lt_rOut := by linarith}
+
+  -- few properties about `φ`
+  let f := fun x => φ.toFun x
+  have hφ : IsTestFunction (fun x : X => φ x) := by
+    constructor
+    apply ContDiffBump.contDiff
+    apply ContDiffBump.hasCompactSupport
+  have hφ' : ∀ x, x ∈ D ∪ D' → x ∈ Metric.closedBall 0 φ.rIn := by
+    intro x hx
+    simp [φ, r]
+    obtain ⟨y, h1, h2, h3⟩ := IsCompact.exists_sSup_image_eq_and_ge (s :=  D ∪ D')
+      (IsCompact.union hD hD') (Set.Nonempty.inl (Set.nonempty_of_mem hm))
+      (f := fun x => ‖x‖) (by fun_prop)
+    rw [h2]
+    have h3' := h3 x hx
+    apply le_trans h3'
+    simp
+  have h := hgrad φ hφ
+    (by intros _ hx; unfold φ; rw[φ.one_of_mem_closedBall]; apply hφ'; simp[hx])
+  have h' := hgrad' φ hφ
+    (by intros _ hx; unfold φ; rw[φ.one_of_mem_closedBall]; apply hφ'; simp[hx])
+  rw[← h, ← h',hF.unique hG φ hφ]
 
 /-- Variation of `S(x) = ∫ 1/2*m*‖ẋ‖² - V(x)` gives Newton's law of motion `δS(x) = - m*ẍ - V'(x)`-/
-example (m : ℝ) (u V : ℝ → ℝ) (hu : ContDiff ℝ ∞ u) (hV : ContDiff ℝ ∞ V) :
+lemma euler_lagrange_particle_1d (m : ℝ) (u V : ℝ → ℝ)
+    (hu : ContDiff ℝ ∞ u) (hV : ContDiff ℝ ∞ V) :
     HasVarGradientAt
       (fun (u : ℝ → ℝ) (t : ℝ) => 1/2 * m * deriv u t ^ 2 - V (u t))
       (fun t => - m * deriv (deriv u) t - deriv V (u t))
       u := by
   apply HasVarGradientAt.intro
+  case diff =>
+    intro _ _ hδu
+    have := hδu.1
+    have : (2:WithTop ℕ∞) ≤ ∞ := ENat.LEInfty.out
+    fun_prop (config:={maxTransitionDepth:=2}) (disch:=aesop) [deriv]
   case adjoint =>
     eta_expand
     have := hu.differentiable ENat.LEInfty.out
@@ -96,4 +165,15 @@ example (m : ℝ) (u V : ℝ → ℝ) (hu : ContDiff ℝ ∞ u) (hV : ContDiff 
       · apply HasVarAdjoint.mul_left (hψ := by fun_prop)
         apply HasVarAdjoint.id
   case eq =>
-    simp only [mul_one, deriv_const_mul_field', Pi.neg_apply, neg_mul]
+    intro x
+    use (Metric.closedBall x 1)
+    constructor
+    · simp
+    · constructor
+      · exact isCompact_closedBall x 1
+      · intro φ hφ hφ'
+        simp[hφ',hφ]
+        have h : (fun x => m * deriv u x * φ x) =ᶠ[nhds x] (fun x => m * deriv u x) :=
+          Filter.eventuallyEq_of_mem (Metric.closedBall_mem_nhds x Real.zero_lt_one)
+            (by intro x' hx'; simp[hφ' x' hx'])
+        simp[h.deriv_eq]

PhysLean/Mathematics/VariationalCalculus/IsTestFunction.lean

@@ -48,6 +48,32 @@ lemma IsTestFunction.deriv {f : ℝ → U} (hf : IsTestFunction f) :
   smooth := deriv' hf.smooth
   supp := HasCompactSupport.deriv hf.supp
 
+@[fun_prop]
+lemma IsTestFunction.add {f g : X → V} (hf : IsTestFunction f) (hg : IsTestFunction g) :
+    IsTestFunction (fun x => f x + g x) where
+  smooth := ContDiff.add hf.smooth hg.smooth
+  supp := by
+    apply HasCompactSupport.add
+    · exact hf.supp
+    · exact hg.supp
+
+@[fun_prop]
+lemma IsTestFunction.neg {f : X → V} (hf : IsTestFunction f) :
+    IsTestFunction (fun x => - f x) where
+  smooth := ContDiff.neg hf.smooth
+  supp := by
+    apply HasCompactSupport.neg' hf.supp
+
+@[fun_prop]
+lemma IsTestFunction.sub {f g : X → V} (hf : IsTestFunction f) (hg : IsTestFunction g) :
+    IsTestFunction (f - g) where
+  smooth := ContDiff.sub hf.smooth hg.smooth
+  supp := by
+    rw [SubNegMonoid.sub_eq_add_neg]
+    apply HasCompactSupport.add
+    · exact hf.supp
+    · exact HasCompactSupport.neg' hg.supp
+
 @[fun_prop]
 lemma IsTestFunction.mul {f g : X → ℝ} (hf : IsTestFunction f) (hg : IsTestFunction g) :
     IsTestFunction (fun x => f x * g x) where