OAI/Analysis/HardSphere/Geometry/PairHistory.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Lattice.pairHistory line 13
  2. def OAI.HardSphere.Lattice.fourHistory line 16
  3. def OAI.HardSphere.Lattice.pairDifference line 19
  4. def OAI.HardSphere.Lattice.differenceAt line 21
  5. def OAI.HardSphere.Lattice.atomCoefficient line 24
  6. def OAI.HardSphere.Lattice.pairJoint line 27
  7. lemma OAI.HardSphere.Lattice.pairJoint_eq line 30
  8. lemma OAI.HardSphere.Lattice.pairJoint_bound line 41
  9. lemma OAI.HardSphere.Lattice.fourJoint_eq line 60
  10. theorem OAI.HardSphere.Lattice.difference_point_prediction line 66
  11. def OAI.HardSphere.Lattice.square line 76
  12. lemma OAI.HardSphere.Lattice.square_card line 78
  13. lemma OAI.HardSphere.Lattice.mem_square line 83
  14. theorem OAI.HardSphere.Lattice.difference_square_prediction line 86
  15. def OAI.HardSphere.Lattice.gapKernel line 101
  16. def OAI.HardSphere.Lattice.radiusFactor line 103
  17. lemma OAI.HardSphere.Lattice.radiusFactor_one_le line 105
  18. def OAI.HardSphere.Lattice.encounterEvent line 109
  19. def OAI.HardSphere.Lattice.encounterMass line 112
  20. lemma OAI.HardSphere.Lattice.pmf_outer_le_one line 115
  21. lemma OAI.HardSphere.Lattice.pmf_outer_univ line 119
  22. def OAI.HardSphere.Lattice.historyDifference line 122
  23. lemma OAI.HardSphere.Lattice.historyDifference_actual line 125
  24. lemma OAI.HardSphere.Lattice.encounter_append_bound line 128
  25. lemma OAI.HardSphere.Lattice.encounter_singleton_bound line 150
  26. theorem OAI.HardSphere.Lattice.encounterMass_le_gap_prod line 162
  27. lemma OAI.HardSphere.Lattice.atomCoefficient_sq line 205
  28. lemma OAI.HardSphere.Lattice.gapKernel_sum_ne_top line 214
  29. lemma OAI.HardSphere.Lattice.gapKernel_sum_one_le line 231
  30. def OAI.HardSphere.Lattice.orderedEncounterConstant line 234
  31. lemma OAI.HardSphere.Lattice.orderedEncounterConstant_pos line 236
  32. lemma OAI.HardSphere.Lattice.orderedEncounterConstant_cast line 241
  33. lemma OAI.HardSphere.Lattice.radiusFactor_le line 245
  34. theorem OAI.HardSphere.Lattice.ordered_encounter_sum line 253
  35. def OAI.HardSphere.Lattice.radiusEnvelope line 275
  36. lemma OAI.HardSphere.Lattice.prod_ite_all line 278
  37. lemma OAI.HardSphere.Lattice.radiusEnvelope_prod line 286
  38. def OAI.HardSphere.Lattice.weightedEncounterMass line 304
  39. lemma OAI.HardSphere.Lattice.weightedEncounterMass_eq line 307
  40. def OAI.HardSphere.Lattice.radiusActivity line 327
  41. lemma OAI.HardSphere.Lattice.weighted_ordered_sum_bound line 330
  42. lemma OAI.HardSphere.Lattice.ordered_product_bound_envelope line 357
  43. theorem OAI.HardSphere.Lattice.ordered_product_bound line 376
  44. lemma OAI.HardSphere.Lattice.exp_sub_one_le_slope line 387
  45. lemma OAI.HardSphere.Lattice.radiusEnvelope_smul line 394