OAI/Combinatorics/Progressions/Geometry/NativeCoordinateEstimates.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.refiltrationCoordinateBudget line 11
  2. theorem OAI.Erdos3.refiltrationCoordinateBudget_nonneg line 14
  3. theorem OAI.Erdos3.NilpotentLieFiltration.exists_refiltration_bases_in_coordinates line 23
  4. def OAI.Erdos3.horizontalCoordinateBudget line 72
  5. theorem OAI.Erdos3.horizontalCoordinateBudget_nonneg line 75
  6. theorem OAI.Erdos3.horizontalCoordinateHeight_bound line 81
  7. def OAI.Erdos3.nativeCoordinateBaseBudget line 108
  8. def OAI.Erdos3.nativeCoordinateInputBudget line 112
  9. def OAI.Erdos3.nativeDependentBudget line 115
  10. def OAI.Erdos3.nativeCoordinateSeparationBudget line 119
  11. def OAI.Erdos3.nativeDependentDenominatorBudget line 122
  12. def OAI.Erdos3.nativeDependentSlowBudget line 126
  13. theorem OAI.Erdos3.nativeCoordinateBaseBudget_bounds line 130
  14. theorem OAI.Erdos3.nativeCoordinateInputBudget_bounds line 150
  15. theorem OAI.Erdos3.nativeCoordinateInputBudget_nonneg line 162
  16. theorem OAI.Erdos3.nativeDependentBudget_nonneg line 166
  17. theorem OAI.Erdos3.nativeCoordinateSeparationBudget_cutoffs line 171
  18. theorem OAI.Erdos3.nativeDependentSlowBudget_bound line 181
  19. theorem OAI.Erdos3.nativeCoordinate_denominator_bound line 207
  20. theorem OAI.Erdos3.nativeCoordinate_slow_bound line 229