OAI/Analysis/HardSphere/Paths/TimeGaps.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.DyadicSkeleton.weighted_gap_concentration line 12
  2. def OAI.HardSphere.DyadicSkeleton.timeGaps line 25
  3. lemma OAI.HardSphere.DyadicSkeleton.timeGaps_zero line 29
  4. lemma OAI.HardSphere.DyadicSkeleton.timeGaps_succ line 30
  5. lemma OAI.HardSphere.DyadicSkeleton.timeGaps_castSucc line 33
  6. lemma OAI.HardSphere.DyadicSkeleton.timeGaps_injective line 39
  7. def OAI.HardSphere.DyadicSkeleton.splitVectorEquiv line 55
  8. lemma OAI.HardSphere.DyadicSkeleton.tsum_vector_prod line 61
  9. lemma OAI.HardSphere.DyadicSkeleton.ordered_gap_sum_bound line 73
  10. abbrev OAI.HardSphere.DyadicSkeleton.BoundedTimes line 86
  11. abbrev OAI.HardSphere.DyadicSkeleton.TimeSubset line 87
  12. def OAI.HardSphere.DyadicSkeleton.encodeTimeSubset line 89
  13. def OAI.HardSphere.DyadicSkeleton.decodeTimes line 95
  14. lemma OAI.HardSphere.DyadicSkeleton.decode_encode line 98
  15. lemma OAI.HardSphere.DyadicSkeleton.encodeTimeSubset_injective line 101
  16. lemma OAI.HardSphere.DyadicSkeleton.prod_encode line 106
  17. lemma OAI.HardSphere.DyadicSkeleton.prod_one_add_le_ordered_series line 112
  18. def OAI.HardSphere.DyadicSkeleton.gapKernel line 129
  19. def OAI.HardSphere.DyadicSkeleton.radiusFactor line 131
  20. lemma OAI.HardSphere.DyadicSkeleton.radiusFactor_one_le line 133
  21. lemma OAI.HardSphere.DyadicSkeleton.weighted_gap_radius line 138
  22. def OAI.HardSphere.DyadicSkeleton.encounterMass line 153
  23. lemma OAI.HardSphere.DyadicSkeleton.encounter_append_bound line 157
  24. lemma OAI.HardSphere.DyadicSkeleton.encounter_singleton_bound line 171
  25. lemma OAI.HardSphere.DyadicSkeleton.encounterMass_le_gap_prod line 186
  26. lemma OAI.HardSphere.DyadicSkeleton.gapKernel_sum_ne_top line 224
  27. lemma OAI.HardSphere.DyadicSkeleton.gapKernel_sum_one_le line 242
  28. def OAI.HardSphere.DyadicSkeleton.orderedEncounterConstant line 245
  29. lemma OAI.HardSphere.DyadicSkeleton.orderedEncounterConstant_pos line 246
  30. lemma OAI.HardSphere.DyadicSkeleton.orderedEncounterConstant_cast line 249
  31. lemma OAI.HardSphere.DyadicSkeleton.ordered_encounter_sum line 252
  32. def OAI.HardSphere.DyadicSkeleton.radiusEnvelope line 268
  33. lemma OAI.HardSphere.DyadicSkeleton.measurable_radiusEnvelope line 271
  34. lemma OAI.HardSphere.DyadicSkeleton.radiusEnvelope_prod line 276
  35. def OAI.HardSphere.DyadicSkeleton.weightedEncounterMass line 286
  36. lemma OAI.HardSphere.DyadicSkeleton.weightedEncounterMass_eq line 290
  37. def OAI.HardSphere.DyadicSkeleton.radiusActivity line 301
  38. lemma OAI.HardSphere.DyadicSkeleton.weighted_ordered_sum_bound line 304
  39. lemma OAI.HardSphere.DyadicSkeleton.ordered_product_bound_envelope line 333
  40. lemma OAI.HardSphere.DyadicSkeleton.ordered_product_bound line 352
  41. lemma OAI.HardSphere.DyadicSkeleton.exp_sub_one_le_slope line 358
  42. lemma OAI.HardSphere.DyadicSkeleton.radiusEnvelope_smul line 365
  43. lemma OAI.HardSphere.DyadicSkeleton.radiusActivity_smul line 374
  44. lemma OAI.HardSphere.DyadicSkeleton.ofReal_exp_finset_sum line 381
  45. lemma OAI.HardSphere.DyadicSkeleton.radius_exponential_bound line 387