OAI/Combinatorics/Progressions/Estimates/EuclideanGraphNorm.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.euclidean_graph_gram line 13
  2. theorem OAI.Erdos3.euclidean_section_gram line 30
  3. theorem OAI.Erdos3.gram_linearMap_quadratic line 65
  4. theorem OAI.Erdos3.norm_le_sqrt_gram_det_mul line 77
  5. theorem OAI.Erdos3.euclidean_section_gram_sub_one_posSemidef line 107
  6. theorem OAI.Erdos3.one_le_euclidean_section_gram_sqrt line 122
  7. theorem OAI.Erdos3.euclidean_section_norm_le_gram_sqrt line 131
  8. theorem OAI.Erdos3.euclidean_section_basis_norm_le_gram_sqrt line 140