OAI/Analysis/HardSphere/Geometry/Sigma.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.Lattice.block_scale line 13
  2. lemma OAI.HardSphere.Lattice.aligned_block_exists line 22
  3. def OAI.HardSphere.Lattice.sigma line 38
  4. lemma OAI.HardSphere.Lattice.sigma_gt_half line 40
  5. lemma OAI.HardSphere.Lattice.sigma_pos line 47
  6. lemma OAI.HardSphere.Lattice.three_rpow_sigma line 49
  7. lemma OAI.HardSphere.Lattice.atom_power_bound line 53
  8. theorem OAI.HardSphere.Lattice.prediction line 69
  9. theorem OAI.HardSphere.Lattice.walk_zero line 97
  10. theorem OAI.HardSphere.Lattice.walk_increment line 99
  11. lemma OAI.HardSphere.Lattice.map_pair_fiber line 106
  12. lemma OAI.HardSphere.Lattice.conditional_push_history line 118
  13. def OAI.HardSphere.Lattice.positionHistory line 129
  14. def OAI.HardSphere.Lattice.positionsFromIncrements line 131
  15. lemma OAI.HardSphere.Lattice.positionHistory_eq line 134
  16. theorem OAI.HardSphere.Lattice.position_prediction line 141
  17. theorem OAI.HardSphere.Lattice.finite_prediction_walk line 156
  18. def OAI.HardSphere.Lattice.independentPair line 168
  19. lemma OAI.HardSphere.Lattice.independentPair_apply line 171
  20. lemma OAI.HardSphere.Lattice.independentPair_map line 184
  21. lemma OAI.HardSphere.Lattice.pmf_fst line 191
  22. lemma OAI.HardSphere.Lattice.enn_tsum_ite_const line 197
  23. lemma OAI.HardSphere.Lattice.independent_difference_fiber line 201
  24. lemma OAI.HardSphere.Lattice.independent_difference_bound line 215
  25. def OAI.HardSphere.Lattice.independentJoint line 224
  26. lemma OAI.HardSphere.Lattice.independentJoint_apply line 228
  27. lemma OAI.HardSphere.Lattice.independentJoint_fst line 237
  28. lemma OAI.HardSphere.Lattice.independentJoint_bound line 243
  29. lemma OAI.HardSphere.Lattice.joint_region_mass line 251
  30. lemma OAI.HardSphere.Lattice.joint_region_bound line 264
  31. def OAI.HardSphere.Lattice.timeGaps line 280
  32. lemma OAI.HardSphere.Lattice.timeGaps_zero line 284
  33. lemma OAI.HardSphere.Lattice.timeGaps_succ line 285
  34. lemma OAI.HardSphere.Lattice.timeGaps_castSucc line 288
  35. lemma OAI.HardSphere.Lattice.timeGaps_injective line 294
  36. def OAI.HardSphere.Lattice.splitVectorEquiv line 310
  37. lemma OAI.HardSphere.Lattice.tsum_vector_prod line 316
  38. lemma OAI.HardSphere.Lattice.ordered_gap_sum_bound line 328
  39. abbrev OAI.HardSphere.Lattice.BoundedTimes line 341
  40. abbrev OAI.HardSphere.Lattice.TimeSubset line 342
  41. def OAI.HardSphere.Lattice.encodeTimeSubset line 344
  42. def OAI.HardSphere.Lattice.decodeTimes line 350
  43. lemma OAI.HardSphere.Lattice.decode_encode line 353
  44. lemma OAI.HardSphere.Lattice.encodeTimeSubset_injective line 356
  45. lemma OAI.HardSphere.Lattice.prod_encode line 361
  46. lemma OAI.HardSphere.Lattice.prod_one_add_le_ordered_series line 367
  47. abbrev OAI.HardSphere.Lattice.PairNoise line 384
  48. abbrev OAI.HardSphere.Lattice.FourNoise line 385
  49. abbrev OAI.HardSphere.Lattice.PairHistory line 386
  50. abbrev OAI.HardSphere.Lattice.FourHistory line 387
  51. def OAI.HardSphere.Lattice.pairLaw line 389
  52. def OAI.HardSphere.Lattice.fourLaw line 392