OAI/Geometry/PolarProducts/MoserField.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Moser.spatialField line 26
  2. theorem OAI.Moser.spatialField_eq_zero_of_oneForm_eq_zero line 31
  3. theorem OAI.Moser.contract_spatialField line 37
  4. theorem OAI.Moser.oneForm_spatialField line 44
  5. theorem OAI.Moser.contDiff_spatialField line 56
  6. theorem OAI.Moser.hasCompactSupport_spatialField line 78
  7. theorem OAI.Moser.exists_lipschitz_spaceTimeField line 94
  8. def OAI.Moser.extendedOneForm line 124
  9. theorem OAI.Moser.extendedOneForm_apply line 128
  10. theorem OAI.Moser.contDiff_extendedOneForm line 131
  11. theorem OAI.Moser.fderiv_extendedOneForm line 136
  12. def OAI.Moser.spatialTensor line 161
  13. def OAI.Moser.spaceTimeTensor line 165
  14. theorem OAI.Moser.contDiffAt_spatialTensor line 170
  15. theorem OAI.Moser.contDiffAt_spaceTimeTensor line 179
  16. theorem OAI.Moser.spaceTimeTensor_apply line 189
  17. theorem OAI.Moser.spaceTimeTensor_skew line 199
  18. theorem OAI.Moser.spaceTimeTensor_closed line 207
  19. theorem OAI.Moser.spaceTimeTensor_kernel line 229
  20. def OAI.Moser.timeCutoff line 261
  21. theorem OAI.Moser.timeCutoff_smooth line 263
  22. theorem OAI.Moser.timeCutoff_mem line 265
  23. theorem OAI.Moser.timeCutoff_zero line 268
  24. theorem OAI.Moser.timeCutoff_one line 270
  25. theorem OAI.Moser.timeCutoff_deriv_smooth line 272
  26. theorem OAI.Moser.timeCutoff_deriv_hasCompactSupport line 275