OAI/Combinatorics/SumProduct/Alignment/CubeTaylor01.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubeHorizontalIrrationality.RationalCharacter line 26
  2. lemma OAI.CubeHorizontalIrrationality.faceLift_continuous line 31
  3. def OAI.CubeHorizontalIrrationality.weight line 44
  4. def OAI.CubeHorizontalIrrationality.scalarPolynomial line 51
  5. lemma OAI.CubeHorizontalIrrationality.maximal_level_le line 57
  6. lemma OAI.CubeHorizontalIrrationality.weight_above line 70
  7. theorem OAI.CubeHorizontalIrrationality.isolated_scalar_coefficient line 85
  8. def OAI.CubeHorizontalIrrationality.scaleCharacter line 110
  9. lemma OAI.CubeHorizontalIrrationality.scaleCharacter_ne line 116
  10. theorem OAI.CubeHorizontalIrrationality.maximal_scaled_character line 129
  11. theorem OAI.CubeHorizontalIrrationality.coefficient_divergence line 178
  12. def OAI.CubeTaylorExpansion.levelPower line 227
  13. lemma OAI.CubeTaylorExpansion.levelPower_zero line 231
  14. lemma OAI.CubeTaylorExpansion.levelPower_one line 236
  15. lemma OAI.CubeTaylorExpansion.levelPower_add line 241
  16. lemma OAI.CubeTaylorExpansion.levelPower_continuous line 247
  17. lemma OAI.CubeTaylorExpansion.character_levelPower line 251
  18. def OAI.CubeTaylorExpansion.faceFactor line 263
  19. lemma OAI.CubeTaylorExpansion.faceFactor_vertex line 269
  20. lemma OAI.CubeTaylorExpansion.faceFactor_character line 279
  21. def OAI.CubeTaylorExpansion.cubeFactor line 292
  22. lemma OAI.CubeTaylorExpansion.cubeFactor_vertex line 297
  23. lemma OAI.CubeTaylorExpansion.character_list_prod line 312
  24. lemma OAI.CubeTaylorExpansion.cubeFactor_character line 319
  25. def OAI.CubeTaylorExpansion.cubePolynomial line 328
  26. def OAI.CubeTaylorExpansion.taylorPolynomial line 332
  27. theorem OAI.CubeTaylorExpansion.cubePolynomial_vertex line 338
  28. lemma OAI.CubeTaylorExpansion.sum_list_range line 352
  29. theorem OAI.CubeTaylorExpansion.scalarPolynomial_eval line 360