OAI/Probability/SLE/Gauge/PassageRetention.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Countable, measurable retention of actual middle visits and continuation prefixes. The middle interval is produced from a continuous progress crossing; the compact certificates are then extracted from fixed countable exhaustions.

  1. theorem OAI.SLEExactGauge.PassageRetention.first_progress_crossing line 18

    Source documentation

    First crossing of a scalar progress level on a compact time interval.

    theorem first_progress_crossing
    (x : ℝ → ℝ) {a b q : ℝ} (hab : a < b)
    (hx : ContinuousOn x (Icc a b)) (ha : x a < q) (hb : q < x b) :
    ∃ θ ∈ Ioo a b, x θ = q ∧ ∀ u ∈ Ico a θ, x u < q := by
…
  2. def OAI.SLEExactGauge.PassageRetention.middleRegion line 44
  3. def OAI.SLEExactGauge.PassageRetention.beforeFrontRegion line 47
  4. def OAI.SLEExactGauge.PassageRetention.beyondFrontRegion line 50
  5. theorem OAI.SLEExactGauge.PassageRetention.rational_middle_before_front line 55

    Source documentation

    Progress from below one third to beyond the front at one forces a rational middle interval before the first front crossing and a later rational endpoint.

    theorem rational_middle_before_front
    (f : ℝ → ℂ) (hf : Continuous f) (O : Set ℂ) (hO : IsOpen O)
    (progress : ℂ → ℝ) (hp : ContinuousOn progress O)
    {a b : ℝ} (hab : a < b) (hfO : MapsTo f (Icc a b) O)
    (hstart : progress (f a) < 1 / 3) (hend : 1 < progress (f b)) :
    ∃ s t u : ℚ, a < (s : ℝ) ∧ (s : ℝ) < t ∧ (t : ℝ) < u ∧ (u : ℝ) < b ∧
      MapsTo f (Icc (s : ℝ) t) (middleRegion O progress) ∧
      MapsTo f (Icc a t) (beforeFrontRegion O progress) ∧
      f u ∈ beyondFrontRegion O progress := by
…

    Mentions: OAI.SLEExactGauge.PassageRetention.middleRegion, OAI.SLEExactGauge.PassageRetention.beforeFrontRegion, OAI.SLEExactGauge.PassageRetention.beyondFrontRegion

  6. theorem OAI.SLEExactGauge.PassageRetention.exists_compact_passage_certificates line 107

    Source documentation

    Fixed compact exhaustions provide countably many certificates for both the whole continuation and the middle subinterval.

    theorem exists_compact_passage_certificates
    (O : Set ℂ) (hO : IsOpen O) (progress : ℂ → ℝ)
    (hp : ContinuousOn progress O) :
    ∃ K M L : ℕ → Set ℂ,
      (∀ n, IsCompact (K n) ∧ K n ⊆ O) ∧
      (∀ n, IsCompact (M n) ∧ M n ⊆ middleRegion O progress) ∧
      (∀ n, IsCompact (L n) ∧ L n ⊆ beforeFrontRegion O progress) ∧
      ∀ (f : ℝ → ℂ), Continuous f → ∀ a b : ℝ, a < b →
        MapsTo f (Icc a b) O → progress (f a) < 1 / 3 → 1 < progress (f b) →
        ∃ (s t u : ℚ) (i j k : ℕ),
          a < (s : ℝ) ∧ (s : ℝ) < t ∧ (t : ℝ) < u ∧ (u : ℝ) < b ∧
          f '' Icc a u ⊆ K i ∧ f '' Icc (s : ℝ) t ⊆ M j ∧
…

    Mentions: OAI.SLEExactGauge.PassageRetention.middleRegion, OAI.SLEExactGauge.PassageRetention.beforeFrontRegion

  7. theorem OAI.SLEExactGauge.PassageRetention.isClosed_variable_start_compact line 140

    Source documentation

    Compact containment from a variable starting time is a closed path test.

    theorem isClosed_variable_start_compact (u : ℝ≥0) {K : Set ℂ} (hK : IsClosed K) :
    IsClosed {x : ℝ≥0 × C(ℝ≥0, ℂ) | x.1 ≤ u ∧ MapsTo x.2 (Icc x.1 u) K} := by
