OAI/Combinatorics/SumProduct/Alignment/CubeTaylor02.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubeTaylorExpansion.faceBinomial_totalDegree line 32
  2. def OAI.CubeTaylorExpansion.facePower line 39
  3. lemma OAI.CubeTaylorExpansion.facePower_mem line 46
  4. theorem OAI.CubeTaylorExpansion.faceFactor_polynomial line 55
  5. lemma OAI.CubeTaylorExpansion.polynomial_list_prod line 69
  6. lemma OAI.CubeTaylorExpansion.cubeFactor_polynomial line 81
  7. theorem OAI.CubeTaylorExpansion.cubePolynomial_adapted line 90
  8. lemma OAI.CorrectedBoxLeibman.exponent_le_sum line 110
  9. def OAI.CorrectedBoxLeibman.exponentGrid line 116
  10. lemma OAI.CorrectedBoxLeibman.gridExponent_exponentGrid line 119
  11. lemma OAI.CorrectedBoxLeibman.exponentGrid_degree line 122
  12. def OAI.CorrectedBoxLeibman.polynomialGrid line 128
  13. lemma OAI.CorrectedBoxLeibman.polynomial_eq_grid line 131
  14. lemma OAI.CorrectedBoxLeibman.gridEval_polynomial line 164
  15. lemma OAI.CubeHorizontalIrrationality.scalarPolynomial_totalDegree line 190
  16. lemma OAI.CubeHorizontalIrrationality.renamed_degree line 202
  17. theorem OAI.CubeHorizontalIrrationality.grid_irrationality line 209
  18. lemma OAI.CubeLocalHaar.iterDiff_comp line 262
  19. lemma OAI.CubeLocalHaar.polynomial_comp line 274
  20. def OAI.CubeLocalHaar.cubeLattice line 283
  21. theorem OAI.CubeLocalHaar.haar_limit line 313