OAI/Geometry/IsometricImmersion/Pulses/PulseMomentGeometry.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Pulse.pulseStrip line 15
  2. def OAI.SmoothLocal.Pulse.pulsePairRectangle line 17
  3. def OAI.SmoothLocal.Pulse.pulsePairPoint line 19
  4. def OAI.SmoothLocal.Pulse.pulseTest line 20
  5. def OAI.SmoothLocal.Pulse.pulseMomentWeight line 21
  6. def OAI.SmoothLocal.Pulse.pulseWeightedMoment line 23
  7. theorem OAI.SmoothLocal.Pulse.pulsePairRectangle_isCompact line 27
  8. theorem OAI.SmoothLocal.Pulse.pulsePairPoint_continuous line 30
  9. theorem OAI.SmoothLocal.Pulse.pulsePairPoint_mem line 34
  10. theorem OAI.SmoothLocal.Pulse.pulseStrip_zero_mem line 38
  11. theorem OAI.SmoothLocal.Pulse.pulsePair_integrableOn line 42
  12. theorem OAI.SmoothLocal.Pulse.pulsePair_integral_eq_rectangleIntegral line 49
  13. theorem OAI.SmoothLocal.Pulse.pulseMomentWeight_continuous line 67
  14. theorem OAI.SmoothLocal.Pulse.pulseMomentWeight_nonneg line 73
  15. theorem OAI.SmoothLocal.Pulse.pulseTest_continuous line 77
  16. theorem OAI.SmoothLocal.Pulse.pulseTest_hasCompactSupport line 80
  17. theorem OAI.SmoothLocal.Pulse.spatial_moment_Icc_eq line 83
  18. theorem OAI.SmoothLocal.Pulse.temporal_pulse_integral line 94
  19. theorem OAI.SmoothLocal.Pulse.pulseMomentWeight_integral line 118