OAI/Combinatorics/Progressions/Estimates/FrozenMarkedLeftOrbitBound.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.frozenMarkedLeftOrbit line 18
  2. def OAI.Erdos3.NilpotentLieFiltration.frozenMarkedRightOrbit line 25
  3. theorem OAI.Erdos3.NilpotentLieFiltration.nativeFrozenMarkedOrbitCoordinates_realValue line 32
  4. theorem OAI.Erdos3.NilpotentLieFiltration.nativeFrozenMarkedOrbitCoordinates_symm_realEval line 37
  5. theorem OAI.Erdos3.NilpotentLieFiltration.frozenMarkedLeftOrbit_realEval line 43
  6. theorem OAI.Erdos3.NilpotentLieFiltration.frozenMarkedRightOrbit_realEval line 53
  7. theorem OAI.Erdos3.NilpotentLieFiltration.frozenMarkedLeftOrbit_realEval_eq_local line 63
  8. theorem OAI.Erdos3.NilpotentLieFiltration.frozenMarkedRightOrbit_realEval_eq_local line 75
  9. theorem OAI.Erdos3.NilpotentLieFiltration.frozenMarkedLeftOrbit_formal_mark line 92
  10. theorem OAI.Erdos3.NilpotentLieFiltration.frozenMarkedRightOrbit_formal_mark line 104
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.observable_frozenMarked_outerOrbits line 129
  12. theorem OAI.Erdos3.NilpotentLieFiltration.exists_frozenMarkedLeftOrbit_exp_bound line 180