OAI/Combinatorics/Progressions/Linear/RankIntervalFactorization.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.rankIntervalInputBudget line 12
  2. theorem OAI.Erdos3.rankIntervalInputBudget_bounds line 15
  3. theorem OAI.Erdos3.exists_rank_interval_product_budget line 28
  4. def OAI.Erdos3.RationalFilteredNilmanifold.productRankLayerBasis line 54
  5. def OAI.Erdos3.RationalFilteredNilmanifold.productRankLayerFinBasis line 60
  6. def OAI.Erdos3.RationalFilteredNilmanifold.piRank line 67
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.productRankLayerBasis_logHeight line 74
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.piRank_complexity line 94
  9. theorem OAI.Erdos3.NilpotentLieFiltration.orbitEquivOfEq_log line 117
  10. theorem OAI.Erdos3.NilpotentLieFiltration.orbitEquivOfEq_translate line 122
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.orbitEquiv_log line 135
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.orbitEquiv_translate line 139
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.productProjectionHom_mem_rank line 159
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.productObservable_rank_vertical line 171
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.piNiltest_rank_vertical line 201
  16. def OAI.Erdos3.NativeDegreeRankFamily.fourPointFactors line 232
  17. def OAI.Erdos3.NativeDegreeRankFamily.fourPointFrequencies line 239
  18. theorem OAI.Erdos3.NativeDegreeRankFamily.fourPointFactors_complexity line 242
  19. theorem OAI.Erdos3.NativeDegreeRankFamily.fourPointFactors_eval line 251
  20. theorem OAI.Erdos3.NativeDegreeRankFamily.fourPointFactors_vertical line 258
  21. def OAI.Erdos3.NativeDegreeRankFamily.fourPointNiltest line 282
  22. theorem OAI.Erdos3.NativeDegreeRankFamily.fourPointNiltest_complexity line 288
  23. theorem OAI.Erdos3.NativeDegreeRankFamily.fourPointNiltest_eval line 294
  24. theorem OAI.Erdos3.NativeDegreeRankFamily.fourPointNiltest_vertical line 302
  25. def OAI.Erdos3.NativeDegreeRankFamily.horizontalCoefficient line 334
  26. theorem OAI.Erdos3.NativeDegreeRankFamily.fourPointFactors_orbit line 339
  27. theorem OAI.Erdos3.NativeDegreeRankFamily.fourPoint_horizontalCoefficient line 345
  28. def OAI.Erdos3.rankQuadrupleParameters line 384
  29. def OAI.Erdos3.NativeRankInterval.productModels line 401
  30. def OAI.Erdos3.NativeRankInterval.productRanks line 406
  31. def OAI.Erdos3.NativeRankInterval.productTests line 412
  32. def OAI.Erdos3.NativeRankInterval.productFrequencies line 417
  33. theorem OAI.Erdos3.NativeRankInterval.productTests_eval line 422
  34. theorem OAI.Erdos3.NativeRankInterval.productTests_vertical line 434
  35. def OAI.Erdos3.rankCoordinateTuple line 458
  36. theorem OAI.Erdos3.rankCoordinateTuple_first12 line 462
  37. theorem OAI.Erdos3.rankCoordinateTuple_first13 line 466
  38. theorem OAI.Erdos3.rankCoordinateTuple_fixed12 line 471
  39. theorem OAI.Erdos3.rankCoordinateTuple_fixed13 line 479
  40. theorem OAI.Erdos3.card_selected_four_le line 487
  41. theorem OAI.Erdos3.exists_rank_interval_product line 513
  42. def OAI.Erdos3.NativeRankInterval.productOrbit line 624
  43. def OAI.Erdos3.NativeRankInterval.productSymbol line 629
  44. theorem OAI.Erdos3.NativeRankInterval.productSymbol_eq line 647
  45. def OAI.Erdos3.NativeRankInterval.rankProjection line 684
  46. theorem OAI.Erdos3.NativeRankInterval.rankProjection_frequency line 691
  47. theorem OAI.Erdos3.NativeRankInterval.rankProjection_mem_layer line 705
  48. theorem OAI.Erdos3.NativeRankInterval.rankProjection_mem_refiltered line 716
  49. theorem OAI.Erdos3.exists_rank_interval_factorization line 742