feat: Uniqueness of variational gradient

PhysLean.lean

@@ -35,6 +35,7 @@ import PhysLean.Mathematics.RatComplexNum
 import PhysLean.Mathematics.SO3.Basic
 import PhysLean.Mathematics.SchurTriangulation
 import PhysLean.Mathematics.SpecialFunctions.PhysHermite
+import PhysLean.Mathematics.VariationalCalculus.Basic
 import PhysLean.Mathematics.VariationalCalculus.HasVarAdjoint
 import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
 import PhysLean.Mathematics.VariationalCalculus.IsTestFunction

PhysLean/Mathematics/VariationalCalculus/Basic.lean

@@ -0,0 +1,56 @@
+/-
+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
+import PhysLean.Meta.Informal.SemiFormal
+/-!
+
+# 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 only [Pi.zero_apply]
+    exact real_inner_self_nonneg
+  · apply IsTestFunction.integrable
+    exact IsTestFunction.inner hf hf
+
+/-- The assumption `IsTestFunction f` `in fundamental_theorem_of_variational_calculus` can be
+weakened to `Continuous f`.
+
+The proof is by contradiction, assume that there is `x₀` such that `f x₀` then you can easily
+ construct `g` test function with support on the neighborhood of `x₀` such that `⟪f x, g x⟫ ≥ 0`. -/
+semiformal_result "FIE3I" 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,9 +3,8 @@ 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
 
@@ -15,19 +14,14 @@ 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`
   - variational adjoint of deriv is `- deriv`, `HasVarAdjoint.deriv`
   - variational adjoint of algebraic operations is algebraic operation of adjoints,
     `HasVarAdjoint.neg`, `HasVarAdjoint.add`, `HasVarAdjoint.sub`, `HasVarAdjoint.mul_left`,
     `HasVarAdjoint.mul_right`, `HasVarAdjoint.smul_left`, `HasVarAdjoint.smul_right`
-
-The variational adjoint is not uniquelly defined, having `HasVarAdjoint F F'` and
-`HasVarAdjoint F G'` does not imply `F' = G'`. Further investigation needs to be done. Likely
-the adjoint is unique almost everywhere when applied to test functions. To extend it to
-other functions one would have to invoke continuity and density of test function in some
-appropriate function space.
 -/
 
 open InnerProductSpace MeasureTheory ContDiff
@@ -74,7 +68,7 @@ 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
+    HasVarAdjoint (fun φ : ℝ → ℝ => deriv φ) (fun φ x => - deriv φ x) where
   test_fun_preserving _ hφ := by
     have ⟨h,h'⟩ := hφ
     constructor
@@ -83,7 +77,7 @@ protected lemma deriv :
   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 +125,41 @@ 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[← F'_adjoint ψ φ hψ hφ,G'_adjoint ψ φ hψ hφ]
+    · 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,83 @@ 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 +164,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