OAI/NumberTheory/PiExponent/Approximation/MatrixArithmetic.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.InterpolationMatrix.entry_eq_binomial_product line 13
  2. theorem OAI.PiExponent.InterpolationMatrix.entry_eq_zero_of_not_le line 44
  3. theorem OAI.PiExponent.InterpolationMatrix.scalar_product_mul_coeff line 57
  4. theorem OAI.PiExponent.InterpolationMatrix.gaussian_center_cast line 67
  5. theorem OAI.PiExponent.InterpolationMatrix.entry_truncatedLog_cleared_gaussian line 74
  6. def OAI.PiExponent.MatrixArithmetic.logWeights line 132
  7. def OAI.PiExponent.MatrixArithmetic.columnScale line 135
  8. def OAI.PiExponent.MatrixArithmetic.rowScale line 138
  9. def OAI.PiExponent.MatrixArithmetic.denominator line 141
  10. def OAI.PiExponent.MatrixArithmetic.rationalCenters line 144
  11. def OAI.PiExponent.MatrixArithmetic.truncationOrders line 147
  12. theorem OAI.PiExponent.MatrixArithmetic.columnScale_pos line 150
  13. theorem OAI.PiExponent.MatrixArithmetic.rowScale_pos line 154
  14. theorem OAI.PiExponent.MatrixArithmetic.denominator_pos line 158
  15. theorem OAI.PiExponent.MatrixArithmetic.log_columnScale line 165
  16. theorem OAI.PiExponent.MatrixArithmetic.log_rowScale line 173
  17. theorem OAI.PiExponent.MatrixArithmetic.log_denominator_le line 178
  18. def OAI.PiExponent.MatrixArithmetic.rowWeightedSum line 189
  19. def OAI.PiExponent.MatrixArithmetic.meanRowWeight line 194
  20. def OAI.PiExponent.MatrixArithmetic.rowCost line 199
  21. def OAI.PiExponent.MatrixArithmetic.columnCost line 204
  22. def OAI.PiExponent.MatrixArithmetic.selectedMinor line 211
  23. theorem OAI.PiExponent.MatrixArithmetic.actual_row_card_pos line 220
  24. theorem OAI.PiExponent.MatrixArithmetic.ceil_log_weight_pos line 229
  25. theorem OAI.PiExponent.MatrixArithmetic.column_coordinate_le_floor line 234
  26. theorem OAI.PiExponent.MatrixArithmetic.column_log_cost_le_H line 248
  27. theorem OAI.PiExponent.MatrixArithmetic.selected_column_log_cost_le line 266
  28. theorem OAI.PiExponent.MatrixArithmetic.row_weighted_cost_le line 279
  29. theorem OAI.PiExponent.MatrixArithmetic.all_row_log_cost_lower line 289
  30. theorem OAI.PiExponent.MatrixArithmetic.selectedMinor_entries_gaussian line 310
  31. theorem OAI.PiExponent.MatrixArithmetic.selectedMinor_clearing_bound line 337
  32. theorem OAI.PiExponent.MatrixArithmetic.selectedMinor_arithmetic_lower_bound line 360
  33. theorem OAI.PiExponent.MatrixArithmetic.meanRowWeight_nonneg line 395
  34. theorem OAI.PiExponent.MatrixArithmetic.meanRowWeight_le_theta line 403
  35. def OAI.PiExponent.MatrixArithmetic.minimumLogWeight line 418
  36. theorem OAI.PiExponent.MatrixArithmetic.minimumLogWeight_pos line 421
  37. theorem OAI.PiExponent.MatrixArithmetic.minimumLogWeight_le line 425
  38. theorem OAI.PiExponent.MatrixArithmetic.selectedMinor_arithmetic_lower_bound_minimum line 429