OAI/Probability/SKRatio/Matrices/PlantedSquares.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Planted.affineDisorder line 16
  2. lemma OAI.SKRatio.Planted.affineDisorder_hasLaw line 19
  3. lemma OAI.SKRatio.Planted.coupling_scaled_norm line 33
  4. lemma OAI.SKRatio.Planted.normalized_absolute_row_le line 41
  5. lemma OAI.SKRatio.Planted.normalized_matrix_norm_le_row_square line 53
  6. lemma OAI.SKRatio.Planted.gaussian_rows_square_bounded line 65
  7. lemma OAI.SKRatio.Planted.affine_square_decomposition line 98
  8. lemma OAI.SKRatio.Planted.affine_square_norm_le line 110
  9. lemma OAI.SKRatio.Planted.affine_square_matrix_rare line 128
  10. theorem OAI.SKRatio.Planted.square_matrix_rare line 157