OAI/Geometry/IsometricImmersion/Pulses/PulseDerivativeBounds.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Pulse.axisBump_derivative_bound_exists line 15
  2. def OAI.SmoothLocal.Pulse.axisBumpDerivativeBound line 20
  3. theorem OAI.SmoothLocal.Pulse.axisBumpDerivativeBound_pos line 23
  4. theorem OAI.SmoothLocal.Pulse.axisBump_derivative_le line 28
  5. def OAI.SmoothLocal.Pulse.xiCLM line 35
  6. def OAI.SmoothLocal.Pulse.thetaCLM line 36
  7. def OAI.SmoothLocal.Pulse.pulseScaleBound line 39
  8. theorem OAI.SmoothLocal.Pulse.pulseScaleBound_pos line 42
  9. theorem OAI.SmoothLocal.Pulse.pulseScaleBound_xi line 46
  10. theorem OAI.SmoothLocal.Pulse.pulseScaleBound_theta line 51
  11. theorem OAI.SmoothLocal.Pulse.norm_scaled_theta_le line 56
  12. theorem OAI.SmoothLocal.Pulse.norm_scaled_xi_le line 63
  13. theorem OAI.SmoothLocal.Pulse.linear_comp_derivative_bound line 68
  14. def OAI.SmoothLocal.Pulse.derivativeConvolution line 81
  15. theorem OAI.SmoothLocal.Pulse.derivativeConvolution_nonneg line 84
  16. theorem OAI.SmoothLocal.Pulse.product_derivative_bound line 89
  17. def OAI.SmoothLocal.Pulse.pulseCore line 114
  18. theorem OAI.SmoothLocal.Pulse.pulseCore_contDiff line 118
  19. def OAI.SmoothLocal.Pulse.pulseCoreDerivativeBound line 123
  20. theorem OAI.SmoothLocal.Pulse.pulseCoreDerivativeBound_nonneg line 128
  21. theorem OAI.SmoothLocal.Pulse.pulseCore_derivative_le line 135
  22. def OAI.SmoothLocal.Pulse.thetaTensor line 176
  23. theorem OAI.SmoothLocal.Pulse.pulseTensor_eq_core line 179
  24. def OAI.SmoothLocal.Pulse.pulseDerivativeBound line 191
  25. theorem OAI.SmoothLocal.Pulse.pulseDerivativeBound_nonneg line 194
  26. theorem OAI.SmoothLocal.Pulse.pulseTensor_derivative_le line 199
  27. theorem OAI.SmoothLocal.Pulse.fixed_order_pulse_bound_tendsto_zero line 231
  28. theorem OAI.SmoothLocal.Pulse.supportedPulse_seminorm_le line 250