OAI/Analysis/AncientFlat/Kernel/AdjointPairDerivative.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FlatDuality.schwartz_bilap_fun line 12
2. lemma OAI.FlatDuality.moving_boundedJets line 17
3. def OAI.FlatDuality.deviationTest line 24
4. def OAI.FlatDuality.potentialTest line 26
5. def OAI.FlatDuality.adjointError line 28
6. lemma OAI.FlatDuality.deviationTest_apply line 30
7. lemma OAI.FlatDuality.potentialTest_apply line 34
8. lemma OAI.FlatDuality.integral_adjoint_cancel line 38
9. lemma OAI.FlatDuality.hasDerivAt_adjoint_pair line 80