…
  8. theorem OAI.SLEExactGauge.PassageRetention.measurableSet_variable_start_compact line 158
  9. def OAI.SLEExactGauge.PassageRetention.ratTime line 165
  10. theorem OAI.SLEExactGauge.PassageRetention.ratTime_coe line 167
  11. theorem OAI.SLEExactGauge.PassageRetention.ratTime_lt line 170
  12. abbrev OAI.SLEExactGauge.PassageRetention.RationalPassageTimes line 175
  13. abbrev OAI.SLEExactGauge.PassageRetention.PassageIndex line 176
  14. def OAI.SLEExactGauge.PassageRetention.intervalStart line 178
  15. def OAI.SLEExactGauge.PassageRetention.intervalEnd line 179
  16. def OAI.SLEExactGauge.PassageRetention.passageEnd line 180
  17. theorem OAI.SLEExactGauge.PassageRetention.intervalStart_lt_end line 182
  18. theorem OAI.SLEExactGauge.PassageRetention.intervalEnd_lt_passageEnd line 185
  19. def OAI.SLEExactGauge.PassageRetention.compactPassageCertificate line 190

    Source documentation

    The three compact tests retain the full prefix, a middle interval, and a prefix ending before any two-thirds front crossing.

    def compactPassageCertificate {Ω : Type*} (f : Ω → C(ℝ≥0, ℂ)) (σ : Ω → ℝ≥0)
    (K M L : ℕ → Set ℂ) (W : Set ℂ) (i : PassageIndex) : Set Ω :=
…

    Mentions: OAI.SLEExactGauge.PassageRetention.PassageIndex

  20. theorem OAI.SLEExactGauge.PassageRetention.compactPassageCertificate_measurable line 197
  21. theorem OAI.SLEExactGauge.PassageRetention.retained_compact_open_margin line 211

    Source documentation

    Fixed compact containment supplies an actual positive open margin.

    theorem retained_compact_open_margin {K O : Set ℂ} (hK : IsCompact K)
    (hO : IsOpen O) (hKO : K ⊆ O) :
    ∃ δ : ℝ, 0 < δ ∧ cthickening δ K ⊆ O :=
…
  22. theorem OAI.SLEExactGauge.PassageRetention.countable_measurable_passage_cover line 218

    Source documentation

    A continuous nonnegative-time path with an actual progress crossing belongs to one of the fixed countable compact certificates.

    theorem countable_measurable_passage_cover
    {Ω : Type*} [MeasurableSpace Ω]
    (f : Ω → C(ℝ≥0, ℂ)) (hf : Measurable f) (σ : Ω → ℝ≥0) (hσ : Measurable σ)
    (O : Set ℂ) (hO : IsOpen O) (hOH : O ⊆ upperHalfPlane)
    (progress : ℂ → ℝ) (hp : ContinuousOn progress O) (E : Set Ω)
    (hpass : ∀ ω ∈ E, ∃ b : ℝ≥0, σ ω < b ∧ MapsTo (f ω) (Icc (σ ω) b) O ∧
      progress (f ω (σ ω)) < 1 / 3 ∧ 1 < progress (f ω b)) :
    ∃ K M L : ℕ → Set ℂ,
      (∀ n, IsCompact (K n) ∧ K n ⊆ O) ∧
      (∀ n, IsCompact (M n) ∧ M n ⊆ middleRegion O progress) ∧
      (∀ n, IsCompact (L n) ∧ L n ⊆ beforeFrontRegion O progress) ∧
      (∀ n, K n ⊆ upperHalfPlane) ∧ (∀ n, M n ⊆ upperHalfPlane) ∧
…

    Mentions: OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.PassageRetention.middleRegion, OAI.SLEExactGauge.PassageRetention.beforeFrontRegion

  23. theorem OAI.SLEExactGauge.PassageRetention.stopped_tube_has_countable_passage_cover line 290

    Source documentation

    The actual future tube event supplies the progress-crossing hypothesis; no compact or interval certificate is assumed.

    theorem stopped_tube_has_countable_passage_cover
    {Ω : Type*} [MeasurableSpace Ω]
    (f : Ω → C(ℝ≥0, ℂ)) (hf : Measurable f) (σ : Ω → ℝ≥0) (hσ : Measurable σ)
    (O W : Set ℂ) (hO : IsOpen O) (hOH : O ⊆ upperHalfPlane)
    (progress : ℂ → ℝ) (hp : ContinuousOn progress O)
    (hW : W ⊆ {z | 1 < progress z}) (E : Set Ω)
    (hE : E ⊆ stoppedPhysicalTube (fun ω => f ω) σ O W)
    (hstart : ∀ ω ∈ E, progress (f ω (σ ω)) < 1 / 3) :
    ∃ K M L : ℕ → Set ℂ,
      (∀ n, IsCompact (K n) ∧ K n ⊆ O) ∧
      (∀ n, IsCompact (M n) ∧ M n ⊆ middleRegion O progress) ∧
      (∀ n, IsCompact (L n) ∧ L n ⊆ beforeFrontRegion O progress) ∧
