OAI/Combinatorics/Progressions/Estimates/MarkedUnitOrbit.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NativeRankRelation.CommonData.localAffineMarkedBase line 26
  2. def OAI.Erdos3.NativeRankRelation.CommonData.localAffineMarkedOrbit line 32
  3. def OAI.Erdos3.NativeRankRelation.CommonData.localAffineMarkedLift line 36
  4. theorem OAI.Erdos3.NativeRankRelation.CommonData.localAffineMarkedOrbit_eval line 41
  5. theorem OAI.Erdos3.NativeRankRelation.CommonData.localAffineMarkedOrbit_at_zero line 49
  6. theorem OAI.Erdos3.NativeRankRelation.CommonData.localAffineMarkedLift_eval line 54
  7. theorem OAI.Erdos3.NativeRankRelation.CommonData.localAffineMarkedLift_eq_polynomial_eval line 75
  8. def OAI.Erdos3.NativeRankRelation.CommonData.localAffineConjugatedLift line 108
  9. def OAI.Erdos3.NativeRankRelation.CommonData.localAffineCorrectingElement line 116
  10. theorem OAI.Erdos3.NativeRankRelation.CommonData.localAffineConjugatedLift_eval line 121
  11. theorem OAI.Erdos3.NativeRankRelation.CommonData.localAffineMarkedOrbit_conjugation line 134
  12. theorem OAI.Erdos3.NativeRankRelation.CommonData.localAffineConjugatedLift_eq_polynomial_eval line 152
  13. def OAI.Erdos3.NativeRankRelation.CommonData.scaledLocalAffineMarkedOrbit line 184
  14. def OAI.Erdos3.NativeRankRelation.CommonData.scaledLocalAffineMarkedLift line 189
  15. theorem OAI.Erdos3.NativeRankRelation.CommonData.scaledLocalAffineMarkedOrbit_eval line 195
  16. theorem OAI.Erdos3.NativeRankRelation.CommonData.scaledLocalAffineMarkedOrbit_at_zero line 204
  17. theorem OAI.Erdos3.NativeRankRelation.CommonData.scaledLocalAffineMarkedLift_eval line 210
  18. def OAI.Erdos3.NativeRankRelation.CommonData.scaledLocalAffineConjugatedLift line 264
  19. def OAI.Erdos3.NativeRankRelation.CommonData.scaledLocalAffineCorrectingElement line 272
  20. theorem OAI.Erdos3.NativeRankRelation.CommonData.scaledLocalAffineConjugatedLift_eval line 277
  21. theorem OAI.Erdos3.NativeRankRelation.CommonData.scaledLocalAffineMarkedOrbit_conjugation line 290
  22. theorem OAI.Erdos3.NativeRankRelation.CommonData.scaledLocalAffineConjugatedLift_eq_polynomial_eval line 308
  23. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_scaled_marked_nilcharacter line 352