Basic objects of the chordal Loewner equation

DefinitionClosed upper half-plane#✓fully proved

The closed upper half-plane {z : 0 ≤ Im z}.

def closedUpperHalfPlane : Set ℂ := {z : ℂ | 0 ≤ z.im}

DefinitionReal axis in the complex plane#✓fully proved

The real axis {z : Im z = 0} in ℂ.

def realLine : Set ℂ := {z : ℂ | z.im = 0}

StructureCompact hull in the upper half-plane#✓fully proved

A compact ℍ-hull: a bounded subset K of ℍ, relatively closed in ℍ, whose complement ℍ \ K is open and simply connected.

structure IsCompactHull (K : Set ℂ) : Prop where
  subset : K ⊆ upperHalfPlaneSet
  bounded : Bornology.IsBounded K
  relClosed : ∃ C : Set ℂ, IsClosed C ∧ K = C ∩ upperHalfPlaneSet
  complement_open : IsOpen (upperHalfPlaneSet \ K)
  complement_simplyConnected : IsSimplyConnected (upperHalfPlaneSet \ K)

Used by 3

Used byComplement of a compact hull is connected · Increasing family of compact hulls · Loewner hulls are compact hulls

LemmaComplement of a compact hull is connected#✓fully proved

The complement of a compact ℍ-hull is connected.

lemma IsCompactHull.complement_connected {K : Set ℂ} (hK : IsCompactHull K) :
    IsConnected (upperHalfPlaneSet \ K)

Uses 1

Statement usesCompact hull in the upper half-plane

LemmaThe upper half-plane is simply connected#✓fully proved

The complex upper half-plane is simply connected.

lemma isSimplyConnected_upperHalfPlane : IsSimplyConnected upperHalfPlaneSet

Used by 1

Used byThe unswallowed domain is simply connected

DefinitionHydrodynamic normalization with half-plane capacity#✓fully proved

g is hydrodynamically normalized at infinity with half-plane capacity a: g(z) - z → 0 and z (g(z) - z) → a as z → ∞, i.e. g(z) = z + a/z + o(1/z).

def HasHalfPlaneCapacity (g : ℂ → ℂ) (a : ℝ) : Prop :=
  Tendsto (fun z => g z - z) (cocompact ℂ) (𝓝 0) ∧
    Tendsto (fun z => z * (g z - z)) (cocompact ℂ) (𝓝 (a : ℂ))

Used by 2

Used byHalf-plane capacity rate of a Loewner family · Additivity of half-plane capacity under composition

DefinitionChordal Loewner vector field#✓fully proved

The chordal Loewner vector field w ↦ 2 / (w - W_t) at time t.

noncomputable def loewnerField (W : ℝ → ℝ) (t : ℝ) (w : ℂ) : ℂ := 2 / (w - (W t : ℂ))

Used by 17

Used byForward extension of a Loewner trajectory · Solution of the Loewner equation at a time · Solution of the Loewner equation on a set of times · Maximal chordal Loewner evolution · Local existence for the chordal Loewner equation · Local existence and uniqueness for the chordal Loewner equation · Concatenation of Loewner forward solutions · Forward solution of the Loewner equation · 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 · Time shift of a Loewner forward solution

DefinitionSolution of the Loewner equation at a time#✓fully proved

t ↦ g_t(z) satisfies the Loewner equation ∂_t g_t(z) = 2 / (g_t(z) - W_t) at time t.

def IsLoewnerSolutionAt (W : ℝ → ℝ) (g : ℝ → ℂ → ℂ) (z : ℂ) (t : ℝ) : Prop :=
  HasDerivAt (fun s => g s z) (loewnerField W t (g t z)) t

Uses 1 · Used by 3

Statement usesChordal Loewner vector field

Used byLoewner equation without domain restriction · Maximal chordal Loewner evolution · Maximal Loewner maps solve the maximal Loewner equation

DefinitionSolution of the Loewner equation on a set of times#✓fully proved

t ↦ g_t(z) satisfies the Loewner equation on s (derivatives within s).

def IsLoewnerSolutionOn (W : ℝ → ℝ) (g : ℝ → ℂ → ℂ) (z : ℂ) (s : Set ℝ) : Prop :=
  ∀ t ∈ s, HasDerivWithinAt (fun u => g u z) (loewnerField W t (g t z)) s t

Uses 1

Statement usesChordal Loewner vector field

DefinitionForward extension of a Loewner trajectory#✓fully proved

The Loewner trajectory from z extends in ℍ beyond time t. This is the intrinsic maximal-lifetime condition used to determine the unswallowed domain.

def HasLoewnerForwardExtension (W : ℝ → ℝ) (z : ℂ) (t : ℝ) : Prop :=
  z ∈ upperHalfPlaneSet ∧ ∃ T, t < T ∧ ∃ γ : ℝ → ℂ,
    γ 0 = z ∧
      (∀ s ∈ Set.Icc (0 : ℝ) T,
        HasDerivWithinAt γ (loewnerField W s (γ s)) (Set.Icc (0 : ℝ) T) s) ∧
      ∀ s ∈ Set.Icc (0 : ℝ) T, γ s ∈ upperHalfPlaneSet

