OAI/Probability/BinarySweep/MatrixBounds/SparsePinching.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.Density.blockVec line 15
  2. def OAI.BinaryCoordinateSweeps.Density.pinch line 18
  3. lemma OAI.BinaryCoordinateSweeps.Density.sum_blockVec line 22
  4. lemma OAI.BinaryCoordinateSweeps.Density.pinch_hermitian line 27
  5. lemma OAI.BinaryCoordinateSweeps.Density.pinch_form line 36
  6. lemma OAI.BinaryCoordinateSweeps.Density.pinch_posSemidef line 53
  7. lemma OAI.BinaryCoordinateSweeps.Density.form_cross_le line 59
  8. lemma OAI.BinaryCoordinateSweeps.Density.block_form_zero line 67
  9. theorem OAI.BinaryCoordinateSweeps.Density.sparse_pinching line 82
  10. def OAI.BinaryCoordinateSweeps.Density.subsetCode line 163
  11. lemma OAI.BinaryCoordinateSweeps.Density.subsetCode_range line 167
  12. lemma OAI.BinaryCoordinateSweeps.Density.card_small_subsets_le line 184
  13. def OAI.BinaryCoordinateSweeps.Density.hamming line 197
  14. lemma OAI.BinaryCoordinateSweeps.Density.hamming_symm line 200
  15. lemma OAI.BinaryCoordinateSweeps.Density.hamming_degree line 206