Maximal solutions of the chordal Loewner equation and the Loewner hulls

TheoremPositivity persists under a nonnegative derivative#✓fully proved

A continuous function on [0, T] that is positive at 0 and has a nonnegative derivative at every interior point where it is positive stays positive on [0, T].

theorem positiveOn_Icc_of_deriv_nonneg_while_pos
    {T : ℝ} {f : ℝ → ℝ}
    (hcont : ContinuousOn f (Icc (0 : ℝ) T)) (hzero : 0 < f 0)
    (hderiv : ∀ s ∈ Ioo (0 : ℝ) T, 0 < f s →
      ∃ v : ℝ, HasDerivAt f v s ∧ 0 ≤ v) :
    ∀ s ∈ Icc (0 : ℝ) T, 0 < f s

Used by 1

Used byLoewner hulls are compact hulls

StructureForward solution of the Loewner equation#✓fully proved

A solution t ↦ g_t(z) of the Loewner equation on [0, T] (one-sided derivatives at the endpoints) with g_0(z) = z and g_t(z) ∈ ℍ for t ∈ [0, T].

structure LoewnerForwardSolution (W : ℝ → ℝ) (z : ℂ) (T : ℝ) where
  curve : ℝ → ℂ
  initial : curve 0 = z
  deriv : ∀ t ∈ Icc (0 : ℝ) T,
    HasDerivWithinAt curve (loewnerField W t (curve t)) (Icc (0 : ℝ) T) t
  upper : ∀ t ∈ Icc (0 : ℝ) T, curve t ∈ upperHalfPlaneSet

Uses 1 · Used by 15

Statement usesChordal Loewner vector field

Used byConcatenation of Loewner forward solutions · Concatenated curve of two Loewner solutions · Admissible duration for the Loewner equation · Maximal Loewner trajectory · Maximal solution of the chordal Loewner equation · Loewner map as a homeomorphism onto the half-plane · Inverse of the maximal Loewner map · Maximal Loewner maps solve the maximal Loewner equation · Loewner hulls are compact hulls · Unswallowed domain equals the forward-extension domain · Reflection of a Loewner forward solution · Restriction of a Loewner forward solution · Chosen admissible Loewner duration · Chosen Loewner forward solution · Time shift of a Loewner forward solution

DefinitionRestriction of a Loewner forward solution#✓fully proved

The restriction of a forward solution to [0, S], S ≤ T.

def LoewnerForwardSolution.restrict {W : ℝ → ℝ} {z : ℂ} {T : ℝ}
    (g : LoewnerForwardSolution W z T) {S : ℝ} (hST : S ≤ T) :
    LoewnerForwardSolution W z S where
  curve := g.curve
  initial := g.initial
  deriv := by
    intro t ht
    exact (g.deriv t ⟨ht.1, ht.2.trans hST⟩).mono (Icc_subset_Icc_right hST)
  upper := by
    intro t ht
    exact g.upper t ⟨ht.1, ht.2.trans hST⟩

Uses 2 · Used by 5

Statement usesForward solution of the Loewner equation · Chordal Loewner vector field

Used byMaximal solution of the chordal Loewner equation · Loewner map as a homeomorphism onto the half-plane · Inverse of the maximal Loewner map · Maximal Loewner maps solve the maximal Loewner equation · Loewner hulls are compact hulls

DefinitionReflection of a Loewner forward solution#✓fully proved

The reflected solution -conj g_t(z), a forward solution for the driving function -W.

StatMech.SLE.LoewnerForwardSolution.reflect · 20 lines