…

    Mentions: OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.stoppedPhysicalTube, OAI.SLEExactGauge.PassageRetention.middleRegion, OAI.SLEExactGauge.PassageRetention.beforeFrontRegion

  24. abbrev OAI.SLEExactGauge.PassageRetention.RetainedPassageIndex line 316
  25. def OAI.SLEExactGauge.PassageRetention.retainedPassageCertificate line 318
  26. theorem OAI.SLEExactGauge.PassageRetention.stopped_tube_retained_cover line 325

    Source documentation

    Actual tube passages admit a countable measurable cover with compact endpoint margins as well as compact prefix and middle margins.

    theorem stopped_tube_retained_cover
    {Ω : Type*} [MeasurableSpace Ω]
    (f : Ω → C(ℝ≥0, ℂ)) (hf : Measurable f) (σ : Ω → ℝ≥0) (hσ : Measurable σ)
    (O W : Set ℂ) (hO : IsOpen O) (hOH : O ⊆ upperHalfPlane)
    (progress : ℂ → ℝ) (hp : ContinuousOn progress O)
    (hW : W ⊆ {z | 1 < progress z}) (E : Set Ω)
    (hE : E ⊆ stoppedPhysicalTube (fun ω => f ω) σ O W)
    (hstart : ∀ ω ∈ E, progress (f ω (σ ω)) < 1 / 3) :
    ∃ K M L N : ℕ → Set ℂ,
      (∀ n, IsCompact (K n) ∧ K n ⊆ O) ∧
      (∀ n, IsCompact (M n) ∧ M n ⊆ middleRegion O progress) ∧
      (∀ n, IsCompact (L n) ∧ L n ⊆ beforeFrontRegion O progress) ∧
…

    Mentions: OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.stoppedPhysicalTube, OAI.SLEExactGauge.PassageRetention.middleRegion, OAI.SLEExactGauge.PassageRetention.beforeFrontRegion

  27. theorem OAI.SLEExactGauge.PassageRetention.retained_certificate_transfers line 359

    Source documentation

    On each retained certificate all strict passage conditions transfer uniformly to sufficiently late locally convergent maps.

    theorem retained_certificate_transfers
    {Ω : Type*} (f : Ω → C(ℝ≥0, ℂ)) (σ : Ω → ℝ≥0)
    (K M L N : ℕ → Set ℂ) (W : Set ℂ) (i : RetainedPassageIndex)
    (Fₙ : ℕ → ℂ → ℂ) (F : ℂ → ℂ)
    (hconv : TendstoLocallyUniformlyOn Fₙ F atTop upperHalfPlane)
    (hF : ContinuousOn F upperHalfPlane)
    (hK : IsCompact (K i.1.2.1)) (hKH : K i.1.2.1 ⊆ upperHalfPlane)
    (hM : IsCompact (M i.1.2.2.1)) (hMH : M i.1.2.2.1 ⊆ upperHalfPlane)
    (hL : IsCompact (L i.1.2.2.2)) (hLH : L i.1.2.2.2 ⊆ upperHalfPlane)
    (hN : IsCompact (N i.2)) (hNH : N i.2 ⊆ upperHalfPlane)
    (R Rmid Rlow Rhigh : Set ℂ)
    (hR : IsOpen R) (hRmid : IsOpen Rmid) (hRlow : IsOpen Rlow) (hRhigh : IsOpen Rhigh)
…

    Mentions: OAI.SLEExactGauge.PassageRetention.RetainedPassageIndex, OAI.SLEExactGauge.upperHalfPlane

  28. theorem OAI.SLEExactGauge.PassageRetention.retained_interval_before_front line 390

    Source documentation

    The middle interval lies before every later time which attains the front level; in particular it precedes the first such passage stop.

    theorem retained_interval_before_front
    {Ω : Type*} (f : Ω → C(ℝ≥0, ℂ)) (σ : Ω → ℝ≥0)
    (K M L N : ℕ → Set ℂ) (W : Set ℂ) (i : RetainedPassageIndex)
    (progress : ℂ → ℝ) (hL : ∀ z ∈ L i.1.2.2.2, progress z < 2 / 3)
    (ω : Ω) (hω : ω ∈ retainedPassageCertificate f σ K M L N W i)
    (τ : ℝ≥0) (hστ : σ ω ≤ τ) (hτ : 2 / 3 ≤ progress (f ω τ)) :
    intervalEnd i.1 < τ := by
…

    Mentions: OAI.SLEExactGauge.PassageRetention.RetainedPassageIndex, OAI.SLEExactGauge.PassageRetention.retainedPassageCertificate, OAI.SLEExactGauge.PassageRetention.intervalEnd

  29. instance OAI.SLEExactGauge.PassageRetention.rationalPassageTimes_nonempty line 402
  30. def OAI.SLEExactGauge.PassageRetention.enumerateRetainedPassage line 407

    Source documentation

    Enumerating the concrete rational/compact indices gives the natural indexing expected by finite-retention and unconditional sausage lemmas.

    def enumerateRetainedPassage : ℕ → RetainedPassageIndex :=
…

    Mentions: OAI.SLEExactGauge.PassageRetention.RetainedPassageIndex

  31. theorem OAI.SLEExactGauge.PassageRetention.enumerateRetainedPassage_surjective line 410
  32. theorem OAI.SLEExactGauge.PassageRetention.nat_retained_cover line 413