OAI/Combinatorics/SumProduct/Alignment/CorrectedBox01.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CorrectedBoxLeibman.Grid line 22
  2. def OAI.CorrectedBoxLeibman.realBasis line 24
  3. lemma OAI.CorrectedBoxLeibman.nat_nodes_injective line 27
  4. lemma OAI.CorrectedBoxLeibman.realBasis_degree line 33
  5. lemma OAI.CorrectedBoxLeibman.interpolate_real line 37
  6. def OAI.CorrectedBoxLeibman.gridEval line 49
  7. def OAI.CorrectedBoxLeibman.LinePolynomial line 53
  8. lemma OAI.CorrectedBoxLeibman.tensor_interpolation line 57
  9. theorem OAI.CorrectedBoxLeibman.exists_grid_expansion line 111
  10. theorem OAI.CorrectedBoxLeibman.character_grid_expansion line 138
  11. def OAI.CorrectedBoxLeibman.lineCoefficient line 161
  12. lemma OAI.CorrectedBoxLeibman.lineCoefficient_eq line 165
  13. lemma OAI.CorrectedBoxLeibman.lineCoefficient_polynomial line 184
  14. lemma OAI.CorrectedBoxLeibman.gridEval_zero line 204
  15. theorem OAI.CorrectedBoxLeibman.dense_line_constant line 221