Uses 1 · Used by 3

Statement usesChordal Loewner vector field

Used byMaximal chordal Loewner evolution · Maximal Loewner maps solve the maximal Loewner equation · Unswallowed domain equals the forward-extension domain

DefinitionLoewner equation without domain restriction#✓fully proved

g_0 = id and t ↦ g_t(z) solves the Loewner equation for every z ∈ ℂ and every t ≥ 0, with no domain restriction (compare SatisfiesMaximalLoewnerEquation, where z ranges over the unswallowed domain D_t).

def SatisfiesLoewnerEquation (W : ℝ → ℝ) (g : ℝ → ℂ → ℂ) : Prop :=
  (∀ z, g 0 z = z) ∧ ∀ z, ∀ t ∈ Set.Ici (0 : ℝ), IsLoewnerSolutionAt W g z t

Uses 1

Statement usesSolution of the Loewner equation at a time

DefinitionMaximal chordal Loewner evolution#✓fully proved

The maximal chordal Loewner evolution with domains D_t. The domains are exactly the points whose trajectories extend beyond t, and g_t : D_t → ℍ is a conformal bijection.

def SatisfiesMaximalLoewnerEquation
    (W : ℝ → ℝ) (D : ℝ → Set ℂ) (g : ℝ → ℂ → ℂ) : Prop :=
  D 0 = upperHalfPlaneSet ∧
    (∀ z ∈ D 0, g 0 z = z) ∧
    (∀ z ∈ D 0, HasDerivWithinAt (fun t => g t z)
      (loewnerField W 0 (g 0 z)) (Set.Ici (0 : ℝ)) 0) ∧
    (∀ t, 0 < t → ∀ z ∈ D t, IsLoewnerSolutionAt W g z t) ∧
    Continuous W ∧
    (∀ t, 0 ≤ t → D t = {z | HasLoewnerForwardExtension W z t}) ∧
    (∀ t, 0 ≤ t → Set.BijOn (g t) (D t) upperHalfPlaneSet) ∧
    ∀ t, 0 ≤ t → ∀ z ∈ D t, ConformalAt (g t) z

Uses 3 · Used by 2

Statement usesForward extension of a Loewner trajectory · Solution of the Loewner equation at a time · Chordal Loewner vector field

Used byChordal Schramm–Loewner evolution · Maximal Loewner maps solve the maximal Loewner equation

StructureStandard real Brownian motion#✓fully proved

A standard real Brownian motion indexed by ℝ (used for t ≥ 0): B_0 = 0 a.s., continuous paths a.s., Gaussian, with independent increments B_t - B_s ~ N(0, t - s).

See also Mathlib's ProbabilityTheory.IsPreBrownianReal (time ℝ≥0, finite-dimensional laws).

structure IsStandardBrownianMotion {Ω : Type*} [MeasurableSpace Ω]
    (B : ℝ → Ω → ℝ) (P : Measure Ω) : Prop where
  start : ∀ᵐ ω ∂P, B 0 ω = 0
  continuous_paths : ∀ᵐ ω ∂P, Continuous fun t => B t ω
  measurable : ∀ t, Measurable (B t)
  gaussian : IsGaussianProcess (fun t ω => B t ω) P
  increment_law : ∀ s t : ℝ, s ≤ t →
    HasLaw (fun ω => B t ω - B s ω) (gaussianReal 0 (t - s).toNNReal) P
  indep_increments : ∀ s t u v : ℝ, s ≤ t → t ≤ u → u ≤ v →
    IndepFun (fun ω => B t ω - B s ω) (fun ω => B v ω - B u ω) P

Used by 1

Used byChordal Schramm–Loewner evolution

DefinitionSLE driving function#✓fully proved

The SLE_κ driving function W_t = √κ B_t(ω).

noncomputable def sleDriving {Ω : Type*} (κ : ℝ) (B : ℝ → Ω → ℝ) (ω : Ω) : ℝ → ℝ :=
  fun t => Real.sqrt κ * B t ω

Used by 1

Used byChordal Schramm–Loewner evolution

StructureChordal Schramm–Loewner evolution#✓fully proved

(D, g) is chordal SLE_κ in ℍ from 0 to ∞: κ ≥ 0, B is a standard Brownian motion and almost surely g solves the maximal Loewner equation with driving function √κ B. This is a definition only; existence of SLE is not proved.

structure IsChordalSLE {Ω : Type*} [MeasurableSpace Ω]
    (κ : ℝ) (B : ℝ → Ω → ℝ) (P : Measure Ω)
    (D : Ω → ℝ → Set ℂ) (g : Ω → ℝ → ℂ → ℂ) : Prop where
  kappa_nonneg : 0 ≤ κ
  isBrownian : IsStandardBrownianMotion B P
  loewner : ∀ᵐ ω ∂P, SatisfiesMaximalLoewnerEquation
    (sleDriving κ B ω) (D ω) (g ω)

Uses 3

Statement usesStandard real Brownian motion · Maximal chordal Loewner evolution · SLE driving function

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.