def LoewnerForwardSolution.reflect {W : ℝ → ℝ} {z : ℂ} {T : ℝ}
    (g : LoewnerForwardSolution W z T) :
    LoewnerForwardSolution (fun t ↦ -W t) (loewnerReflection z) T where
  curve := fun t ↦ loewnerReflection (g.curve t)
  initial := by simp [g.initial]
  deriv := by
    intro t ht
    have hconj : HasDerivWithinAt (fun s ↦ conj (g.curve s))
        (conj (loewnerField W t (g.curve t))) (Icc (0 : ℝ) T) t := by
      exact Complex.conjCLE.hasFDerivAt.comp_hasDerivWithinAt t (g.deriv t ht)
    have hreflect : HasDerivWithinAt
        (fun s ↦ loewnerReflection (g.curve s))
        (loewnerReflection (loewnerField W t (g.curve t))) (Icc (0 : ℝ) T) t := by
      exact hconj.neg
    simpa only [loewnerReflection_loewnerField] using hreflect
  upper := by
    intro t ht
    rw [mem_upperHalfPlane]
    simpa only [loewnerReflection_im] using
      mem_upperHalfPlane.mp (g.upper t ht)

Uses 3 · Used by 1

Statement usesForward solution of the Loewner equation · Chordal Loewner vector field · Reflection across the imaginary axis

Used byLoewner hulls are compact hulls

DefinitionTime shift of a Loewner forward solution#✓fully proved

The solution restarted at time s: u ↦ g_{s+u}(z), for the driving function u ↦ W(s + u).

StatMech.SLE.LoewnerForwardSolution.timeShift · 22 lines

def LoewnerForwardSolution.timeShift
    {W : ℝ → ℝ} {z : ℂ} {T : ℝ}
    (g : LoewnerForwardSolution W z T) (s : ℝ) (hs0 : 0 ≤ s) :
    LoewnerForwardSolution (fun u ↦ W (s + u)) (g.curve s) (T - s) where
  curve := fun u ↦ g.curve (s + u)
  initial := by simp
  deriv := by
    intro u hu
    have hmap : MapsTo (fun r : ℝ ↦ s + r) (Icc (0 : ℝ) (T - s)) (Icc 0 T) := by
      intro r hr
      change 0 ≤ s + r ∧ s + r ≤ T
      constructor <;> linarith [hr.1, hr.2]
    have hsu : s + u ∈ Icc (0 : ℝ) T := hmap hu
    have hinner : HasDerivWithinAt (fun r : ℝ ↦ s + r) 1
        (Icc (0 : ℝ) (T - s)) u := by
      exact ((hasDerivAt_id u).const_add s).hasDerivWithinAt
    have hd := (g.deriv (s + u) hsu).scomp u hinner hmap
    simp only [Function.comp_def, one_smul] at hd
    exact hd
  upper := by
    intro u hu
    exact g.upper (s + u) ⟨by linarith [hu.1], by linarith [hu.2]⟩

Uses 2 · Used by 3

Statement usesForward solution of the Loewner equation · Chordal Loewner vector field

Used byLoewner map as a homeomorphism onto the half-plane · Maximal Loewner maps solve the maximal Loewner equation · Loewner hulls are compact hulls

DefinitionConcatenated curve of two Loewner solutions#✓fully proved

The concatenation of g on [0, S] with a solution h started from g_S(z) at time S.

noncomputable def LoewnerForwardSolution.appendCurve
    {W : ℝ → ℝ} {z : ℂ} {S T : ℝ}
    (g : LoewnerForwardSolution W z S)
    (h : LoewnerForwardSolution (fun u ↦ W (S + u)) (g.curve S) T) :
    ℝ → ℂ := fun t ↦ if t ≤ S then g.curve t else h.curve (t - S)

Uses 1 · Used by 4

Statement usesForward solution of the Loewner equation

Used byConcatenation of Loewner forward solutions · Loewner map as a homeomorphism onto the half-plane · Inverse of the maximal Loewner map · Maximal Loewner maps solve the maximal Loewner equation

DefinitionConcatenation of Loewner forward solutions#✓fully proved

The concatenation of two forward solutions, a forward solution on [0, S + T].

StatMech.SLE.LoewnerForwardSolution.append · 120 lines

