feat: Tweak definition of HasVarAdjoint

[lecopivo]

Generalize variational adjoint to functions of type (X → U) → (Y → V). The main purpose of this allow for change of variables. For example the function:

(· ∘ equiv) : (Space 3 → ℝ) → (ℝ×ℝ×ℝ → ℝ)

has adjoint

(· ∘ equiv.symm) :  (ℝ×ℝ×ℝ → ℝ) →(Space 3 → ℝ) 

for equiv : ℝ×ℝ×ℝ ≃ Space 3

Additionally

• I have removed the condition K ⊆ L from HasVarAdjoint.ext as it does not make sense anymore and it wasn't necessary.
• I have removed the μ parameter. Everything is now done on MeasureSpace. I can not think of an application where a special measure would be needed.

[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).