OAI/Geometry/IsometricImmersion/Pulses/PulseProfiles.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Pulse.axisBump line 16
  2. theorem OAI.SmoothLocal.Pulse.axisBump_contDiff line 18
  3. theorem OAI.SmoothLocal.Pulse.axisBump_nonneg line 21
  4. theorem OAI.SmoothLocal.Pulse.axisBump_pos line 23
  5. theorem OAI.SmoothLocal.Pulse.axisBump_zero line 27
  6. theorem OAI.SmoothLocal.Pulse.axisBump_support_bound line 31
  7. theorem OAI.SmoothLocal.Pulse.axisBump_tsupport_subset line 36
  8. theorem OAI.SmoothLocal.Pulse.axisBump_hasCompactSupport line 43
  9. theorem OAI.SmoothLocal.Pulse.axisBump_pos_zero line 46
  10. theorem OAI.SmoothLocal.Pulse.axisBump_integral_pos line 49
  11. def OAI.SmoothLocal.Pulse.spatialCutoff line 53
  12. def OAI.SmoothLocal.Pulse.temporalCutoff line 55
  13. theorem OAI.SmoothLocal.Pulse.temporalCutoff_integral_pos line 57
  14. theorem OAI.SmoothLocal.Pulse.spatialCutoff_tsupport_inside line 60
  15. theorem OAI.SmoothLocal.Pulse.temporalCutoff_tsupport_inside line 66
  16. def OAI.SmoothLocal.Pulse.shearCoordinates line 71
  17. def OAI.SmoothLocal.Pulse.inverseShearCoordinates line 72
  18. def OAI.SmoothLocal.Pulse.inverseShearMatrix line 73
  19. def OAI.SmoothLocal.Pulse.thetaCovector line 74
  20. theorem OAI.SmoothLocal.Pulse.shearCoordinates_contDiff line 76
  21. theorem OAI.SmoothLocal.Pulse.inverseShearCoordinates_contDiff line 85
  22. theorem OAI.SmoothLocal.Pulse.shear_inverse line 94
  23. theorem OAI.SmoothLocal.Pulse.inverse_shear line 99
  24. theorem OAI.SmoothLocal.Pulse.inverseShearCoordinates_eq_affine line 104
  25. def OAI.SmoothLocal.Pulse.pulseScalar line 111
  26. def OAI.SmoothLocal.Pulse.pulseTensor line 115
  27. def OAI.SmoothLocal.Pulse.testMetric line 118
  28. theorem OAI.SmoothLocal.Pulse.pulseScalar_contDiff line 121
  29. theorem OAI.SmoothLocal.Pulse.pulseTensor_contDiff line 129
  30. theorem OAI.SmoothLocal.Pulse.pulseTensor_symmetric line 138
  31. def OAI.SmoothLocal.Pulse.pulseLocalBox line 143
  32. def OAI.SmoothLocal.Pulse.pulseOriginalBox line 146
  33. theorem OAI.SmoothLocal.Pulse.pulseLocalBox_isCompact line 149
  34. theorem OAI.SmoothLocal.Pulse.pulseOriginalBox_isCompact line 152
  35. theorem OAI.SmoothLocal.Pulse.pulseScalar_support_bound line 156
  36. theorem OAI.SmoothLocal.Pulse.pulseTensor_tsupport_subset line 180
  37. theorem OAI.SmoothLocal.Pulse.pulseTensor_hasCompactSupport line 192
  38. theorem OAI.SmoothLocal.Pulse.pulseOriginalBox_subset_patchBox line 198
  39. def OAI.SmoothLocal.Pulse.supportedPulse line 219
  40. theorem OAI.SmoothLocal.Pulse.pulseTensor_inverseShear line 231
  41. theorem OAI.SmoothLocal.Pulse.testMetric_inverseShear line 240