OAI/Combinatorics/Progressions/Geometry/CoordinateSupNorm.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.coordinateL2Norm line 16
  2. theorem OAI.Erdos3.coordinateL2Norm_nonneg line 18
  3. theorem OAI.Erdos3.coordinateL2Norm_le_card_bound line 20
  4. theorem OAI.Erdos3.coordinateL2Norm_matrix_le line 35
  5. theorem OAI.Erdos3.coordinateL2Norm_matrix_entry_bound line 45
  6. theorem OAI.Erdos3.coordinateLinearMap_apply_sum line 84
  7. theorem OAI.Erdos3.coordinateLinearMap_L2_bound line 92
  8. theorem OAI.Erdos3.abs_coordinate_le_coordinateL2Norm line 109
  9. theorem OAI.Erdos3.norm_le_coordinateL2Norm line 119