OAI/Geometry/IsometricImmersion/Pulses/PulseTestEnergy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Pulse.pulseTest_contDiff line 14
  2. theorem OAI.SmoothLocal.Pulse.pulseTest_hasDerivAt line 17
  3. theorem OAI.SmoothLocal.Pulse.pulseTest_deriv line 26
  4. def OAI.SmoothLocal.Pulse.pulseTestDerivativeBound line 31
  5. theorem OAI.SmoothLocal.Pulse.pulseTestDerivativeBound_nonneg line 34
  6. theorem OAI.SmoothLocal.Pulse.pulseTest_deriv_bound line 38
  7. theorem OAI.SmoothLocal.Pulse.real_Icc_memLp_two line 63
  8. theorem OAI.SmoothLocal.Pulse.sqrt_Icc_square_le_of_abs line 68
  9. theorem OAI.SmoothLocal.Pulse.real_Icc_pairing_bound line 83
  10. theorem OAI.SmoothLocal.Pulse.pulse_strip_pairing_bound line 92
  11. theorem OAI.SmoothLocal.Pulse.pulse_derivative_pairing_delta_sq line 137
  12. theorem OAI.SmoothLocal.Pulse.pulse_test_pairing_extra_inv_tau line 159