OAI/MathematicalPhysics/RapidForcing/Profiles.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RapidForcing.Machine.initialDigit_eq line 11
  2. lemma OAI.RapidForcing.Machine.initialDigit_lt line 16
  3. lemma OAI.RapidForcing.Machine.terminalDigit_le_one line 36
  4. lemma OAI.RapidForcing.vec_zero_coord line 42
  5. lemma OAI.RapidForcing.vec_one_coord line 43
  6. lemma OAI.RapidForcing.vec_two_coord line 44
  7. lemma OAI.RapidForcing.vec_all_zero line 45
  8. lemma OAI.RapidForcing.theta_nonneg line 49
  9. lemma OAI.RapidForcing.theta_le_one line 50
  10. lemma OAI.RapidForcing.theta_zero line 51
  11. lemma OAI.RapidForcing.theta_one line 53
  12. lemma OAI.RapidForcing.theta_smooth line 55
  13. def OAI.RapidForcing.supportBox line 59
  14. lemma OAI.RapidForcing.supportBox_closed line 61
  15. lemma OAI.RapidForcing.zeta_nonneg line 68
  16. lemma OAI.RapidForcing.zeta_le_one line 73
  17. lemma OAI.RapidForcing.zeta_zero line 81
  18. lemma OAI.RapidForcing.zeta_one line 92
  19. lemma OAI.RapidForcing.zeta_smooth line 99
  20. lemma OAI.RapidForcing.curl_tsupport_subset line 103
  21. lemma OAI.RapidForcing.movingCurl_tsupport_subset line 111