OAI/Probability/JammingConcavity/DeletionDeterministicRepairSmallness.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Deletion Deterministic Repair Smallness.

  1. theorem OAI.MicroscopicJamming.exists_orthogonal_solution line 46
  2. def OAI.MicroscopicJamming.rowRestriction line 61
  3. lemma OAI.MicroscopicJamming.rowRestriction_mem_ker line 68
  4. lemma OAI.MicroscopicJamming.card_large_rows_bound line 81
  5. theorem OAI.MicroscopicJamming.exists_slack_correction line 104
  6. theorem OAI.MicroscopicJamming.active_slabs_card_ge line 212
  7. theorem OAI.MicroscopicJamming.slab_direction line 271
  8. theorem OAI.MicroscopicJamming.orthogonal_kernel_slab_direction line 346
  9. theorem OAI.MicroscopicJamming.exists_solution_of_adjoint_lower_bound line 388
  10. theorem OAI.MicroscopicJamming.complete_feasible_to_sphere line 423
  11. theorem OAI.MicroscopicJamming.deterministic_repair_of_small_solves line 477
  12. def OAI.MicroscopicJamming.euclideanRows line 522
  13. lemma OAI.MicroscopicJamming.norm_euclidean_restrict line 527
  14. theorem OAI.MicroscopicJamming.small_row_solves_of_adjoint_lower_bound line 539
  15. theorem OAI.MicroscopicJamming.deterministic_repair_smallness line 556