OAI/Combinatorics/SumProduct/Alignment/CubeRational01.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubeLocalHaar.haar_limit_scaled line 46
  2. theorem OAI.CubeLocalHaar.haar_limit_compact_scaled line 132
  3. theorem OAI.CubeRationalCharts.cube_corner_mem line 197
  4. def OAI.CubeRationalCharts.restrict line 229
  5. lemma OAI.CubeRationalCharts.restrict_mem line 234
  6. lemma OAI.CubeRationalCharts.supported_value_mem line 254
  7. def OAI.CubeRationalCharts.Compatible line 266
  8. lemma OAI.CubeRationalCharts.not_subset_of_lt line 268
  9. def OAI.CubeRationalCharts.residual line 278
  10. def OAI.CubeRationalCharts.coefficients line 284
  11. def OAI.CubeRationalCharts.prefixProduct line 288
  12. def OAI.CubeRationalCharts.assemble line 293
  13. lemma OAI.CubeRationalCharts.residual_prior line 295
  14. lemma OAI.CubeRationalCharts.residual_final line 312
  15. lemma OAI.CubeRationalCharts.prefixProduct_residual line 317
  16. lemma OAI.CubeRationalCharts.assemble_coefficients line 327
  17. lemma OAI.CubeRationalCharts.prefixProduct_eval_after line 332
  18. lemma OAI.CubeRationalCharts.assemble_eval line 348
  19. lemma OAI.CubeRationalCharts.assemble_injective line 353
  20. lemma OAI.CubeRationalCharts.coefficients_assemble line 374
  21. lemma OAI.CubeRationalCharts.coefficients_mem line 378
  22. lemma OAI.CubeRationalCharts.assemble_mem line 402
  23. lemma OAI.CubeRationalCharts.coefficients_lattice line 416
  24. lemma OAI.CubeRationalCharts.residual_continuous line 458
  25. lemma OAI.CubeRationalCharts.coefficients_continuous line 467
  26. lemma OAI.CubeRationalCharts.prefixProduct_continuous line 472
  27. lemma OAI.CubeRationalCharts.assemble_continuous line 482
  28. def OAI.CubeRationalCharts.faceHomeomorph line 488
  29. lemma OAI.CubeRationalCharts.faceHomeomorph_lattice line 511
  30. theorem OAI.CubeRationalCharts.exists_compatible_order line 522
  31. lemma OAI.CubeRationalCharts.residual_map line 542
  32. lemma OAI.CubeRationalCharts.coefficients_map line 554
  33. lemma OAI.CubeRationalCharts.prefixProduct_map line 558
  34. lemma OAI.CubeRationalCharts.assemble_map line 570
  35. lemma OAI.CubeRationalCharts.coefficients_map_product line 574
  36. lemma OAI.CubeRationalCharts.assemble_mul line 587
  37. lemma OAI.CubeRationalCharts.coefficients_mul line 602
  38. lemma OAI.CubeRationalCharts.coefficients_hom_product line 609
  39. def OAI.CubeRationalCharts.lowerPairs line 622
  40. def OAI.CubeRationalCharts.differenceCharacter line 649
  41. theorem OAI.CubeRationalCharts.cube_mul_correction_lower line 661
  42. lemma OAI.CubeRationalCharts.residual_polynomial line 693
  43. lemma OAI.CubeRationalCharts.coefficients_polynomial line 708
  44. lemma OAI.CubeRationalCharts.prefixProduct_polynomial line 713
  45. lemma OAI.CubeRationalCharts.assemble_polynomial line 727
  46. abbrev OAI.CubeRationalCharts.FreeIndex line 734
  47. def OAI.CubeRationalCharts.expand line 742
  48. lemma OAI.CubeRationalCharts.expand_coord line 746
  49. lemma OAI.CubeRationalCharts.expand_polynomial line 752
  50. lemma OAI.CubeRationalCharts.expand_continuous line 761
  51. lemma OAI.CubeRationalCharts.expand_mem line 776
  52. def OAI.CubeRationalCharts.freeHomeomorph line 785
  53. lemma OAI.CubeRationalCharts.freeHomeomorph_apply line 817
  54. lemma OAI.CubeRationalCharts.expand_freeHomeomorph line 820
  55. lemma OAI.CubeRationalCharts.freeHomeomorph_lattice line 831
  56. def OAI.CubeRationalCharts.BaseFirst line 855
  57. theorem OAI.CubeRationalCharts.exists_baseFirst_order line 859
  58. def OAI.CubeRationalCharts.truncate line 880
  59. lemma OAI.CubeRationalCharts.truncate_polynomial line 884
  60. lemma OAI.CubeRationalCharts.expand_truncate_lower line 892
  61. def OAI.CubeRationalCharts.rankedHomeomorph line 912
  62. lemma OAI.CubeRationalCharts.rankedHomeomorph_apply line 915
  63. def OAI.CubeRationalCharts.correctionFunction line 919
  64. lemma OAI.CubeRationalCharts.correctionFunction_polynomial line 926
  65. lemma OAI.CubeRationalCharts.ranked_mul_correction line 949
  66. def OAI.CubeRationalCharts.realCoordinates line 976
  67. lemma OAI.CubeRationalCharts.realCoordinates_lattice line 996
  68. lemma OAI.CubeRationalCharts.cube_mem_iff_coefficients line 1019
  69. lemma OAI.CubeRationalCharts.realCoordinates_max_level line 1029
  70. theorem OAI.CubeRationalCharts.exists_adapted_cube_coordinates line 1049
  71. theorem OAI.CubeRationalCharts.cube_chart_from_base line 1080