OAI/Analysis/HardSphere/Bridges/GaussianPacking.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HardSphere.GaussianPacking.Point line 13
  2. def OAI.HardSphere.GaussianPacking.square line 14
  3. def OAI.HardSphere.GaussianPacking.kernel line 15
  4. def OAI.HardSphere.GaussianPacking.cube line 16
  5. lemma OAI.HardSphere.GaussianPacking.kernel_product line 18
  6. lemma OAI.HardSphere.GaussianPacking.kernel_integrable line 21
  7. lemma OAI.HardSphere.GaussianPacking.kernel_integral line 25
  8. lemma OAI.HardSphere.GaussianPacking.cube_real_volume line 30
  9. lemma OAI.HardSphere.GaussianPacking.cube_coord line 34
  10. lemma OAI.HardSphere.GaussianPacking.square_triangle line 39
  11. lemma OAI.HardSphere.GaussianPacking.square_le_of_coord line 46
  12. lemma OAI.HardSphere.GaussianPacking.cube_kernel_lower line 53
  13. lemma OAI.HardSphere.GaussianPacking.cubes_disjoint line 67
  14. lemma OAI.HardSphere.GaussianPacking.kernel_translate_integrable line 83
  15. lemma OAI.HardSphere.GaussianPacking.sum_kernel_le line 87
  16. abbrev OAI.HardSphere.Bridge.Noise line 128
  17. def OAI.HardSphere.Bridge.law line 129
  18. instance OAI.HardSphere.Bridge.(instance at line 130) line 130
  19. def OAI.HardSphere.Bridge.eval line 132
  20. def OAI.HardSphere.Bridge.remainder line 133
  21. lemma OAI.HardSphere.Bridge.eval_measurable line 134
  22. lemma OAI.HardSphere.Bridge.remainder_measurable line 137
  23. def OAI.HardSphere.Bridge.variance line 139
  24. lemma OAI.HardSphere.Bridge.scalar_eval line 140
  25. lemma OAI.HardSphere.Bridge.scalar_remainder line 143
  26. lemma OAI.HardSphere.Bridge.scalar_joint line 147
  27. lemma OAI.HardSphere.Bridge.eval_law line 158
  28. lemma OAI.HardSphere.Bridge.remainder_law line 162
  29. lemma OAI.HardSphere.Bridge.joint_law line 169
  30. lemma OAI.HardSphere.Bridge.independent line 186