OAI/Computability/RationalHitting/DenseDeterminant.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalHitting.StackLanguage.list_code_length_nil line 8
  2. lemma OAI.RationalHitting.StackLanguage.list_code_cons line 9
  3. lemma OAI.RationalHitting.StackLanguage.code_le_of_mem line 14
  4. lemma OAI.RationalHitting.StackLanguage.list_code_length_le line 25
  5. lemma OAI.RationalHitting.StackLanguage.drop_headD_getElem line 35
  6. lemma OAI.RationalHitting.StackLanguage.finRows_access line 41
  7. lemma OAI.RationalHitting.StackLanguage.finRange_map_val line 46
  8. lemma OAI.RationalHitting.StackLanguage.range_map_to_finRange line 49
  9. structure OAI.RationalHitting.StackLanguage.DenseSquare line 54
  10. def OAI.RationalHitting.StackLanguage.DenseSquare.rows line 58
  11. instance OAI.RationalHitting.StackLanguage.(instance at line 61) line 61
  12. instance OAI.RationalHitting.StackLanguage.(instance at line 63) line 63
  13. def OAI.RationalHitting.StackLanguage.DenseSquare.get line 65
  14. lemma OAI.RationalHitting.StackLanguage.DenseSquare.get_fin line 68
  15. lemma OAI.RationalHitting.StackLanguage.DenseSquare.rows_get line 71
  16. lemma OAI.RationalHitting.StackLanguage.DenseSquare.dim_le_code line 90
  17. lemma OAI.RationalHitting.StackLanguage.DenseSquare.entry_bits_le_code line 94
  18. lemma OAI.RationalHitting.StackLanguage.DenseSquare.get_bits_le_code line 105
  19. lemma OAI.RationalHitting.StackLanguage.DenseSquare.code_length_le line 112
  20. theorem OAI.RationalHitting.StackLanguage.Poly.denseDim line 129
  21. theorem OAI.RationalHitting.StackLanguage.Poly.denseRows line 132
  22. theorem OAI.RationalHitting.StackLanguage.Poly.denseGet line 136
  23. theorem OAI.RationalHitting.StackLanguage.Poly.denseBuild line 153
  24. theorem OAI.RationalHitting.StackLanguage.Poly.sumRange line 171
  25. def OAI.RationalHitting.StackLanguage.DenseSquare.of line 183
  26. def OAI.RationalHitting.StackLanguage.DenseSquare.step line 185
  27. lemma OAI.RationalHitting.StackLanguage.DenseSquare.step_dim line 188
  28. lemma OAI.RationalHitting.StackLanguage.DenseSquare.step_of line 189
  29. lemma OAI.RationalHitting.StackLanguage.sum_diag_range line 193
  30. lemma OAI.RationalHitting.StackLanguage.sum_product_range line 199
  31. theorem OAI.RationalHitting.StackLanguage.Poly.denseStep line 207
  32. lemma OAI.RationalHitting.StackLanguage.abs_le_pow_of_bits_le line 245
  33. lemma OAI.RationalHitting.StackLanguage.bits_le_of_abs_le_pow line 252
  34. lemma OAI.RationalHitting.StackLanguage.DenseSquare.get_abs_le line 259
  35. lemma OAI.RationalHitting.StackLanguage.DenseSquare.step_get_bound line 263
  36. lemma OAI.RationalHitting.StackLanguage.DenseSquare.iterate_get_bound line 279
  37. lemma OAI.RationalHitting.StackLanguage.DenseSquare.iterate_dim line 297
  38. lemma OAI.RationalHitting.StackLanguage.DenseSquare.iterate_code_bound line 300
  39. def OAI.RationalHitting.StackLanguage.birdState line 315
  40. lemma OAI.RationalHitting.StackLanguage.birdState_iterate line 317
  41. lemma OAI.RationalHitting.StackLanguage.birdState_iterate_size line 323
  42. theorem OAI.RationalHitting.StackLanguage.Poly.birdState_poly line 350
  43. theorem OAI.RationalHitting.StackLanguage.Poly.birdStages line 353
  44. def OAI.RationalHitting.StackLanguage.DenseSquare.detAlgorithm line 365
  45. lemma OAI.RationalHitting.StackLanguage.DenseSquare.iterate_of line 368
  46. lemma OAI.RationalHitting.StackLanguage.DenseSquare.detAlgorithm_eq line 375
  47. theorem OAI.RationalHitting.StackLanguage.Poly.denseDet line 390