OAI/Probability/JammingConcavity/Deletion.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Deletion.

  1. lemma OAI.MicroscopicJamming.separated_unit_card line 41
  2. theorem OAI.MicroscopicJamming.unit_sphere_net line 86
  3. lemma OAI.MicroscopicJamming.opNorm_le_of_quarter_nets line 140
  4. lemma OAI.MicroscopicJamming.subGaussian_abs_tail line 197
  5. lemma OAI.MicroscopicJamming.quarter_net_operator_tail line 217
  6. def OAI.MicroscopicJamming.matrixOperator line 253
  7. lemma OAI.MicroscopicJamming.matrixOperator_apply line 257
  8. lemma OAI.MicroscopicJamming.measurePreserving_uncurry line 261
  9. lemma OAI.MicroscopicJamming.matrix_bilinear_subGaussian line 277
  10. theorem OAI.MicroscopicJamming.mixture_operator_tail line 311