OAI/Combinatorics/Progressions/Estimates/SourceUnitCover.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RationalTorus.trivialMultidegreeFiltration line 17
  2. def OAI.Erdos3.RationalTorus.trivialMultidegreeStructure line 33
  3. theorem OAI.Erdos3.RationalTorus.trivialMultidegreeStructure_complexity line 42
  4. structure OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable line 62
  5. def OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.mono line 82
  6. def OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.constOne line 88
  7. theorem OAI.Erdos3.frozen_quotient_map_smul line 116
  8. def OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.withLattice line 140
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.withLattice_complexity line 149
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.top_realSubgroup_commute line 158
  11. def OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.frozenCover line 171
  12. def OAI.Erdos3.invariantVerticalBudget line 216
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.exists_invariant line 228
  14. theorem OAI.Erdos3.exists_invariantVertical_cost line 291
  15. structure OAI.Erdos3.NativeMultidegreeNilcharacter line 311
  16. def OAI.Erdos3.NativeMultidegreeNilcharacter.eval line 338
  17. def OAI.Erdos3.NativeMultidegreeNilcharacter.evalCyclic line 342
  18. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.unit_eval line 345
  19. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.norm_eval line 347
  20. def OAI.Erdos3.NativeMultidegreeNilcharacter.mono line 349
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mono_eval line 355
  22. def OAI.Erdos3.NativeMultidegreeNilcharacter.constOne line 358
  23. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.constOne_eval line 371
  24. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.constOne_evalCyclic line 374
  25. def OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.pullback line 410
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.pullback_frequency line 436
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.pullback_observable_mk line 439
  28. def OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.onSublattice line 465
  29. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.onSublattice_frequency line 482
  30. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.onSublattice_lipBound line 485
  31. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.onSublattice_observable_mk line 488
  32. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.onSublattice_orbit_eval line 492
  33. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_source_unit_cover line 509