OAI/Combinatorics/Progressions/Linear/NormalizedBasisBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.covolume_basis_eq_orthonormal_det line 18
  2. theorem OAI.Erdos3.covolume_basis_scale line 33
  3. theorem OAI.Erdos3.orthonormal_basis_coordinate_abs_le line 44
  4. theorem OAI.Erdos3.covolume_basis_le_norm_bound line 50
  5. theorem OAI.Erdos3.basis_synthesis_norm_le line 71
  6. theorem OAI.Erdos3.basis_coordinates_norm_le_of_covolume line 87
  7. theorem OAI.Erdos3.normalizedAxisBasis_covolume line 137
  8. theorem OAI.Erdos3.normalizedAxisBasis_covolume_lower line 144
  9. theorem OAI.Erdos3.normalizedAxisBasis_covolume_upper line 164
  10. theorem OAI.Erdos3.normalizedAxisBasis_coordinates_bound line 171
  11. theorem OAI.Erdos3.normalizedAxisBasis_synthesis_bound line 184
  12. theorem OAI.Erdos3.normalizedAxisBasis_reciprocal_covolume line 190
  13. theorem OAI.Erdos3.normalizedAxisBasis_covolume_ratio_bounds line 202