noncomputable def LoewnerForwardSolution.append
    {W : ℝ → ℝ} {z : ℂ} {S T : ℝ}
    (g : LoewnerForwardSolution W z S)
    (h : LoewnerForwardSolution (fun u ↦ W (S + u)) (g.curve S) T)
    (hS : 0 ≤ S) (hT : 0 ≤ T) :
    LoewnerForwardSolution W z (S + T) where
  curve := g.appendCurve h
  initial := by simp [LoewnerForwardSolution.appendCurve, hS, g.initial]
  deriv := by
    intro t ht
    by_cases hleft : t < S
    · have htS : t ∈ Icc (0 : ℝ) S := ⟨ht.1, hleft.le⟩
      have hlocal : Icc (0 : ℝ) S ∈ 𝓝[Icc (0 : ℝ) (S + T)] t := by
        filter_upwards [self_mem_nhdsWithin,
          mem_nhdsWithin_of_mem_nhds (Iic_mem_nhds hleft)] with x hx hxs
        exact ⟨hx.1, hxs⟩
      have hd := (g.deriv t htS).mono_of_mem_nhdsWithin hlocal
      have happ : (g.appendCurve h) t = g.curve t := by
        simp [LoewnerForwardSolution.appendCurve, hleft.le]
      rw [happ]
      apply hd.congr_of_eventuallyEq_of_mem _ ht
      filter_upwards [mem_nhdsWithin_of_mem_nhds (Iic_mem_nhds hleft)] with x hx
      change x ≤ S at hx
      simp [LoewnerForwardSolution.appendCurve, hx]
    · by_cases hright : S < t
      · have hsub : t - S ∈ Icc (0 : ℝ) T := ⟨by linarith, by linarith [ht.2]⟩
        let k : ℝ → ℂ := fun x ↦ h.curve (x - S)
        have hmap : MapsTo (fun x : ℝ ↦ x - S) (Icc S (S + T)) (Icc 0 T) := by
          intro x hx
          change 0 ≤ x - S ∧ x - S ≤ T
          constructor <;> linarith [hx.1, hx.2]
        have hinner : HasDerivWithinAt (fun x : ℝ ↦ x - S) 1
            (Icc S (S + T)) t := by
          exact ((hasDerivAt_id t).sub_const S).hasDerivWithinAt
        have hk : HasDerivWithinAt k
            (loewnerField W t (k t)) (Icc S (S + T)) t := by
          have hraw := (h.deriv (t - S) hsub).scomp t hinner hmap
          convert hraw using 1
          · rfl
          simp only [one_smul]
          change loewnerField W t (h.curve (t - S)) =
            loewnerField W (S + (t - S)) (h.curve (t - S))
          rw [show S + (t - S) = t by ring]
        have hlocal : Icc S (S + T) ∈ 𝓝[Icc (0 : ℝ) (S + T)] t := by
          filter_upwards [self_mem_nhdsWithin,
            mem_nhdsWithin_of_mem_nhds (Ici_mem_nhds hright)] with x hx hxs
          exact ⟨hxs, hx.2⟩
        have hk' := hk.mono_of_mem_nhdsWithin hlocal
        have happ : (g.appendCurve h) t = k t := by
          simp [LoewnerForwardSolution.appendCurve, k, not_le.mpr hright]
        rw [happ]
        apply hk'.congr_of_eventuallyEq_of_mem _ ht
        filter_upwards [mem_nhdsWithin_of_mem_nhds (Ici_mem_nhds hright)] with x hx
        change S ≤ x at hx
        rcases hx.eq_or_lt with rfl | hxlt
        · simp [LoewnerForwardSolution.appendCurve, k, h.initial]
        · simp [LoewnerForwardSolution.appendCurve, k, not_le.mpr hxlt]
      · have hts : t = S := le_antisymm (not_lt.mp hright) (not_lt.mp hleft)
        subst t
        let k : ℝ → ℂ := fun x ↦ h.curve (x - S)
        have hmap : MapsTo (fun x : ℝ ↦ x - S) (Icc S (S + T)) (Icc 0 T) := by
          intro x hx
          change 0 ≤ x - S ∧ x - S ≤ T
          constructor <;> linarith [hx.1, hx.2]
        have hinner : HasDerivWithinAt (fun x : ℝ ↦ x - S) 1
            (Icc S (S + T)) S := by
          simpa using ((hasDerivAt_id S).sub_const S).hasDerivWithinAt
        have hk : HasDerivWithinAt k
            (loewnerField W S (k S)) (Icc S (S + T)) S := by
          have hh := h.deriv 0 ⟨le_rfl, hT⟩
          have hraw := hh.scomp_of_eq S hinner hmap (by ring : (0 : ℝ) = S - S)
          convert hraw using 1
          · rfl
          · simp [k]
        have hkvalue : k S = g.curve S := by simp [k, h.initial]
        have happLeft : EqOn (g.appendCurve h) g.curve (Icc (0 : ℝ) S) := by
          intro x hx
          simp [LoewnerForwardSolution.appendCurve, hx.2]
        have happRight : EqOn (g.appendCurve h) k (Icc S (S + T)) := by
          intro x hx
          rcases hx.1.eq_or_lt with rfl | hxlt
          · simp [LoewnerForwardSolution.appendCurve, k, h.initial]
          · simp [LoewnerForwardSolution.appendCurve, k, not_le.mpr hxlt]
        have hdl : HasDerivWithinAt (g.appendCurve h)
            (loewnerField W S ((g.appendCurve h) S)) (Icc (0 : ℝ) S) S := by
          have happS : (g.appendCurve h) S = g.curve S :=
            happLeft ⟨hS, le_rfl⟩
          rw [happS]
          exact (g.deriv S ⟨hS, le_rfl⟩).congr happLeft happS
        have hdr : HasDerivWithinAt (g.appendCurve h)
            (loewnerField W S ((g.appendCurve h) S)) (Icc S (S + T)) S := by
          have hk' : HasDerivWithinAt k
              (loewnerField W S (g.curve S)) (Icc S (S + T)) S := by
            rwa [hkvalue] at hk
          have happS : (g.appendCurve h) S = g.curve S := by
            simp [LoewnerForwardSolution.appendCurve]
          rw [happS]
          exact hk'.congr happRight (happRight ⟨le_rfl, by linarith⟩)
        have hdu := hdl.union hdr
        have hsets : Icc (0 : ℝ) S ∪ Icc S (S + T) = Icc 0 (S + T) := by
          ext x
          change ((0 ≤ x ∧ x ≤ S) ∨ (S ≤ x ∧ x ≤ S + T)) ↔
            (0 ≤ x ∧ x ≤ S + T)
          constructor
          · intro hx
            rcases hx with hx | hx
            · constructor <;> linarith [hx.1, hx.2, hT]
            · constructor <;> linarith [hx.1, hx.2, hS]
          · intro hx
            by_cases hxs : x ≤ S
            · exact Or.inl ⟨hx.1, hxs⟩
            · exact Or.inr ⟨le_of_not_ge hxs, hx.2⟩
        rwa [hsets] at hdu
  upper := by
    intro t ht
    by_cases hts : t ≤ S
    · simp only [LoewnerForwardSolution.appendCurve, ite_eq_left hts]
      exact g.upper t ⟨ht.1, hts⟩
    · simp only [LoewnerForwardSolution.appendCurve, ite_eq_right hts]
      exact h.upper (t - S) ⟨by linarith, by linarith [ht.2]⟩

