LongitudinalCrossing.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The last-rear/first-front portion of an arbitrary continuous past is a longitudinal rectangle crossing. Together with RectangleCrossing this proves the separation assertion used in the ribbon waypoint argument.

theorem OAI.SLEExactGauge.RectangleCrossing.last_rear_before_first_front line 16
def OAI.SLEExactGauge.RectangleCrossing.intervalParam line 56
theorem OAI.SLEExactGauge.RectangleCrossing.intervalParam_mem line 58

theorem OAI.SLEExactGauge.RectangleCrossing.transverse_crossing_hits_past line 68

Source documentation

The continuous past need not be simple. Its transverse separation comes from a compact crossing portion, whose endpoints are selected in the prescribed last-rear/first-front order.

theorem transverse_crossing_hits_past
    (p q : ℝ → ℂ) {T a b c d : ℝ} (hT : 0 < T) (hab : a < b) (hcd : c < d)
    (hp : ContinuousOn p (Icc 0 T)) (hq : ContinuousOn q (Icc 0 1))
    (hp0 : (p 0).re < a) (hpT : b < (p T).re)
    (hpim : ∀ t ∈ Icc (0 : ℝ) T, (p t).im ∈ Icc c d)
    (hqr : ∀ t ∈ Icc (0 : ℝ) 1, (q t).re ∈ Icc a b ∧ (q t).im ∈ Icc c d)
    (hq0 : (q 0).im = c) (hq1 : (q 1).im = d) :
    ∃ s ∈ Icc (0 : ℝ) T, ∃ t ∈ Icc (0 : ℝ) 1, p s = q t := by
…