OAI/Probability/JammingConcavity/DeletionUniformRowEstimates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Deletion Uniform Row Estimates.

  1. lemma OAI.MicroscopicJamming.net_power_cancel line 40
  2. lemma OAI.MicroscopicJamming.row_net_geometric_bound line 49
  3. lemma OAI.MicroscopicJamming.gap_net_geometric_bound line 77
  4. lemma OAI.MicroscopicJamming.geometry_indices line 100
  5. lemma OAI.MicroscopicJamming.lower_bound_of_unit line 148
  6. def OAI.MicroscopicJamming.RowGeometry line 163
  7. lemma OAI.MicroscopicJamming.small_power_choice line 172
  8. lemma OAI.MicroscopicJamming.exp_neg_one_pow line 183
  9. lemma OAI.MicroscopicJamming.mixture_operator_geometric line 189
  10. lemma OAI.MicroscopicJamming.uniform_row_geometric line 231
  11. lemma OAI.MicroscopicJamming.uniform_gap_geometric line 309
  12. theorem OAI.MicroscopicJamming.uniform_row_estimates line 368