Skip to content

Commit 504d8cd

Browse files
committed
update docs string
1 parent 49a6376 commit 504d8cd

File tree

1 file changed

+0
-6
lines changed

1 file changed

+0
-6
lines changed

PhysLean/Mathematics/VariationalCalculus/HasVarAdjoint.lean

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -23,12 +23,6 @@ The key results are:
2323
- variational adjoint of algebraic operations is algebraic operation of adjoints,
2424
`HasVarAdjoint.neg`, `HasVarAdjoint.add`, `HasVarAdjoint.sub`, `HasVarAdjoint.mul_left`,
2525
`HasVarAdjoint.mul_right`, `HasVarAdjoint.smul_left`, `HasVarAdjoint.smul_right`
26-
27-
The variational adjoint is not uniquelly defined, having `HasVarAdjoint F F'` and
28-
`HasVarAdjoint F G'` does not imply `F' = G'`. Further investigation needs to be done. Likely
29-
the adjoint is unique almost everywhere when applied to test functions. To extend it to
30-
other functions one would have to invoke continuity and density of test function in some
31-
appropriate function space.
3226
-/
3327

3428
open InnerProductSpace MeasureTheory ContDiff

0 commit comments

Comments
 (0)