Skip to content

Commit 953ed21

Browse files
committed
update docs string
1 parent 1ec2367 commit 953ed21

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
@@ -46,12 +46,6 @@ The key results are:
4646
- variational adjoint of algebraic operations is algebraic operation of adjoints,
4747
`HasVarAdjoint.neg`, `HasVarAdjoint.add`, `HasVarAdjoint.sub`, `HasVarAdjoint.mul_left`,
4848
`HasVarAdjoint.mul_right`, `HasVarAdjoint.smul_left`, `HasVarAdjoint.smul_right`
49-
50-
The variational adjoint is not uniquelly defined, having `HasVarAdjoint F F'` and
51-
`HasVarAdjoint F G'` does not imply `F' = G'`. Further investigation needs to be done. Likely
52-
the adjoint is unique almost everywhere when applied to test functions. To extend it to
53-
other functions one would have to invoke continuity and density of test function in some
54-
appropriate function space.
5549
-/
5650

5751
open InnerProductSpace MeasureTheory ContDiff

0 commit comments

Comments
 (0)