OAI/NumberTheory/PiExponent/Approximation/InterpolationMatrix.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.InterpolationMatrix.exponentVector line 9
  2. theorem OAI.PiExponent.InterpolationMatrix.exponentVector_apply line 12
  3. def OAI.PiExponent.InterpolationMatrix.truncatedLog line 16
  4. theorem OAI.PiExponent.InterpolationMatrix.truncatedLog_coeff line 19
  5. def OAI.PiExponent.InterpolationMatrix.monomialImage line 26
  6. def OAI.PiExponent.InterpolationMatrix.entry line 33
  7. def OAI.PiExponent.InterpolationMatrix.sectionImage line 38
  8. theorem OAI.PiExponent.InterpolationMatrix.sectionImage_coeff line 44
  9. def OAI.PiExponent.InterpolationMatrix.columnWeights line 57
  10. def OAI.PiExponent.InterpolationMatrix.rowWeights line 60
  11. abbrev OAI.PiExponent.InterpolationMatrix.Column line 63
  12. abbrev OAI.PiExponent.InterpolationMatrix.Row line 66
  13. theorem OAI.PiExponent.InterpolationMatrix.column_mem_iff line 69
  14. theorem OAI.PiExponent.InterpolationMatrix.row_mem_iff line 79
  15. theorem OAI.PiExponent.InterpolationMatrix.column_weight_le line 90
  16. theorem OAI.PiExponent.InterpolationMatrix.row_weight_lt line 95
  17. def OAI.PiExponent.InterpolationMatrix.matrix line 100
  18. def OAI.PiExponent.InterpolationMatrix.linearEvaluation line 106
  19. theorem OAI.PiExponent.InterpolationMatrix.linearEvaluation_apply line 111
  20. theorem OAI.PiExponent.InterpolationMatrix.linearEvaluation_eq_coeff line 118
  21. theorem OAI.PiExponent.InterpolationMatrix.row_card line 127
  22. theorem OAI.PiExponent.InterpolationMatrix.exists_full_row_minor_of_surjective line 134
  23. theorem OAI.PiExponent.InterpolationMatrix.interpolation_full_row_minor line 167
  24. def OAI.PiExponent.InterpolationMatrix.truncatedLogMatrix line 176
  25. theorem OAI.PiExponent.InterpolationMatrix.truncatedLog_full_row_minor line 181