Uses 3 · Used by 4

Statement usesForward solution of the Loewner equation · Concatenated curve of two Loewner solutions · Chordal Loewner vector field

Used byLoewner map as a homeomorphism onto the half-plane · Inverse of the maximal Loewner map · Maximal Loewner maps solve the maximal Loewner equation · Loewner hulls are compact hulls

DefinitionAdmissible duration for the Loewner equation#✓fully proved

T > 0 and there is a forward solution from z on [0, T].

def IsLoewnerAdmissibleDuration (W : ℝ → ℝ) (z : ℂ) (T : ℝ) : Prop :=
  0 < T ∧ Nonempty (LoewnerForwardSolution W z T)

Uses 1 · Used by 9

Statement usesForward solution of the Loewner equation

Used byLifetime of a point under the Loewner flow · Maximal solution of the chordal Loewner equation · Loewner map as a homeomorphism onto the half-plane · Inverse of the maximal Loewner map · Maximal Loewner maps solve the maximal Loewner equation · Loewner hulls are compact hulls · Unswallowed domain equals the forward-extension domain · Chosen admissible Loewner duration · Chosen Loewner forward solution

DefinitionLifetime of a point under the Loewner flow#✓fully proved

The lifetime T_z ∈ [0, ∞] of z: the supremum of admissible durations.

