OAI/Probability/JammingConcavity/DeletionMeasurePreservingSelectRows.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Deletion Measure Preserving Select Rows.

  1. abbrev OAI.MicroscopicJamming.SpinSpace line 40
  2. def OAI.MicroscopicJamming.rowCount line 42
  3. abbrev OAI.MicroscopicJamming.PatternMatrix line 44
  4. def OAI.MicroscopicJamming.disorderLaw line 48
  5. def OAI.MicroscopicJamming.surfaceLaw line 52
  6. def OAI.MicroscopicJamming.field line 57
  7. def OAI.MicroscopicJamming.gap line 61
  8. def OAI.MicroscopicJamming.potential line 65
  9. def OAI.MicroscopicJamming.energy line 67
  10. def OAI.MicroscopicJamming.satisfiable line 70
  11. def OAI.MicroscopicJamming.satProbability line 73
  12. def OAI.MicroscopicJamming.groundEnergy line 77
  13. def OAI.MicroscopicJamming.unitEnergy line 81
  14. def OAI.MicroscopicJamming.unitGround line 85
  15. def OAI.MicroscopicJamming.unitSatisfiable line 88
  16. lemma OAI.MicroscopicJamming.potential_nonneg line 91
  17. lemma OAI.MicroscopicJamming.potential_eq_zero_iff line 95
  18. lemma OAI.MicroscopicJamming.unitEnergy_nonneg line 100
  19. lemma OAI.MicroscopicJamming.unitEnergy_zero_iff line 104
  20. lemma OAI.MicroscopicJamming.continuous_unitEnergy line 110
  21. lemma OAI.MicroscopicJamming.continuous_unitGround line 116
  22. lemma OAI.MicroscopicJamming.unitGround_attained line 119
  23. lemma OAI.MicroscopicJamming.unitGround_nonneg line 129
  24. lemma OAI.MicroscopicJamming.unitGround_le line 135
  25. lemma OAI.MicroscopicJamming.unitSatisfiable_iff_ground line 141
  26. lemma OAI.MicroscopicJamming.measurableSet_unitSatisfiable line 151
  27. lemma OAI.MicroscopicJamming.field_rescale line 156
  28. lemma OAI.MicroscopicJamming.energy_rescale line 162
  29. lemma OAI.MicroscopicJamming.norm_rescale_sq line 166
  30. lemma OAI.MicroscopicJamming.exists_rescale_unit line 171
  31. lemma OAI.MicroscopicJamming.groundEnergy_eq_unitGround line 180
  32. lemma OAI.MicroscopicJamming.satisfiable_iff_unit line 192
  33. lemma OAI.MicroscopicJamming.coordinateLaw_memLp_two line 204
  34. lemma OAI.MicroscopicJamming.matrix_field_memLp_two line 209
  35. lemma OAI.MicroscopicJamming.potential_le_quadratic line 220
  36. lemma OAI.MicroscopicJamming.integrable_unitEnergy line 228
  37. lemma OAI.MicroscopicJamming.integrable_unitGround line 241
  38. lemma OAI.MicroscopicJamming.integrable_groundEnergy line 251
  39. def OAI.MicroscopicJamming.finiteAverage line 267
  40. lemma OAI.MicroscopicJamming.finiteAverage_add line 270
  41. lemma OAI.MicroscopicJamming.finiteAverage_sub line 274
  42. lemma OAI.MicroscopicJamming.finiteAverage_mul_const line 278
  43. lemma OAI.MicroscopicJamming.finiteAverage_const line 284
  44. lemma OAI.MicroscopicJamming.finiteAverage_sum line 288
  45. lemma OAI.MicroscopicJamming.finiteAverage_congr line 293
  46. lemma OAI.MicroscopicJamming.finiteAverage_mono line 299
  47. lemma OAI.MicroscopicJamming.finiteAverage_centered_product line 303
  48. lemma OAI.MicroscopicJamming.finiteAverage_indicator line 313
  49. lemma OAI.MicroscopicJamming.finite_indicator_variance line 319
  50. lemma OAI.MicroscopicJamming.finite_chebyshev line 365
  51. def OAI.MicroscopicJamming.retainedSubsets line 392
  52. lemma OAI.MicroscopicJamming.retainedSubsets_nonempty line 394
  53. lemma OAI.MicroscopicJamming.retainedSubsets_card line 398
  54. lemma OAI.MicroscopicJamming.retained_single_count line 401
  55. lemma OAI.MicroscopicJamming.retained_pair_count line 407
  56. lemma OAI.MicroscopicJamming.choose_ratio_one line 413
  57. lemma OAI.MicroscopicJamming.choose_ratio_two line 424
  58. lemma OAI.MicroscopicJamming.choose_ratio_two_le line 442
  59. lemma OAI.MicroscopicJamming.retained_intersection_variance line 460
  60. theorem OAI.MicroscopicJamming.hypergeometric_deletion line 487
  61. def OAI.MicroscopicJamming.selectRows line 524
  62. lemma OAI.MicroscopicJamming.norm_select_le line 527
  63. lemma OAI.MicroscopicJamming.matrixOperator_select_apply line 536
  64. lemma OAI.MicroscopicJamming.matrixOperator_select_norm line 541
  65. lemma OAI.MicroscopicJamming.selected_rows_adjoint line 548
  66. lemma OAI.MicroscopicJamming.selected_rows_lower_bound line 563
  67. lemma OAI.MicroscopicJamming.measurePreserving_selectRows line 578