OAI/Probability/SLE/Geometry/GuideSplice.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

The deterministic last-crossing and connector geometry following es:good-semicircle. All sets below are actual subsets of the complex plane.

  1. theorem OAI.SLEExactGauge.GuideSplice.exists_last_circle_crossing line 19

    Source documentation

    The final crossing of a small circle occurs before the specified positive time; the remainder of the guide lies strictly outside that circle.

    theorem exists_last_circle_crossing
    {β : ℝ → ℂ} {B δ T : ℝ} (hB : 0 < B) (hδ : 0 < δ) (hδT : δ ≤ T)
    (hβ : ContinuousOn β (Icc 0 T)) (hβ₀ : β 0 = 0)
    (hlate : ∀ t ∈ Icc δ T, B < ‖β t‖) :
    ∃ tB ∈ Ioo 0 δ, ‖β tB‖ = B ∧
      ∀ t ∈ Ioc tB T, B < ‖β t‖ := by
…
  2. def OAI.SLEExactGauge.GuideSplice.connectorTop line 56
  3. def OAI.SLEExactGauge.GuideSplice.verticalConnector line 58
  4. def OAI.SLEExactGauge.GuideSplice.initialRectangle line 61
  5. lemma OAI.SLEExactGauge.GuideSplice.circle_height_pos line 64
  6. lemma OAI.SLEExactGauge.GuideSplice.connectorTop_norm line 70
  7. theorem OAI.SLEExactGauge.GuideSplice.verticalConnector_subset_sector line 81

    Source documentation

    The entire vertical connector lies in the central sector controlled by the small-image estimate, including its lower endpoint.

    theorem verticalConnector_subset_sector {B x : ℝ}
    (hB : 0 < B) (hx : |x| < B / 16) :
    verticalConnector B x ⊆
      {z | B / 8 ≤ ‖z‖ ∧ ‖z‖ ≤ B ∧ ‖z‖ / 2 ≤ z.im} := by
…

    Mentions: OAI.SLEExactGauge.GuideSplice.verticalConnector

  8. lemma OAI.SLEExactGauge.GuideSplice.initialRectangle_subset_smallBall line 102
  9. lemma OAI.SLEExactGauge.GuideSplice.verticalConnector_meets_rectangle_only_at_start line 116

    Source documentation

    Above its first point, the vertical connector is disjoint from every initial hull contained in the specified rectangle.

    lemma verticalConnector_meets_rectangle_only_at_start {B x : ℝ}
    {z : ℂ} (hz : z ∈ verticalConnector B x) (hrect : z ∈ initialRectangle B) :
    z = (x : ℂ) + ((B / 4 : ℝ) : ℂ) * Complex.I := by
…

    Mentions: OAI.SLEExactGauge.GuideSplice.verticalConnector, OAI.SLEExactGauge.GuideSplice.initialRectangle

  10. lemma OAI.SLEExactGauge.GuideSplice.circle_and_outerGuide_avoid_initialRectangle line 123
  11. def OAI.SLEExactGauge.GuideSplice.semicircleArc line 129
  12. lemma OAI.SLEExactGauge.GuideSplice.semicircleArc_compact line 132
  13. lemma OAI.SLEExactGauge.GuideSplice.semicircleArc_norm line 136
  14. lemma OAI.SLEExactGauge.GuideSplice.semicircleArc_subset_halfPlane line 141
  15. lemma OAI.SLEExactGauge.GuideSplice.verticalConnector_eq_image line 149
  16. lemma OAI.SLEExactGauge.GuideSplice.verticalConnector_compact line 160
  17. lemma OAI.SLEExactGauge.GuideSplice.verticalConnector_subset_halfPlane line 165
  18. def OAI.SLEExactGauge.GuideSplice.continuationRoute line 172

    Source documentation

    The actual compact set traced by the vertical piece, the circular piece, and the remainder of the guide.

    def continuationRoute (B x α ω : ℝ) (β : ℝ → ℂ) (tB T : ℝ) : Set ℂ :=
…
  19. theorem OAI.SLEExactGauge.GuideSplice.continuationRoute_compact line 175
  20. theorem OAI.SLEExactGauge.GuideSplice.continuationRoute_subset_halfPlane line 182
  21. theorem OAI.SLEExactGauge.GuideSplice.continuationRoute_meets_rectangle_only_at_start line 195

    Source documentation

    The continuation route avoids an arbitrary hull in the source rectangle, except at its initial tip.

    theorem continuationRoute_meets_rectangle_only_at_start
    {B x α ω tB T : ℝ} {β : ℝ → ℂ} (hB : 0 < B)
    (hcross : ‖β tB‖ = B) (hafter : ∀ t ∈ Ioc tB T, B < ‖β t‖)
    {z : ℂ} (hz : z ∈ continuationRoute B x α ω β tB T)
    (hrect : z ∈ initialRectangle B) :
    z = (x : ℂ) + ((B / 4 : ℝ) : ℂ) * Complex.I := by
…

    Mentions: OAI.SLEExactGauge.GuideSplice.continuationRoute, OAI.SLEExactGauge.GuideSplice.initialRectangle

  22. lemma OAI.SLEExactGauge.GuideSplice.verticalConnector_meets_circle_only_at_top line 212

    Source documentation

    The vertical connector reaches the radius-B circle only at its top.

    lemma verticalConnector_meets_circle_only_at_top {B x : ℝ}
    (hB : 0 < B) (hx : |x| < B / 16) {z : ℂ}
    (hz : z ∈ verticalConnector B x) (hcircle : ‖z‖ = B) :
    z = connectorTop B x := by
