OAI/Analysis/HardSphere/Bridges/BridgeNoise.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Bridge.fluctuation line 16
  2. lemma OAI.HardSphere.Bridge.fluctuation_continuous line 17
  3. lemma OAI.HardSphere.Bridge.fluctuation_nonneg line 19
  4. lemma OAI.HardSphere.Bridge.fluctuation_memLp line 21
  5. lemma OAI.HardSphere.Bridge.fluctuation_mean line 24
  6. lemma OAI.HardSphere.Bridge.prefix_norm_eval line 47
  7. lemma OAI.HardSphere.Bridge.fluctuation_eval line 58
  8. lemma OAI.HardSphere.GaussianPacking.cube_volume line 78
  9. lemma OAI.HardSphere.GaussianPacking.measurable_cube_event line 83
  10. theorem OAI.HardSphere.GaussianPacking.collision_volume_bound line 93
  11. theorem OAI.HardSphere.GaussianPacking.collision_cubic_bound line 120
  12. lemma OAI.HardSphere.Bridge.leg_segment line 153
  13. def OAI.HardSphere.Bridge.segmentHit line 160
  14. lemma OAI.HardSphere.Bridge.segment_necessary line 163
  15. lemma OAI.HardSphere.Bridge.segment_sum_bound line 189