OAI/Combinatorics/Progressions/Linear/BinaryLowerRankFamily.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.NativeUnitRankFamily line 12
  2. def OAI.Erdos3.NativeUnitRankFamily.eval line 41
  3. theorem OAI.Erdos3.NativeUnitRankFamily.unit_eval line 45
  4. theorem OAI.Erdos3.NativeUnitRankFamily.norm_eval line 48
  5. def OAI.Erdos3.NativeUnitRankFamily.mono line 54
  6. theorem OAI.Erdos3.NativeUnitRankFamily.mono_eval line 59
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.rank_invariant_of_frequency_zero line 80
  8. def OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.coordinateNiltest line 109
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.coordinateNiltest_complexity line 118
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.exists_lower_rank_family line 133
  11. def OAI.Erdos3.RationalFilteredNilmanifold.HasLowerRankUnitFamily line 221
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.uniform_lower_rank_family line 253
  13. def OAI.Erdos3.RationalFilteredNilmanifold.HasUniformLowerRankUnitFamily line 315
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.HasUniformLowerRankUnitFamily.atOrbit line 335
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.hasUniformLowerRankUnitFamily line 354
  16. def OAI.Erdos3.RationalFilteredNilmanifold.HasLowerRankOrbitFamily line 389
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.HasUniformLowerRankUnitFamily.realizeFamily line 406
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.HasLowerRankOrbitFamily.mono line 441
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_lower_rank_product_family line 456
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_binary_lower_rank_unit_family line 521