OAI/LinearAlgebra/MatrixFields/Arithmetic/ArithmeticExponent.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Program.registerCost line 21
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Program.sum_registerCost line 25
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Program.eval_eq_constant_or_input_of_registerCost_eq_zero line 31
  4. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.elementaryLeft line 59
  5. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.elementaryRight line 62
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.elementaryProduct line 65
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.output_injective line 77
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.one_le_output_registerCost line 97
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.output_size_le_cost line 127
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_two_le line 147
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_bddBelow line 177
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularOmega_le_of_admissibleExponent line 181
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.admissibleExponent_iff_rectangular_one line 185
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.admissibleExponent_two_le line 202
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.admissibleExponent_bddBelow line 206
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.omega_le_of_admissibleExponent line 210
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularOmega_one line 214
  18. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Expression.sumFin line 229
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Expression.sumFin_eval line 233
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.Expression.sumFin_cost line 239
  21. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.naiveEntry line 249
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.naiveEntry_eval line 253
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.naiveEntry_cost line 258
  24. def OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.naiveAlgorithm line 262
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.naiveAlgorithm_correct line 268
  26. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.naiveAlgorithm_cost line 276
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.naiveAlgorithm_cost_le line 285
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.admissibleExponent_three line 289
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.admissibleExponent_nonempty line 308
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.AdmissibleExponent.mono line 321
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.omega_two_le line 333
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.omega_nonneg line 336
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.omega_le_three line 338
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.omega_admissibleExponent line 341
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.admissibleExponent_iff_omega_le line 355
  36. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.RectangularAdmissibleExponent.mono line 359
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_of_uniform_costs line 372
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_naive line 385
  39. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_nonempty line 406
  40. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularOmega_two_le line 410
  41. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularOmega_admissibleExponent line 414
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularAdmissibleExponent_iff_omega_le line 429
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularOmega_mono line 433
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.rectangularOmega_zero line 438
  45. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.complexAlpha_set_nonempty line 443
  46. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.complexAlpha_set_bddAbove line 447
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.le_complexAlpha line 451
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.complexAlpha_le_one line 455
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.Arithmetic.complexAlpha_nonneg line 458