Elementary properties of Loewner solutions and of half-plane capacity

DefinitionReflection across the imaginary axis#✓fully proved

The reflection z ↦ -z̄ across the imaginary axis.

def loewnerReflection (z : ℂ) : ℂ := -conj z

Used by 2

Used byLoewner hulls are compact hulls · Reflection of a Loewner forward solution

TheoremAdditivity of half-plane capacity under composition#✓fully proved

Half-plane capacity is additive under composition: hcap(f ∘ g) = hcap(f) + hcap(g).

theorem hasHalfPlaneCapacity_comp {f g : ℂ → ℂ} {a b : ℝ}
    (hf : HasHalfPlaneCapacity f a) (hg : HasHalfPlaneCapacity g b) :
    HasHalfPlaneCapacity (g ∘ f) (a + b)

Uses 1

Statement usesHydrodynamic normalization with half-plane capacity

DefinitionHalf-plane capacity rate of a Loewner family#✓fully proved

The family g_t has half-plane capacity a t for every t ≥ 0.

def HasCapacityRate (g : ℝ → ℂ → ℂ) (a : ℝ) : Prop :=
  ∀ t ∈ Set.Ici (0 : ℝ), HasHalfPlaneCapacity (g t) (a * t)

Uses 1

Statement usesHydrodynamic normalization with half-plane capacity

DefinitionIncreasing family of compact hulls#✓fully proved

An increasing family (K_t) of compact ℍ-hulls.

def MonotoneHullFamily (K : ℝ → Set ℂ) : Prop :=
  (∀ t, IsCompactHull (K t)) ∧ Monotone K

Uses 1

Statement usesCompact hull in the upper half-plane

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.