OAI/MathematicalPhysics/RapidForcing/Rapid.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RapidForcing.norm_iteratedFDeriv_slice_le line 16
  2. lemma OAI.RapidForcing.uniform_derivative_bound line 41
  3. def OAI.RapidForcing.scaledCurl line 61
  4. lemma OAI.RapidForcing.scaledCurl_joint_smooth line 65
  5. lemma OAI.RapidForcing.deriv_theta_left line 87
  6. lemma OAI.RapidForcing.deriv_theta_right line 93
  7. lemma OAI.RapidForcing.scaledCurl_eq_zero_of_deriv_theta line 99
  8. lemma OAI.RapidForcing.norm_le_two_mul_of_coord_le line 108
  9. lemma OAI.RapidForcing.scaledCurl_tsupport_subset line 116
  10. lemma OAI.RapidForcing.scaledCurl_derivative_bound line 157
  11. lemma OAI.RapidForcing.cross_smul_left line 168
  12. lemma OAI.RapidForcing.cross_smul_right line 172
  13. lemma OAI.RapidForcing.curl_const_smul line 176
  14. lemma OAI.RapidForcing.curl_affine_scale line 184
  15. lemma OAI.RapidForcing.movingCurl_normalized line 198
  16. lemma OAI.RapidForcing.address_parameters_bound line 239
  17. lemma OAI.RapidForcing.norm_iteratedFDeriv_scaled line 260
  18. lemma OAI.RapidForcing.addressCurl_derivative_bound line 298
  19. lemma OAI.RapidForcing.stepVelocity_derivative_bound line 337