feat: Uniqueness of variational gradient

[lecopivo]

The main theorem of this PR is that variational gradient is unique

 HasVarGradientAt S' grad u μ → HasVarGradientAt S' grad' u μ → grad = grad'

Slightly weaker result holds for variational adjoint which is true only point wise on test functions.

  HasVarAdjoint F F' μ → HasVarAdjoint F G' μ →
  ∀ φ, IsTestFunction φ → F' φ = G' φ

[github-actions]

Thank you for your PR! The following checklist can be used to ensure that the PR is as helpful as possible and to help maintain the quality of the project.

This checklist is experimental and can be ignored if you wish.
Feel free to ask if anything is unclear, or make suggestions.

Documentation

• I have updated the module doc-strings of any modules modified, or this comment is not relevant.
• I created a new module doc-string for any new modules created, including an overall description of the module and the main results, or this comment is not relevant.
• I have changed all doc-string occurances of decleration names which I have changed, or this comment is not relevant.
• For definitions and key theorems I have added, I have added an english-readable statement of the result, which is as self-contained as possible, and where appropriate contain a readable UTF-8 version of the result.
• Where appropriate and helpful I have included references to the original source of results in the module doc-string.

Lemmas and theorems

• I have ensured that the theorem key word is reserved for important theorems, and lemma is used for everything else.
• I have ensured that no lemmas or definitions are duplications of other results.

Layout

• I have ensured that results are in the appropriate modules.

Usage of AI

Please tick one that applies to this PR:

• I have not used any AI to generate code.
• I have used basic AI coding assistance (e.g. Copilot) to generate repeative bits of code, but the lemmas and definitions are my own.
• I used AI to generate the structure of the code and/or guide its organization, but I have checked it for corectness.
• Other (please specify with a comment).

[lecopivo]

Ugh I can't git and I didn't branch from master but from lecopivo/has_var_gradient and now it thinks that all the files are brand new ... I will try to fix it

[jstoobysmith]

Yeah this happens :(. I think rebasing works git rebase origin/master

[lecopivo]

Fixed!

[jstoobysmith]

If you use

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

(where the "FIE3I" is just a unique identifier) with the import

import PhysLean.Meta.Informal.SemiFormal

then this will be added to the TODO list.

[jstoobysmith]

semiformal_result is a thin wrapper around proof_wanted just to make the TODO list work.

[lecopivo]

How am I supposed to come up with the unique identifiers?

[jstoobysmith]

"FIE3I" is unique :), but generally lake exe make_tag

[lecopivo]

fixed

[lecopivo]

Hmm id does not work. I'm getting unexpected token 'semiformal_result'; expected command

[jstoobysmith]

Sorry - my bad, the semi-formal result is required to have a doc-string (which is the thing which will actually appear in the TODO list).

[jstoobysmith]

Maybe we could put this in the ClassicalMechanics directory?

[lecopivo]

Yes this needs to be moved. I'm drafting PR where I show that variational gradient of action are Euler-Lagrange equations. This will be just a corollary.

[lecopivo]

This will be fixed in #615