OAI/Combinatorics/Progressions/Polynomial/NormalizedMarkedPhase.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.markedShiftPhase line 12
  2. theorem OAI.Erdos3.markedShiftPhase_apply line 19
  3. def OAI.Erdos3.markedQuotientPhase line 22
  4. theorem OAI.Erdos3.markedQuotientPhase_map line 27
  5. theorem OAI.Erdos3.markedQuotientPhase_direction line 31
  6. def OAI.Erdos3.markedQuotientPolynomialAlgebra line 34
  7. theorem OAI.Erdos3.mem_markedQuotientPolynomialAlgebra line 38
  8. theorem OAI.Erdos3.exists_zero_phase_lift line 42
  9. theorem OAI.Erdos3.markedPhase_lattice_map line 67
  10. def OAI.Erdos3.markedPhaseProjection line 75
  11. def OAI.Erdos3.markedPhaseRealCoordinates line 80
  12. theorem OAI.Erdos3.markedPhaseProjection_mk line 85
  13. def OAI.Erdos3.markedPhaseLocalLift line 89
  14. theorem OAI.Erdos3.markedPhaseLocalLift_mk line 92
  15. theorem OAI.Erdos3.markedPhaseRealCoordinates_eq_of_small line 100
  16. theorem OAI.Erdos3.markedPhaseProjection_lipschitz line 114
  17. theorem OAI.Erdos3.markedPhaseLocalLift_lipschitzOn line 135
  18. theorem OAI.Erdos3.rationalLogHeight_nat_inv_mul_exp_bound line 160
  19. def OAI.Erdos3.normalizedMarkedPhase line 178
  20. theorem OAI.Erdos3.normalizedMarkedPhase_apply line 185
  21. theorem OAI.Erdos3.normalizedMarkedPhase_scaled_direction line 189
  22. theorem OAI.Erdos3.normalizedMarkedPhase_height line 197