OAI/Geometry/IsometricImmersion/Pulses/PulseFirstJetControl.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Pulse.scalarPulseDerivativeBound line 14
  2. theorem OAI.SmoothLocal.Pulse.scalarPulseDerivativeBound_nonneg line 17
  3. theorem OAI.SmoothLocal.Pulse.pulseScalar_eq_core line 21
  4. theorem OAI.SmoothLocal.Pulse.pulseScalar_derivative_le line 31
  5. def OAI.SmoothLocal.Pulse.scalarPulseFirstJetBound line 46
  6. theorem OAI.SmoothLocal.Pulse.scalarPulseFirstJetBound_nonneg line 49
  7. def OAI.SmoothLocal.Pulse.scalarPulseFirstJetBudget line 53
  8. theorem OAI.SmoothLocal.Pulse.scalarPulseFirstJetBudget_nonneg line 56
  9. theorem OAI.SmoothLocal.Pulse.pulseScalar_first_jet_bounds line 61
  10. theorem OAI.SmoothLocal.Pulse.thetaPulse_first_increment_bound line 83
  11. theorem OAI.SmoothLocal.Pulse.scalarPulseFirstJetBudget_tendsto_zero line 90
  12. theorem OAI.SmoothLocal.Pulse.exists_uniform_actual_pulse_lower_bound line 106