OAI/MathematicalPhysics/RapidForcing/SchwartzRestriction.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RapidForcing.HasSchwartzExtension line 11
  2. lemma OAI.RapidForcing.HasSchwartzExtension.zero line 21
  3. lemma OAI.RapidForcing.HasSchwartzExtension.add line 23
  4. lemma OAI.RapidForcing.HasSchwartzExtension.sub line 29
  5. lemma OAI.RapidForcing.HasSchwartzExtension.sum line 35
  6. lemma OAI.RapidForcing.HasSchwartzExtension.const_smul line 45
  7. lemma OAI.RapidForcing.HasSchwartzExtension.postcomp line 50
  8. lemma OAI.RapidForcing.HasSchwartzExtension.spatialD line 55
  9. lemma OAI.RapidForcing.HasSchwartzExtension.timeD line 68
  10. lemma OAI.RapidForcing.HasSchwartzExtension.spatialD_iterate line 81
  11. lemma OAI.RapidForcing.HasSchwartzExtension.timeD_iterate line 87
  12. lemma OAI.RapidForcing.HasSchwartzExtension.mixedD line 93
  13. lemma OAI.RapidForcing.HasSchwartzExtension.rapid line 97
  14. lemma OAI.RapidForcing.HasSchwartzExtension.smul line 118
  15. lemma OAI.RapidForcing.HasSchwartzExtension.advection line 127
  16. lemma OAI.RapidForcing.HasSchwartzExtension.laplace line 133
  17. lemma OAI.RapidForcing.HasSchwartzExtension.residual line 139
  18. theorem OAI.RapidForcing.addressed_fields_rapid line 145