OAI/Combinatorics/Progressions/Estimates/DerivativeIndexBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.weighted_row_minor_det line 16
  2. theorem OAI.Erdos3.exists_weighted_minor_lower_bound line 26
  3. theorem OAI.Erdos3.weighted_lattice_covolume_lower line 48
  4. theorem OAI.Erdos3.weighted_isometric_lattice_covolume_lower line 69
  5. theorem OAI.Erdos3.weighted_isometric_lattice_minor_data line 100
  6. theorem OAI.Erdos3.lower_triangular_horizontal_row line 145
  7. theorem OAI.Erdos3.lower_triangular_horizontal_mulVec line 156
  8. theorem OAI.Erdos3.euclideanVerticalMap_horizontal line 166
  9. theorem OAI.Erdos3.euclideanDerivative_vertical_covolume_lower line 189
  10. theorem OAI.Erdos3.euclideanDerivative_vertical_minor_data line 244
  11. theorem OAI.Erdos3.euclideanDerivative_horizontal_basis_data line 293
  12. theorem OAI.Erdos3.euclideanDerivative_horizontal_injective line 343
  13. theorem OAI.Erdos3.euclideanDerivative_covolume_factorization line 398
  14. theorem OAI.Erdos3.scaled_covolume_product_le line 449
  15. theorem OAI.Erdos3.euclideanDerivative_covolume_product_bound line 459
  16. theorem OAI.Erdos3.euclideanDerivative_index_graph_bounds line 501