OAI/Combinatorics/Progressions/Nilpotent/NiltestBasepointNormalization.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.basis_reindex_equivFun_symm line 19
  2. theorem OAI.Erdos3.bchSubgroupCoordinates_reindex line 28
  3. theorem OAI.Erdos3.bchSubgroup_inner_grid_reindex line 35
  4. theorem OAI.Erdos3.bchSubgroup_outer_grid_reindex line 43
  5. theorem OAI.Erdos3.basis_reindex_span_weights line 53
  6. theorem OAI.Erdos3.lieStructureConstants_reindex line 68
  7. theorem OAI.Erdos3.NilpotentLieBCHGroup.contMDiff_of_quotient_pullback line 95
  8. theorem OAI.Erdos3.NilpotentLieBCHGroup.contMDiff_quotient_iff line 127
  9. theorem OAI.Erdos3.NilpotentLieBCHGroup.contMDiff_quotient_left_smul line 143
  10. def OAI.Erdos3.realificationQuotientChartedSpace line 177
  11. theorem OAI.Erdos3.isManifold_realification_quotient line 184
  12. theorem OAI.Erdos3.contMDiff_realification_quotient_mk line 192
  13. theorem OAI.Erdos3.contMDiff_realification_quotient_iff line 203
  14. theorem OAI.Erdos3.realification_quotient_chart_mem_maximalAtlas line 217
  15. theorem OAI.Erdos3.NilpotentLieBCHGroup.contMDiff_realificationMap_quotient line 248
  16. theorem OAI.Erdos3.realification_filtered_nilmanifold line 280
  17. structure OAI.Erdos3.RationalFilteredNilmanifold line 341
  18. def OAI.Erdos3.rationalLogHeight line 352
  19. abbrev OAI.Erdos3.RationalFilteredNilmanifold.RealGroup line 359
  20. def OAI.Erdos3.RationalFilteredNilmanifold.realLattice line 361
  21. abbrev OAI.Erdos3.RationalFilteredNilmanifold.Space line 364
  22. def OAI.Erdos3.RationalFilteredNilmanifold.GeometryComplexityLE line 366
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.GeometryComplexityLE.mono line 371
  24. def OAI.Erdos3.RationalFilteredNilmanifold.metricSpace line 381
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.space_compact line 384
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.realLattice_closed_discrete line 387
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.layer_lattice_cocompact line 393
  28. def OAI.Erdos3.RationalFilteredNilmanifold.dropTop line 411
  29. theorem OAI.Erdos3.RationalFilteredNilmanifold.dropTop_geometry line 426
  30. theorem OAI.Erdos3.RationalFilteredNilmanifold.dropTop_lattice_back line 430
  31. structure OAI.Erdos3.RationalFilteredNilmanifold.Niltest line 454
  32. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.const line 466
  33. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval line 477
  34. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval_const line 480
  35. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.norm_eval_le line 483
  36. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.evalCyclic line 486
  37. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.evalCyclic_natCast line 489
  38. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.norm_evalCyclic_le line 494
  39. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.ComplexityLE line 497
  40. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.ComplexityLE.mono line 500
  41. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.observable_budget line 504
  42. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval_budget line 509
  43. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval_step_zero line 516
  44. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval_dimension_zero line 522
  45. def OAI.Erdos3.RationalFilteredNilmanifold.raisedLayerBasis line 546
  46. theorem OAI.Erdos3.RationalFilteredNilmanifold.raisedLayerBasis_of_lt line 553
  47. def OAI.Erdos3.RationalFilteredNilmanifold.raiseStep line 558
  48. theorem OAI.Erdos3.RationalFilteredNilmanifold.raiseStep_geometry line 573
  49. theorem OAI.Erdos3.RationalFilteredNilmanifold.raiseStep_lattice_back line 591
  50. def OAI.Erdos3.NilpotentLieFiltration.piLayerEquiv line 615
  51. def OAI.Erdos3.RationalFilteredNilmanifold.productFinBasis line 632
  52. def OAI.Erdos3.RationalFilteredNilmanifold.productLayerBasis line 635
  53. def OAI.Erdos3.RationalFilteredNilmanifold.productLayerFinBasis line 641
  54. theorem OAI.Erdos3.RationalFilteredNilmanifold.product_inner_grid line 646
  55. theorem OAI.Erdos3.RationalFilteredNilmanifold.product_outer_grid line 655
  56. def OAI.Erdos3.RationalFilteredNilmanifold.pi line 665
  57. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.normalizeBasepoint line 691
  58. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.normalizeBasepoint_normBound line 702
  59. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.normalizeBasepoint_zero line 706
  60. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.normalizeBasepoint_eval line 712
  61. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.normalizeBasepoint_evalCyclic line 723
  62. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.normalizeBasepoint_complexity line 729