OAI/Combinatorics/SumProduct/Alignment/CorrectedBox03.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CorrectedBoxLeibman.choose_short_scale line 26
  2. def OAI.CorrectedBoxLeibman.monomialVector line 87
  3. def OAI.CorrectedBoxLeibman.monomialPolynomial line 90
  4. lemma OAI.CorrectedBoxLeibman.monomialPolynomial_coeff line 93
  5. lemma OAI.CorrectedBoxLeibman.monomialPolynomial_eval line 102
  6. theorem OAI.CorrectedBoxLeibman.dense_monomial_unique line 108
  7. lemma OAI.CorrectedBoxLeibman.linear_form_coordinates line 137
  8. theorem OAI.CorrectedBoxLeibman.dense_monomial_span line 148
  9. lemma OAI.CorrectedBoxLeibman.integer_weights_of_span line 188
  10. lemma OAI.CorrectedBoxLeibman.homogeneous_recovery line 216
  11. lemma OAI.CorrectedBoxLeibman.monomialVector_eq_prod line 252
  12. def OAI.CorrectedBoxLeibman.gridMonomial line 256
  13. theorem OAI.CorrectedBoxLeibman.dense_grid_integer_weights line 261
  14. theorem OAI.CorrectedBoxLeibman.uniform_dense_grid_weights line 305