noncomputable def loewnerLifetime (W : ℝ → ℝ) (z : ℂ) : ENNReal :=
  ⨆ T : {T : ℝ // IsLoewnerAdmissibleDuration W z T}, ENNReal.ofReal T.1

Uses 1 · Used by 9

Statement usesAdmissible duration for the Loewner equation

Used byTimes before the Loewner lifetime · Maximal solution of the chordal Loewner equation · Loewner map as a homeomorphism onto the half-plane · Inverse of the maximal Loewner map · Maximal Loewner maps solve the maximal Loewner equation · Loewner hulls are compact hulls · Unswallowed domain equals the forward-extension domain · Chosen admissible Loewner duration · Chosen Loewner forward solution

DefinitionTimes before the Loewner lifetime#✓fully proved

0 ≤ t < T_z.

def IsBeforeLoewnerLifetime (W : ℝ → ℝ) (z : ℂ) (t : ℝ) : Prop :=
  0 ≤ t ∧ ENNReal.ofReal t < loewnerLifetime W z

Uses 1 · Used by 10

Statement usesLifetime of a point under the Loewner flow

Used byMaximal Loewner trajectory · Maximal solution of the chordal Loewner equation · Loewner map as a homeomorphism onto the half-plane · Inverse of the maximal Loewner map · Maximal Loewner maps solve the maximal Loewner equation · Loewner hulls are compact hulls · Unswallowed domain of the Loewner flow · Unswallowed domain equals the forward-extension domain · Chosen admissible Loewner duration · Chosen Loewner forward solution

DefinitionChosen admissible Loewner duration#✓fully proved

A chosen admissible duration exceeding t, for t before the lifetime.

noncomputable def selectedLoewnerDuration {W : ℝ → ℝ} {z : ℂ} {t : ℝ}
    (ht : IsBeforeLoewnerLifetime W z t) : ℝ :=
  Classical.choose (exists_admissibleDuration_gt_of_ofReal_lt_lifetime ht.2)

Uses 4 · Used by 7

Statement usesTimes before the Loewner lifetime · Admissible duration for the Loewner equation · Forward solution of the Loewner equation · Lifetime of a point under the Loewner flow

Used byMaximal Loewner trajectory · Maximal solution of the chordal Loewner equation · Loewner map as a homeomorphism onto the half-plane · Inverse of the maximal Loewner map · Maximal Loewner maps solve the maximal Loewner equation · Loewner hulls are compact hulls · Chosen Loewner forward solution

DefinitionChosen Loewner forward solution#✓fully proved

A chosen forward solution on [0, selectedLoewnerDuration ht].

noncomputable def selectedLoewnerSolution {W : ℝ → ℝ} {z : ℂ} {t : ℝ}
    (ht : IsBeforeLoewnerLifetime W z t) :
    LoewnerForwardSolution W z (selectedLoewnerDuration ht) :=
  Classical.choice (selectedLoewnerDuration_spec ht).1.2

Uses 5 · Used by 6

Statement usesTimes before the Loewner lifetime · Admissible duration for the Loewner equation · Forward solution of the Loewner equation · Lifetime of a point under the Loewner flow · Chosen admissible Loewner duration

Used byMaximal Loewner trajectory · Maximal solution of the chordal Loewner equation · Loewner map as a homeomorphism onto the half-plane · Inverse of the maximal Loewner map · Maximal Loewner maps solve the maximal Loewner equation · Loewner hulls are compact hulls

DefinitionMaximal Loewner trajectory#✓fully proved

The maximal solution t ↦ g_t(z) for 0 ≤ t < T_z (independent of choices by uniqueness); it is z outside [0, T_z).

noncomputable def loewnerMaximalCurve (W : ℝ → ℝ) (z : ℂ) (t : ℝ) : ℂ :=
  by
    classical
    exact if ht : IsBeforeLoewnerLifetime W z t then
      (selectedLoewnerSolution ht).curve t else z

Uses 4 · Used by 6

Statement usesTimes before the Loewner lifetime · Forward solution of the Loewner equation · Chosen admissible Loewner duration · Chosen Loewner forward solution

Used byMaximal solution of the chordal Loewner equation · Maximal Loewner maps · Loewner map as a homeomorphism onto the half-plane · Inverse of the maximal Loewner map · Maximal Loewner maps solve the maximal Loewner equation · Loewner hulls are compact hulls

TheoremMaximal solution of the chordal Loewner equation#✓fully proved

For continuous W and z ∈ ℍ, the lifetime T_z is positive, g_0(z) = z, g_t(z) ∈ ℍ for 0 ≤ t < T_z, the equation holds at t = 0 from the right and at every 0 < t < T_z (Lawler 2005, Chapter 4).

theorem loewner_maximal_forward_exists {W : ℝ → ℝ} (hW : Continuous W) {z : ℂ}
    (hz : 0 < z.im) :
    0 < loewnerLifetime W z ∧
      loewnerMaximalCurve W z 0 = z ∧
      (∀ t, IsBeforeLoewnerLifetime W z t →
        loewnerMaximalCurve W z t ∈ upperHalfPlaneSet) ∧
      HasDerivWithinAt (loewnerMaximalCurve W z)
        (loewnerField W 0 (loewnerMaximalCurve W z 0)) (Ici (0 : ℝ)) 0 ∧
      ∀ t, 0 < t → ENNReal.ofReal t < loewnerLifetime W z →
        HasDerivAt (loewnerMaximalCurve W z)
          (loewnerField W t (loewnerMaximalCurve W z t)) t

Uses 11

Statement usesTimes before the Loewner lifetime · Chordal Loewner vector field · Lifetime of a point under the Loewner flow · Maximal Loewner trajectory

Proof usesAdmissible duration for the Loewner equation · Forward solution of the Loewner equation · Restriction of a Loewner forward solution · Closed half-plane above a horizontal line · Local existence for the chordal Loewner equation · Chosen admissible Loewner duration · Chosen Loewner forward solution

DefinitionUnswallowed domain of the Loewner flow#✓fully proved

The domain H_t = {z ∈ ℍ : t < T_z} of points not swallowed by time t.

def loewnerUnswallowedDomain (W : ℝ → ℝ) (t : ℝ) : Set ℂ :=
  {z | z ∈ upperHalfPlaneSet ∧ IsBeforeLoewnerLifetime W z t}

Uses 1 · Used by 7

Statement usesTimes before the Loewner lifetime

Used byThe unswallowed domain is simply connected · Loewner map as a homeomorphism onto the half-plane · Inverse of the maximal Loewner map · Maximal Loewner maps solve the maximal Loewner equation · Loewner hull · Loewner hulls are compact hulls · Unswallowed domain equals the forward-extension domain

DefinitionMaximal Loewner maps#✓fully proved

The Loewner map g_t(z), the maximal solution at time t.

noncomputable def loewnerMaximalMaps (W : ℝ → ℝ) (t : ℝ) (z : ℂ) : ℂ :=
  loewnerMaximalCurve W z t

Uses 1 · Used by 4

Statement usesMaximal Loewner trajectory

Used byLoewner map as a homeomorphism onto the half-plane · Inverse of the maximal Loewner map · Maximal Loewner maps solve the maximal Loewner equation · Loewner hulls are compact hulls

DefinitionInverse of the maximal Loewner map#✓fully proved

The inverse g_t⁻¹ : ℍ → H_t (0 outside ℍ).

noncomputable def loewnerMaximalMapsInverse
    {W : ℝ → ℝ} (hW : Continuous W) {t : ℝ} (ht : 0 ≤ t) (y : ℂ) : ℂ := by
  classical
  exact if hy : y ∈ upperHalfPlaneSet then
      Classical.choose (loewnerMaximalMaps_surjOn_upperHalfPlane hW ht hy)
    else 0

Uses 16 · Used by 1

Statement usesTimes before the Loewner lifetime · Admissible duration for the Loewner equation · Forward solution of the Loewner equation · Concatenation of Loewner forward solutions · Concatenated curve of two Loewner solutions · Restriction of a Loewner forward solution · Chordal Loewner vector field · Lifetime of a point under the Loewner flow · Maximal Loewner trajectory · Maximal Loewner maps · Closed half-plane above a horizontal line · Unswallowed domain of the Loewner flow · Local existence for the chordal Loewner equation · Lipschitz Picard–Lindelöf flow confined to a ball · Chosen admissible Loewner duration · Chosen Loewner forward solution

Used byLoewner map as a homeomorphism onto the half-plane

TheoremUnswallowed domain equals the forward-extension domain#✓fully proved

The lifetime-defined unswallowed domain is exactly the intrinsic forward-extension domain.

theorem loewnerUnswallowedDomain_eq_setOf_hasLoewnerForwardExtension
    {W : ℝ → ℝ} {t : ℝ} (ht : 0 ≤ t) :
    loewnerUnswallowedDomain W t = {z | HasLoewnerForwardExtension W z t}

Uses 7 · Used by 1

Statement usesForward extension of a Loewner trajectory · Unswallowed domain of the Loewner flow

Proof usesTimes before the Loewner lifetime · Admissible duration for the Loewner equation · Forward solution of the Loewner equation · Chordal Loewner vector field · Lifetime of a point under the Loewner flow

Used byMaximal Loewner maps solve the maximal Loewner equation

DefinitionLoewner map as a homeomorphism onto the half-plane#✓fully proved

g_t as a homeomorphism H_t ≃ₜ ℍ.

StatMech.SLE.loewnerMaximalMapsHomeomorph · 24 lines

noncomputable def loewnerMaximalMapsHomeomorph
    {W : ℝ → ℝ} (hW : Continuous W) {t : ℝ} (ht : 0 ≤ t) :
    loewnerUnswallowedDomain W t ≃ₜ upperHalfPlaneSet where
  toFun := MapsTo.restrict (loewnerMaximalMaps W t)
    (loewnerUnswallowedDomain W t) upperHalfPlaneSet
    (loewnerMaximalMaps_bijOn_upperHalfPlane hW ht).1
  invFun := MapsTo.restrict (loewnerMaximalMapsInverse hW ht)
    upperHalfPlaneSet (loewnerUnswallowedDomain W t)
    (fun _ hy ↦ loewnerMaximalMapsInverse_mem hW ht hy)
  left_inv := by
    intro x
    apply Subtype.ext
    exact (eq_loewnerMaximalMapsInverse_of_mapsTo hW ht x.2
      (loewnerMaximalMaps_mem_upperHalfPlane x.2) rfl).symm
  right_inv := by
    intro y
    apply Subtype.ext
    exact loewnerMaximalMaps_inverse hW ht y.2
  continuous_toFun :=
    (continuousOn_loewnerMaximalMaps hW ht).mapsToRestrict
      (loewnerMaximalMaps_bijOn_upperHalfPlane hW ht).1
  continuous_invFun :=
    (continuousOn_loewnerMaximalMapsInverse hW ht).mapsToRestrict
      (fun _ hy ↦ loewnerMaximalMapsInverse_mem hW ht hy)

Uses 18 · Used by 1

Statement usesTimes before the Loewner lifetime · Admissible duration for the Loewner equation · Forward solution of the Loewner equation · Concatenation of Loewner forward solutions · Concatenated curve of two Loewner solutions · Restriction of a Loewner forward solution · Time shift of a Loewner forward solution · Chordal Loewner vector field · Lifetime of a point under the Loewner flow · Maximal Loewner trajectory · Maximal Loewner maps · Inverse of the maximal Loewner map · Closed half-plane above a horizontal line · Unswallowed domain of the Loewner flow · Local existence for the chordal Loewner equation · Lipschitz Picard–Lindelöf flow confined to a ball · Chosen admissible Loewner duration · Chosen Loewner forward solution

Used byThe unswallowed domain is simply connected

TheoremThe unswallowed domain is simply connected#✓fully proved

The unswallowed domain is simply connected.

theorem isSimplyConnected_loewnerUnswallowedDomain
    {W : ℝ → ℝ} (hW : Continuous W) {t : ℝ} (ht : 0 ≤ t) :
    IsSimplyConnected (loewnerUnswallowedDomain W t)

Uses 3 · Used by 1

Statement usesUnswallowed domain of the Loewner flow

Proof usesThe upper half-plane is simply connected · Loewner map as a homeomorphism onto the half-plane

Used byLoewner hulls are compact hulls

TheoremMaximal Loewner maps solve the maximal Loewner equation#✓fully proved

The canonical maximal family has the exact lifetime domains and conformal Loewner maps.

theorem loewnerMaximalMaps_satisfiesMaximalLoewnerEquation
    {W : ℝ → ℝ} (hW : Continuous W) :
    SatisfiesMaximalLoewnerEquation W (loewnerUnswallowedDomain W)
      (loewnerMaximalMaps W)

Uses 21

Statement usesMaximal chordal Loewner evolution · Maximal Loewner maps · Unswallowed domain of the Loewner flow

Proof usesForward extension of a Loewner trajectory · Times before the Loewner lifetime · Admissible duration for the Loewner equation · Solution of the Loewner equation at a time · Forward solution of the Loewner equation · Concatenation of Loewner forward solutions · Concatenated curve of two Loewner solutions · Restriction of a Loewner forward solution · Time shift of a Loewner forward solution · Chordal Loewner vector field · Lifetime of a point under the Loewner flow · Maximal Loewner trajectory · Closed half-plane above a horizontal line · Unswallowed domain equals the forward-extension domain · Local existence for the chordal Loewner equation · Lipschitz Picard–Lindelöf flow confined to a ball · Chosen admissible Loewner duration · Chosen Loewner forward solution

DefinitionLoewner hull#✓fully proved

The Loewner hull K_t = ℍ \ H_t of points swallowed by time t.

def loewnerSwallowedSet (W : ℝ → ℝ) (t : ℝ) : Set ℂ :=
  upperHalfPlaneSet \ loewnerUnswallowedDomain W t

Uses 1 · Used by 1

Statement usesUnswallowed domain of the Loewner flow

Used byLoewner hulls are compact hulls

TheoremLoewner hulls are compact hulls#✓fully proved

For continuous W and t ≥ 0, the Loewner hull K_t is a compact ℍ-hull (Lawler 2005, Chapter 4; the capacity normalization is not proved).

theorem loewnerSwallowedSet_isCompactHull
    {W : ℝ → ℝ} (hW : Continuous W) {t : ℝ} (ht : 0 ≤ t) :
    IsCompactHull (loewnerSwallowedSet W t)

Uses 23

Statement usesCompact hull in the upper half-plane · Loewner hull

Proof usesTimes before the Loewner lifetime · Admissible duration for the Loewner equation · Forward solution of the Loewner equation · Concatenation of Loewner forward solutions · Reflection of a Loewner forward solution · Restriction of a Loewner forward solution · Time shift of a Loewner forward solution · The unswallowed domain is simply connected · Chordal Loewner vector field · Lifetime of a point under the Loewner flow · Maximal Loewner trajectory · Maximal Loewner maps · Reflection across the imaginary axis · Closed half-plane above a horizontal line · Unswallowed domain of the Loewner flow · Local existence for the chordal Loewner equation · Picard–Lindelöf theorem with solutions confined to a ball · Lipschitz Picard–Lindelöf flow confined to a ball · Positivity persists under a nonnegative derivative · Chosen admissible Loewner duration · Chosen Loewner forward solution

23 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.