OAI/MathematicalPhysics/AlternatingFlow/InitialNames.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AlternatingNS.Effective.ratCode line 11
  2. lemma OAI.AlternatingNS.Effective.ratCode_cast line 14
  3. lemma OAI.AlternatingNS.Effective.ratCode_primrec line 21
  4. lemma OAI.AlternatingNS.Effective.digits_eq_map line 28
  5. lemma OAI.AlternatingNS.Effective.initial_digits_primrec line 35
  6. def OAI.AlternatingNS.Effective.initialBlock line 57
  7. lemma OAI.AlternatingNS.Effective.initialBlock_primrec line 59
  8. lemma OAI.AlternatingNS.Effective.initialBlock_cast line 62
  9. lemma OAI.AlternatingNS.Effective.epsilon_named line 65
  10. lemma OAI.AlternatingNS.Effective.loadingPotential_scaled line 72