OAI/NumberTheory/PiExponent/Approximation/RowTranslation.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.RowTranslation.shift line 13
  2. theorem OAI.PiExponent.RowTranslation.shift_C line 16
  3. theorem OAI.PiExponent.RowTranslation.shift_X line 19
  4. theorem OAI.PiExponent.RowTranslation.shift_add line 22
  5. theorem OAI.PiExponent.RowTranslation.shift_zero line 28
  6. def OAI.PiExponent.RowTranslation.shiftCoefficient line 33
  7. theorem OAI.PiExponent.RowTranslation.coeff_shift line 36
  8. theorem OAI.PiExponent.RowTranslation.coeff_shift_over line 47
  9. theorem OAI.PiExponent.RowTranslation.shift_three line 56
  10. def OAI.PiExponent.RowTranslation.multiIndex line 68
  11. theorem OAI.PiExponent.RowTranslation.multiIndex_apply line 71
  12. theorem OAI.PiExponent.RowTranslation.shifted_X_pow line 75
  13. theorem OAI.PiExponent.RowTranslation.shifted_product_expansion line 84
  14. theorem OAI.PiExponent.RowTranslation.shift_monomial_one line 101
  15. theorem OAI.PiExponent.RowTranslation.shiftCoefficient_eq line 106
  16. theorem OAI.PiExponent.RowTranslation.product_add_expansion line 142
  17. theorem OAI.PiExponent.RowTranslation.row_coefficient_identity line 165
  18. theorem OAI.PiExponent.RowTranslation.coefficient_error_tail line 178
  19. def OAI.PiExponent.RowTranslation.rowScalar line 194
  20. theorem OAI.PiExponent.RowTranslation.rowScalar_ne_zero_le line 201
  21. theorem OAI.PiExponent.RowTranslation.coeff_shiftCoefficient_error_tail line 212
  22. theorem OAI.PiExponent.RowTranslation.exact_row_identity line 225
  23. theorem OAI.PiExponent.RowTranslation.choose_product_le_four_pow line 243
  24. theorem OAI.PiExponent.RowTranslation.multi_choose_product_le_four_pow line 252
  25. theorem OAI.PiExponent.RowTranslation.card_bounded_indices_le line 259
  26. abbrev OAI.PiExponent.RowTranslation.RowChoices line 267
  27. theorem OAI.PiExponent.RowTranslation.card_rowChoices_le line 270
  28. theorem OAI.PiExponent.RowTranslation.card_rowChoices_box_le line 284
  29. theorem OAI.PiExponent.RowTranslation.norm_rowScalar_le line 296
  30. def OAI.PiExponent.RowTranslation.tail line 312
  31. theorem OAI.PiExponent.RowTranslation.coeff_tail_of_lt line 315
  32. theorem OAI.PiExponent.RowTranslation.order_tail line 319
  33. theorem OAI.PiExponent.RowTranslation.order_tail_prod line 324
  34. theorem OAI.PiExponent.RowTranslation.tail_budget_nat line 337
  35. theorem OAI.PiExponent.RowTranslation.tail_weight_budget line 343