OAI/Probability/SLE/Geometry/GuideTube.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SLEExactGauge.GuideSplice.closedInitialRectangle line 18
2. lemma OAI.SLEExactGauge.GuideSplice.closedInitialRectangle_isClosed line 21
3. lemma OAI.SLEExactGauge.GuideSplice.initialRectangle_subset_closed line 26
4. lemma OAI.SLEExactGauge.GuideSplice.closedInitialRectangle_subset_smallBall line 30
5. lemma OAI.SLEExactGauge.GuideSplice.outer_circle_avoids_closedInitialRectangle line 42
6. lemma OAI.SLEExactGauge.GuideSplice.continuationRoute_meets_closed_rectangle_only_at_start line 48
7. theorem OAI.SLEExactGauge.GuideSplice.initial_splice_image_subset_quarter_ball line 67

   Source documentation

   The image bound for the actual initial vertical and circular pieces.

   theorem initial_splice_image_subset_quarter_ball
       {F : ℂ → ℂ} {a : ℂ} {B x α ω r : ℝ}
       (hB : 0 < B) (hx : |x| < B / 16)
       (hα : α ∈ Ioo 0 Real.pi) (hω : ω ∈ Ioo 0 Real.pi)
       (hcircle : ∀ θ ∈ Ioo 0 Real.pi, ‖F (circlePoint B θ) - a‖ < r / 4)
       (hsector : ∀ z : ℂ, B / 8 ≤ ‖z‖ → ‖z‖ ≤ B → ‖z‖ / 2 ≤ z.im →
         ‖F z - a‖ < r / 4) :
       F '' (verticalConnector B x ∪ semicircleArc B α ω) ⊆ ball a (r / 4) := by
   …

   Mentions: OAI.SLEExactGauge.GuideSplice.circlePoint, OAI.SLEExactGauge.GuideSplice.verticalConnector, OAI.SLEExactGauge.GuideSplice.semicircleArc

8. def OAI.SLEExactGauge.GuideSplice.continuationTube line 82
9. lemma OAI.SLEExactGauge.GuideSplice.continuationTube_isOpen line 85
10. lemma OAI.SLEExactGauge.GuideSplice.continuationTube_subset_halfPlane line 91
11. lemma OAI.SLEExactGauge.GuideSplice.continuationTube_disjoint_rectangle line 94
12. lemma OAI.SLEExactGauge.GuideSplice.continuationTube_image_subset line 98
13. theorem OAI.SLEExactGauge.GuideSplice.continuationRoute_rest_subset_tube line 106

    Source documentation

    An open tube avoids the entire initial rectangle while retaining every continuation point other than the initial tip. Its physical image lies in the half-radius ball or in the prescribed open region for the compact tail.

    theorem continuationRoute_rest_subset_tube
        {F : ℂ → ℂ} {a : ℂ} {B x α ω r tB T : ℝ} {β : ℝ → ℂ} {O : Set ℂ}
        (hr : 0 < r) (hB : 0 < B) (hx : |x| < B / 16)
        (hα : α ∈ Ioo 0 Real.pi) (hω : ω ∈ Ioo 0 Real.pi) (htB : 0 < tB)
        (hβH : ∀ t ∈ Ioc 0 T, 0 < (β t).im)
        (hcross : ‖β tB‖ = B) (hafter : ∀ t ∈ Ioc tB T, B < ‖β t‖)
        (hcircle : ∀ θ ∈ Ioo 0 Real.pi, ‖F (circlePoint B θ) - a‖ < r / 4)
        (hsector : ∀ z : ℂ, B / 8 ≤ ‖z‖ → ‖z‖ ≤ B → ‖z‖ / 2 ≤ z.im →
          ‖F z - a‖ < r / 4)
        (htail : F '' (β '' Icc tB T) ⊆ O) :
        continuationRoute B x α ω β tB T \
            {(x : ℂ) + ((B / 4 : ℝ) : ℂ) * Complex.I} ⊆ continuationTube F a r B O := by
    …

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

14. lemma OAI.SLEExactGauge.GuideSplice.initial_tip_mem_closure_of_connector_rest line 133
15. lemma OAI.SLEExactGauge.GuideSplice.initial_tip_mem_closure_of_route_rest line 168
16. theorem OAI.SLEExactGauge.GuideSplice.compact_initial_splice_has_small_image_tube line 178

    Source documentation

    Compact parts of the initial splice have a tube lying entirely in the physical half-radius ball, as well as outside the old containing rectangle.

    theorem compact_initial_splice_has_small_image_tube
        {F : ℂ → ℂ} (hF : ContinuousOn F upperHalfPlane) {a : ℂ}
        {B x α ω r : ℝ} (hr : 0 < r) (hB : 0 < B) (hx : |x| < B / 16)
        (hα : α ∈ Ioo 0 Real.pi) (hω : ω ∈ Ioo 0 Real.pi)
        (hcircle : ∀ θ ∈ Ioo 0 Real.pi, ‖F (circlePoint B θ) - a‖ < r / 4)
        (hsector : ∀ z : ℂ, B / 8 ≤ ‖z‖ → ‖z‖ ≤ B → ‖z‖ / 2 ≤ z.im →
          ‖F z - a‖ < r / 4)
        (K : Set ℂ) (hK : IsCompact K)
        (hsub : K ⊆ (verticalConnector B x ∪ semicircleArc B α ω) \
          {(x : ℂ) + ((B / 4 : ℝ) : ℂ) * Complex.I}) :
        ∃ ε : ℝ, 0 < ε ∧ thickening ε K ⊆ continuationTube F a r B ∅ := by
    …

    Mentions: OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.GuideSplice.circlePoint, OAI.SLEExactGauge.GuideSplice.verticalConnector, OAI.SLEExactGauge.GuideSplice.semicircleArc, OAI.SLEExactGauge.GuideSplice.continuationTube

17. theorem OAI.SLEExactGauge.GuideSplice.positive_subpath_has_uniform_tube line 210

    Source documentation

    Every compact positive-time piece of a simple route has a uniform tube radius; the radius is allowed to shrink towards the initial tip.

    theorem positive_subpath_has_uniform_tube
        {z₀ z₁ : ℂ} (p : Path z₀ z₁) (hp : Function.Injective p)
        {N : Set ℂ} (hN : IsOpen N) (hsub : range p \ {z₀} ⊆ N)
        (δ : unitInterval) (hδ : 0 < (δ : ℝ)) :
        ∃ ε : ℝ, 0 < ε ∧ thickening ε (p '' Icc δ 1) ⊆ N := by
    …