OAI/Combinatorics/Progressions/Geometry/EmptyLayerChartBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.normalizedOrthogonalChart line 17
  2. theorem OAI.Erdos3.normalizedOrthogonalChart_apply line 20
  3. theorem OAI.Erdos3.normalizedOrthogonalChart_integer_coordinates line 28
  4. theorem OAI.Erdos3.normalizedOrthogonalChart_norm_le line 44
  5. theorem OAI.Erdos3.normalizedOrthogonalChart_symm_norm_le line 54
  6. theorem OAI.Erdos3.normalizedOrthogonalChart_norm_le_zero_of_isEmpty line 72
  7. theorem OAI.Erdos3.normalizedOrthogonalChart_symm_norm_le_zero_of_isEmpty line 79
  8. theorem OAI.Erdos3.hasLayerSamplingRank_of_isEmpty line 86
  9. theorem OAI.Erdos3.VectorPolynomial.degreeLE_of_subsingleton line 93