OAI/Combinatorics/Progressions/Geometry/ScalarSpatialScaleBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.integerColumnEquiv_range line 9
  2. theorem OAI.Erdos3.selectedSpatial_full_image line 22
  3. theorem OAI.Erdos3.selectedSpatial_extended_period line 29
  4. theorem OAI.Erdos3.selectedSpatial_extended_index line 39
  5. theorem OAI.Erdos3.goodScalarKernelTuple_spatial_det_ne_zero line 49
  6. theorem OAI.Erdos3.scalarSpatialPivot_normalized line 60
  7. theorem OAI.Erdos3.scalarSpatialPivot_coeff_bound line 69
  8. theorem OAI.Erdos3.scalarSpatialPivot_inverse_bound line 84
  9. theorem OAI.Erdos3.scalarSpatialFree_scaled_bound line 117
  10. theorem OAI.Erdos3.scalarSpatial_free_norm_bound line 134
  11. theorem OAI.Erdos3.scalarSpatialPivot_det_bound line 161
  12. theorem OAI.Erdos3.spatialPivotScale_lower line 174