Local existence and uniqueness for the chordal Loewner equation

TheoremPicard–Lindelöf theorem with solutions confined to a ball#✓fully proved

Picard–Lindelöf with the solution confined to closedBall x₀ a: a strengthening of Mathlib's IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt₀ by the bound α t ∈ closedBall x₀ a for all t.

theorem picard_exists_ball {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : Icc tmin tmax} {x₀ : E}
    {a L K : ℝ≥0} (hf : IsPicardLindelof f t₀ x₀ a 0 L K) :
    ∃ α : ℝ → E, α t₀ = x₀ ∧
      (∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t) ∧
      (∀ t, α t ∈ closedBall x₀ a)

Used by 2

Used byLocal existence for the chordal Loewner equation · Loewner hulls are compact hulls

TheoremLipschitz Picard–Lindelöf flow confined to a ball#✓fully proved

Picard–Lindelöf local flow, Lipschitz in the initial point, with every trajectory in closedBall x₀ a: a strengthening of Mathlib's IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith by the ball bound.

theorem picard_exists_ball_family_lipschitz
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : Icc tmin tmax} {x₀ : E}
    {a r L K : ℝ≥0} (hf : IsPicardLindelof f t₀ x₀ a r L K) :
    ∃ α : E → ℝ → E,
      (∀ x ∈ closedBall x₀ r,
        α x t₀ = x ∧
          (∀ t ∈ Icc tmin tmax,
            HasDerivWithinAt (α x) (f t (α x t)) (Icc tmin tmax) t) ∧
          (∀ t, α x t ∈ closedBall x₀ a)) ∧
      ∃ C : ℝ≥0, ∀ t ∈ Icc tmin tmax,
        LipschitzOnWith C (fun x ↦ α x t) (closedBall x₀ r)

Used by 4

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

TheoremLocal existence for the chordal Loewner equation#✓fully proved

For continuous W and Im z > 0 there are ε > 0 and g with g 0 = z, ġ(t) = 2 / (g(t) - W_t) on [0, ε] (one-sided derivatives at the endpoints), and g(t) ∈ ℍ on [0, ε] (Lawler 2005, Chapter 4).

theorem loewner_local_existence {W : ℝ → ℝ} (hW : Continuous W) {z : ℂ}
    (hz : 0 < z.im) :
    ∃ ε > (0 : ℝ), ∃ g : ℝ → ℂ, g 0 = z ∧
      (∀ t ∈ Icc (0 : ℝ) ε, HasDerivWithinAt g (loewnerField W t (g t)) (Icc (0 : ℝ) ε) t) ∧
      (∀ t ∈ Icc (0 : ℝ) ε, g t ∈ upperHalfPlaneSet)

Uses 3 · Used by 6

Statement usesChordal Loewner vector field

Proof usesClosed half-plane above a horizontal line · Picard–Lindelöf theorem with solutions confined to a ball

Used byLocal existence and uniqueness for the chordal 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

TheoremLocal existence and uniqueness for the chordal Loewner equation#✓fully proved

Local existence and uniqueness for the chordal Loewner equation: the solution from loewner_local_existence is the unique continuous solution on [0, ε] with right derivatives on [0, ε) that stays in ℍ.

theorem loewner_local_existsUnique {W : ℝ → ℝ} (hW : Continuous W) {z : ℂ}
    (hz : 0 < z.im) :
    ∃ ε > (0 : ℝ), ∃ g : ℝ → ℂ,
      (g 0 = z ∧
        (∀ t ∈ Icc (0 : ℝ) ε, HasDerivWithinAt g (loewnerField W t (g t)) (Icc (0 : ℝ) ε) t) ∧
        (∀ t ∈ Icc (0 : ℝ) ε, g t ∈ upperHalfPlaneSet)) ∧
      ∀ h : ℝ → ℂ, h 0 = z →
        ContinuousOn h (Icc 0 ε) →
        (∀ t ∈ Ico 0 ε, HasDerivWithinAt h (loewnerField W t (h t)) (Ici t) t) →
        (∀ t ∈ Icc 0 ε, h t ∈ upperHalfPlaneSet) →
        EqOn g h (Icc 0 ε)

Uses 3

Statement usesChordal Loewner vector field

Proof usesClosed half-plane above a horizontal line · Local existence for the chordal Loewner equation

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.