…

    Mentions: OAI.SLEExactGauge.GuideSplice.verticalConnector, OAI.SLEExactGauge.GuideSplice.connectorTop

  23. lemma OAI.SLEExactGauge.GuideSplice.tail_meets_circle_only_at_start line 227

    Source documentation

    The tail meets the selected circle only at the last-crossing point.

    lemma tail_meets_circle_only_at_start {β : ℝ → ℂ} {B tB T : ℝ}
    (hafter : ∀ t ∈ Ioc tB T, B < ‖β t‖) {z : ℂ}
    (hz : z ∈ β '' Icc tB T) (hcircle : ‖z‖ = B) : z = β tB := by
…
  24. lemma OAI.SLEExactGauge.GuideSplice.verticalConnector_inter_semicircleArc line 235
  25. lemma OAI.SLEExactGauge.GuideSplice.semicircleArc_inter_tail line 241
  26. lemma OAI.SLEExactGauge.GuideSplice.verticalConnector_inter_tail line 247
  27. lemma OAI.SLEExactGauge.GuideSplice.path_trans_injective line 260
  28. def OAI.SLEExactGauge.GuideSplice.circlePoint line 292
  29. def OAI.SLEExactGauge.GuideSplice.circularPath line 294
  30. lemma OAI.SLEExactGauge.GuideSplice.circularPath_range line 299
  31. lemma OAI.SLEExactGauge.GuideSplice.circularPath_injective line 304
  32. lemma OAI.SLEExactGauge.GuideSplice.path_trans_injective_of_inter line 326
  33. lemma OAI.SLEExactGauge.GuideSplice.circle_height_gt_quarter line 334
  34. def OAI.SLEExactGauge.GuideSplice.verticalPath line 341
  35. lemma OAI.SLEExactGauge.GuideSplice.verticalPath_range line 347
  36. lemma OAI.SLEExactGauge.GuideSplice.verticalPath_injective line 354
  37. def OAI.SLEExactGauge.GuideSplice.tailPath line 364
  38. lemma OAI.SLEExactGauge.GuideSplice.tailPath_range line 370
  39. lemma OAI.SLEExactGauge.GuideSplice.tailPath_injective line 375
  40. theorem OAI.SLEExactGauge.GuideSplice.exists_simple_continuation_path line 388

    Source documentation

    The three source pieces form an actual simple continuation path. When the circular arc degenerates, it is omitted from the parametrization.

    theorem exists_simple_continuation_path
    {B x α ω tB T : ℝ} {β : ℝ → ℂ}
    (hB : 0 < B) (hx : |x| < B / 16)
    (hα : α ∈ Ioo 0 Real.pi) (hω : ω ∈ Ioo 0 Real.pi)
    (htB : tB < T) (hβ : ContinuousOn β (Icc tB T)) (hi : InjOn β (Icc tB T))
    (hstart : connectorTop B x = circlePoint B α) (hend : β tB = circlePoint B ω)
    (hcross : ‖β tB‖ = B) (hafter : ∀ t ∈ Ioc tB T, B < ‖β t‖) :
    ∃ p : Path ((x : ℂ) + ((B / 4 : ℝ) : ℂ) * Complex.I) (β T),
      Function.Injective p ∧ range p = continuationRoute B x α ω β tB T := by
…

    Mentions: OAI.SLEExactGauge.GuideSplice.connectorTop, OAI.SLEExactGauge.GuideSplice.circlePoint, OAI.SLEExactGauge.GuideSplice.continuationRoute

  41. lemma OAI.SLEExactGauge.GuideSplice.arg_mem_upper_interval line 440
  42. theorem OAI.SLEExactGauge.GuideSplice.exists_simple_splice_path line 449

    Source documentation

    The source splice as an injective path in a compact subset of the upper half-plane. It meets any initial hull in the prescribed rectangle only at the starting tip.

    theorem exists_simple_splice_path
    {B x tB T : ℝ} {β : ℝ → ℂ} (hB : 0 < B) (hx : |x| < B / 16)
    (htB₀ : 0 < tB) (htBT : tB < T)
    (hβ : ContinuousOn β (Icc 0 T)) (hi : InjOn β (Icc 0 T))
    (hβH : ∀ t ∈ Ioc 0 T, 0 < (β t).im)
    (hcross : ‖β tB‖ = B) (hafter : ∀ t ∈ Ioc tB T, B < ‖β t‖) :
    ∃ p : Path ((x : ℂ) + ((B / 4 : ℝ) : ℂ) * Complex.I) (β T),
      Function.Injective p ∧ IsCompact (range p) ∧
      range p ⊆ {z : ℂ | 0 < z.im} ∧
      (∀ z ∈ range p, z ∈ initialRectangle B →
        z = (x : ℂ) + ((B / 4 : ℝ) : ℂ) * Complex.I) ∧
      range p = continuationRoute B x (connectorTop B x).arg (β tB).arg β tB T := by
…

    Mentions: OAI.SLEExactGauge.GuideSplice.initialRectangle, OAI.SLEExactGauge.GuideSplice.continuationRoute, OAI.SLEExactGauge.GuideSplice.connectorTop