OAI/Probability/Ballisticity/Estimates/AlignedRecordPrefix.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.AlignedRecordPrefix line 18
  2. lemma OAI.DirectionalTransience.alignedRecordPrefix_order line 23
  3. def OAI.DirectionalTransience.FirstPairTest line 34
  4. lemma OAI.DirectionalTransience.measurableSet_firstPairTest line 37
  5. lemma OAI.DirectionalTransience.firstPairTest_prefix line 44
  6. lemma OAI.DirectionalTransience.firstPairTest_disjoint line 54
  7. lemma OAI.DirectionalTransience.iUnion_firstPairTest line 66
  8. theorem OAI.DirectionalTransience.independent_exact_cut_transfer line 80
  9. def OAI.DirectionalTransience.RecordOrZeroPrefix line 128
  10. lemma OAI.DirectionalTransience.measurableSet_recordOrZeroPrefix line 131
  11. lemma OAI.DirectionalTransience.recordOrZeroPrefix_prefix line 138
  12. lemma OAI.DirectionalTransience.recordOrZeroPrefix_time line 146
  13. def OAI.DirectionalTransience.PairOscillationTest line 154
  14. lemma OAI.DirectionalTransience.measurableSet_pairOscillationTest line 163
  15. lemma OAI.DirectionalTransience.pairOscillationTest_prefix line 185
  16. lemma OAI.DirectionalTransience.pairOscillationTest_aligned line 202
  17. lemma OAI.DirectionalTransience.independent_firstHit_aligned line 208
  18. lemma OAI.DirectionalTransience.firstHitPairGap_prefix_test line 242
  19. theorem OAI.DirectionalTransience.independent_firstHit_oscillation_transfer line 272
  20. def OAI.DirectionalTransience.commonBoundaryGap line 307
  21. def OAI.DirectionalTransience.commonDecoration line 312
  22. lemma OAI.DirectionalTransience.commonBoundaryGap_eq_at_true line 317
  23. lemma OAI.DirectionalTransience.independent_commonBoundary_at_true line 336
  24. theorem OAI.DirectionalTransience.independent_firstHit_boundary_transfer line 352
  25. theorem OAI.DirectionalTransience.independent_firstHit_gap_transfer line 371
  26. def OAI.DirectionalTransience.HeightBlockRelation line 389
  27. def OAI.DirectionalTransience.HeightOscillation line 392
  28. def OAI.DirectionalTransience.BlockDecoration line 395
  29. def OAI.DirectionalTransience.HeightGapEvent line 398
  30. lemma OAI.DirectionalTransience.heightBlockRelation_order line 401
  31. lemma OAI.DirectionalTransience.heightGap_subset line 407