OAI/Probability/SLE/Geometry/FiniteStopSorting.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

A finite min/max sorting network for bounded stopping times. Unlike sorting sampled values by a sample-dependent permutation, every output is directly a stopping time. Ties and simultaneous switches are kept.

  1. def OAI.SLEExactGauge.Multipoint.insertStop line 15
  2. def OAI.SLEExactGauge.Multipoint.sortStops line 20
  3. lemma OAI.SLEExactGauge.Multipoint.insertStop_length line 24
  4. lemma OAI.SLEExactGauge.Multipoint.sortStops_length line 30
  5. lemma OAI.SLEExactGauge.Multipoint.insertStop_lower_bound line 36
  6. lemma OAI.SLEExactGauge.Multipoint.insertStop_ordered line 52
  7. theorem OAI.SLEExactGauge.Multipoint.sortStops_ordered line 65
  8. lemma OAI.SLEExactGauge.Multipoint.insertStop_permutation line 71
  9. theorem OAI.SLEExactGauge.Multipoint.sortStops_permutation line 86
  10. lemma OAI.SLEExactGauge.Multipoint.insertStop_bounded line 93
  11. theorem OAI.SLEExactGauge.Multipoint.sortStops_bounded line 109
  12. lemma OAI.SLEExactGauge.Multipoint.insertStop_stopping line 117
  13. theorem OAI.SLEExactGauge.Multipoint.sortStops_stopping line 136
  14. def OAI.SLEExactGauge.Multipoint.sortedStopAt line 146
  15. theorem OAI.SLEExactGauge.Multipoint.sortedStopAt_stopping line 149
  16. theorem OAI.SLEExactGauge.Multipoint.sortedStopAt_bounded line 159
  17. theorem OAI.SLEExactGauge.Multipoint.sortedStopAt_monotone line 166
  18. theorem OAI.SLEExactGauge.Multipoint.sortedStopAt_length line 183
  19. theorem OAI.SLEExactGauge.Multipoint.sortedStopAt_covers line 188

    Source documentation

    Every original switch occurs in the sorted sequence, including ties.

    theorem sortedStopAt_covers {Ω : Type*} (l : List (Ω → ℝ≥0)) (H : ℝ≥0)
    (σ : Ω → ℝ≥0) (hσ : σ ∈ l) (ω : Ω) :
    ∃ n < l.length, sortedStopAt l H n ω = σ ω := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.sortedStopAt

  20. theorem OAI.SLEExactGauge.Multipoint.sortedStopAt_zero line 198