OAI/Computability/MinUncut/Search/ParameterFields.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncut.Preprocess.InnerDataRaw line 9
  2. def OAI.MinUncut.Preprocess.innerDataEquiv line 10
  3. instance OAI.MinUncut.Preprocess.innerDataPrimcodable line 15
  4. lemma OAI.MinUncut.Preprocess.c_innerData_s line 16
  5. lemma OAI.MinUncut.Preprocess.c_innerData_m line 18
  6. lemma OAI.MinUncut.Preprocess.c_innerData_k line 20
  7. lemma OAI.MinUncut.Preprocess.c_innerData_n line 22
  8. lemma OAI.MinUncut.Preprocess.c_innerData_H line 24
  9. lemma OAI.MinUncut.Preprocess.c_innerData_A line 26
  10. lemma OAI.MinUncut.Preprocess.c_innerData_γ line 28
  11. lemma OAI.MinUncut.Preprocess.c_innerData_p line 30
  12. lemma OAI.MinUncut.Preprocess.c_innerData_θ line 32
  13. abbrev OAI.MinUncut.Preprocess.OuterDataRaw line 34
  14. def OAI.MinUncut.Preprocess.outerDataEquiv line 35
  15. instance OAI.MinUncut.Preprocess.outerDataPrimcodable line 40
  16. lemma OAI.MinUncut.Preprocess.c_outerData_u line 41
  17. lemma OAI.MinUncut.Preprocess.c_outerData_b4 line 43
  18. lemma OAI.MinUncut.Preprocess.c_outerData_v line 45
  19. lemma OAI.MinUncut.Preprocess.c_outerData_k line 47
  20. lemma OAI.MinUncut.Preprocess.c_outerData_t line 49
  21. abbrev OAI.MinUncut.Preprocess.GridDataRaw line 51
  22. def OAI.MinUncut.Preprocess.gridDataEquiv line 52
  23. instance OAI.MinUncut.Preprocess.gridDataPrimcodable line 57
  24. lemma OAI.MinUncut.Preprocess.c_gridData_T line 58
  25. lemma OAI.MinUncut.Preprocess.c_gridData_L line 60
  26. lemma OAI.MinUncut.Preprocess.c_gridData_r line 62
  27. lemma OAI.MinUncut.Preprocess.c_sigma line 65
  28. lemma OAI.MinUncut.Preprocess.c_eta line 66
  29. lemma OAI.MinUncut.Preprocess.c_R line 67
  30. lemma OAI.MinUncut.Preprocess.c_T line 68