OAI/Analysis/AncientFlat/Kernel/AdjointKernel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FlatDuality.adjointTime line 12
  2. def OAI.FlatDuality.adjointAmplitude line 13
  3. lemma OAI.FlatDuality.adjointTime_bounds line 14
  4. lemma OAI.FlatDuality.adjointAmplitude_bounds line 23
  5. lemma OAI.FlatDuality.hasDerivAt_adjointTime line 26
  6. lemma OAI.FlatDuality.hasDerivAt_adjointAmplitude line 31
  7. lemma OAI.FlatDuality.contDiff_adjointTime line 36
  8. lemma OAI.FlatDuality.contDiff_adjointAmplitude line 37
  9. lemma OAI.FlatDuality.laplacian_translate line 38
  10. lemma OAI.FlatDuality.bilaplacian_translate line 41
  11. def OAI.FlatDuality.adjointSchwartz line 46
  12. lemma OAI.FlatDuality.adjointSchwartz_apply line 48
  13. lemma OAI.FlatDuality.adjointSchwartz_bilap line 52
  14. lemma OAI.FlatDuality.adjointSchwartz_equation line 69