The Jordan curve theorem to Wolff's lemma…

TheoremThe Jordan curve theorem#

The complement of a Jordan curve in the plane has exactly two connected components: by TauCeti.IsJordanCurve.connectedComponentIn_eq_filledHull_sdiff_or_compl they are its inside filledHull C \ C and its unbounded outside (filledHull C)ᶜ.

TauCeti.IsJordanCurve.natCard_connectedComponents_compl_eq_two {C : Set ℂ}
  (hC : TauCeti.IsJordanCurve C) : Nat.card (ConnectedComponents ↑Cᶜ) = 2

Lean

Formalized in Tau Ceti as TauCeti.IsJordanCurve.natCard_connectedComponents_compl_eq_two.

Other forms

The Jordan curve theorem on the Riemann sphere. Formalized in Tau Ceti as TauCeti.IsJordanCurve.natCard_zerothHomotopy_compl_eq_two_onePoint.

TauCeti.IsJordanCurve.natCard_zerothHomotopy_compl_eq_two_onePoint {J : Set (OnePoint ℂ)}
  (hJ : TauCeti.IsJordanCurve J) : Nat.card (ZerothHomotopy ↑Jᶜ) = 2

Sources

• Tau Ceti documentation: TauCeti.IsJordanCurve.natCard_connectedComponents_compl_eq_two
• Source of TauCeti.IsJordanCurve.natCard_connectedComponents_compl_eq_two in TauCeti/Analysis/Complex/PlaneSeparation/Inside.lean

LeanTauCeti.IsJordanCurve.natCard_connectedComponents_compl_eq_two · TauCeti.IsJordanCurve.natCard_zerothHomotopy_compl_eq_two_onePoint

Uses 2 · Used by 2

Proof usesThe Jordan separation theorem · The Jordan–Brouwer separation theorem

Used byCarathéodory's theorem for the inside of a Jordan curve · Jordan index theorem (orientation sign dichotomy)

TheoremThe monodromy theorem#

Let h be a homotopy rel endpoints between two paths from z₀ to z₁ in ℂ, and suppose a germ at z₀ continues along every path h (t, ·) of the homotopy, all the continuations starting from that one germ. Then they all end at one and the same germ at z₁: the result of the continuation depends on the path only through its homotopy class.

This is the rel-endpoints case of TauCeti.monodromy_theorem_of_free_homotopy, whose homotopy is allowed to move the endpoints and whose conclusion is correspondingly a continuation along the path the terminal point sweeps out rather than a single germ at z₁.

TauCeti.monodromy_theorem.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E]
  [CompleteSpace E] {z₀ z₁ : ℂ} {p₀ p₁ : Path z₀ z₁} (h : p₀.Homotopy p₁)
  {f : ↑unitInterval → ↑unitInterval → ℂ → E}
  (hf :
    ∀ (t : ↑unitInterval), TauCeti.IsAnalyticContinuationAlong (f t) (fun x => h (t, x)) Set.univ)
  (hstart : ∀ (t : ↑unitInterval), f t 0 =ᶠ[nhds z₀] f 0 0) (t : ↑unitInterval) :
  f t 1 =ᶠ[nhds z₁] f 0 1

Lean

Formalized in Tau Ceti as TauCeti.monodromy_theorem.

Other forms

The monodromy theorem, in two-way form. Formalized in Tau Ceti as TauCeti.continuesInside_iff_exists_analyticOnNhd.

TauCeti.continuesInside_iff_exists_analyticOnNhd.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] [CompleteSpace E] {U : Set ℂ} {z₀ : ℂ} {f₀ : ℂ → E} (hUo : IsOpen U)
  (hUc : IsSimplyConnected U) (hz₀ : z₀ ∈ U) :
  TauCeti.ContinuesInside f₀ U z₀ ↔ ∃ F, AnalyticOnNhd ℂ F U ∧ F =ᶠ[nhds z₀] f₀

Sources

• Tau Ceti documentation: TauCeti.monodromy_theorem
• Source of TauCeti.monodromy_theorem in TauCeti/Analysis/Complex/Conformal/Monodromy.lean

LeanTauCeti.monodromy_theorem · TauCeti.continuesInside_iff_exists_analyticOnNhd

Uses 2

Proof usesThe monodromy theorem for a free homotopy of paths · The monodromy theorem for a simply connected domain

TheoremThe monodromy theorem for a free homotopy of paths#

Let h be a continuous map of the square, read as a family of paths h (t, ·) whose endpoints are allowed to move, and suppose a family of germs continues along each of those paths. If the initial germs — the germ of f t 0 at h (t, 0) — themselves continue along the initial edge t ↦ h (t, 0), then the terminal germs continue along the terminal edge t ↦ h (t, 1).

This is the monodromy theorem in the form the deck-group and covering-space consumers need: the continuation of a germ across a homotopy is itself a continuation, along the path the far endpoint sweeps out. Nothing is assumed rel endpoints; TauCeti.monodromy_theorem is the special case in which both edges are constant, where "continues along a constant path" degenerates to "carries one germ throughout".

TauCeti.monodromy_theorem_of_free_homotopy.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] [CompleteSpace E] {h : ↑unitInterval × ↑unitInterval → ℂ} (hh : Continuous h)
  {f : ↑unitInterval → ↑unitInterval → ℂ → E}
  (hf :
    ∀ (t : ↑unitInterval), TauCeti.IsAnalyticContinuationAlong (f t) (fun x => h (t, x)) Set.univ)
  (hstart : TauCeti.IsAnalyticContinuationAlong (fun t => f t 0) (fun t => h (t, 0)) Set.univ) :
  TauCeti.IsAnalyticContinuationAlong (fun t => f t 1) (fun t => h (t, 1)) Set.univ

Lean

Formalized in Tau Ceti as TauCeti.monodromy_theorem_of_free_homotopy.

Sources

• Tau Ceti documentation: TauCeti.monodromy_theorem_of_free_homotopy
• Source of TauCeti.monodromy_theorem_of_free_homotopy in TauCeti/Analysis/Complex/Conformal/Monodromy.lean

LeanTauCeti.monodromy_theorem_of_free_homotopy

Used by 1

Used byThe monodromy theorem

TheoremThe monodromy theorem for a simply connected domain#

A germ that continues along every path of a simply connected open set U issuing from z₀ is the germ at z₀ of a single function analytic on all of U.

So on a simply connected domain analytic continuation produces no new branches, and a "multi-valued analytic function" there is single-valued after all.

TauCeti.ContinuesInside.exists_analyticOnNhd.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] [CompleteSpace E] {U : Set ℂ} {z₀ : ℂ} {f₀ : ℂ → E} (hUo : IsOpen U)
  (hUc : IsSimplyConnected U) (hz₀ : z₀ ∈ U) (H : TauCeti.ContinuesInside f₀ U z₀) :
  ∃ F, AnalyticOnNhd ℂ F U ∧ F =ᶠ[nhds z₀] f₀

Informally uses

• The monodromy theorem

Lean

Formalized in Tau Ceti as TauCeti.ContinuesInside.exists_analyticOnNhd.

Sources

• Tau Ceti documentation: TauCeti.ContinuesInside.exists_analyticOnNhd
• Source of TauCeti.ContinuesInside.exists_analyticOnNhd in TauCeti/Analysis/Complex/Conformal/GlobalBranch.lean

LeanTauCeti.ContinuesInside.exists_analyticOnNhd

Used by 1

Used byThe monodromy theorem

TheoremMorera's theorem#

A continuous function with values in a complex Banach space, defined on an open set of ℂ and conservative there (its integrals over the boundaries of rectangles in the set vanish), is complex differentiable on that set.

TauCeti.morera.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
  {U : Set ℂ} {f : ℂ → E} (hU : IsOpen U) (hcont : ContinuousOn f U)
  (hcons : Complex.IsConservativeOn f U) : DifferentiableOn ℂ f U

Lean

Formalized in Tau Ceti as TauCeti.morera.

Sources

• Tau Ceti documentation: TauCeti.morera
• Source of TauCeti.morera in TauCeti/Analysis/Complex/Conformal/Morera.lean

LeanTauCeti.morera

TheoremPoincaré defect identity (norm form)#

The difference of the squared norms of the Moebius denominator and numerator factors is the product of the two hyperbolic defects: ‖1 - conj w * z‖ ^ 2 - ‖z - w‖ ^ 2 = (1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2).

TauCeti.norm_sq_one_sub_conj_mul_sub_norm_sq_sub (z w : ℂ) :
  ‖1 - (starRingEnd ℂ) w * z‖ ^ 2 - ‖z - w‖ ^ 2 = (1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2)

Lean

Formalized in Tau Ceti as TauCeti.norm_sq_one_sub_conj_mul_sub_norm_sq_sub.

Sources

• Tau Ceti documentation: TauCeti.norm_sq_one_sub_conj_mul_sub_norm_sq_sub
• Source of TauCeti.norm_sq_one_sub_conj_mul_sub_norm_sq_sub in TauCeti/Analysis/Complex/Conformal/PseudoHyperbolic.lean

LeanTauCeti.norm_sq_one_sub_conj_mul_sub_norm_sq_sub

Used by 1

Used bySchwarz–Pick, Lipschitz form

TheoremRouché's theorem for a disc, classical form#

If f and g are holomorphic on the closed disc closedBall c R and ‖f z - g z‖ < ‖f z‖ at every point z of the bounding circle, then f and g have the same number of zeros in ball c R, each counted with multiplicity.

This is the special case of TauCeti.rouche_symm obtained by discarding the nonnegative summand ‖g z‖ from the symmetric hypothesis.

TauCeti.rouche {f g : ℂ → ℂ} {c : ℂ} {R : ℝ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall c R))
  (hg : AnalyticOnNhd ℂ g (Metric.closedBall c R))
  (hs : ∀ z ∈ Metric.sphere c R, ‖f z - g z‖ < ‖f z‖) :
  ∑ᶠ (z : ℂ) (_ : z ∈ Metric.ball c R), analyticOrderNatAt f z =
    ∑ᶠ (z : ℂ) (_ : z ∈ Metric.ball c R), analyticOrderNatAt g z

Lean

Formalized in Tau Ceti as TauCeti.rouche.

Other forms

Rouché's theorem, in the additive phrasing of most textbooks. Formalized in Tau Ceti as TauCeti.rouche_add.

TauCeti.rouche_add {f g : ℂ → ℂ} {c : ℂ} {R : ℝ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall c R))
  (hg : AnalyticOnNhd ℂ g (Metric.closedBall c R)) (hs : ∀ z ∈ Metric.sphere c R, ‖g z‖ < ‖f z‖) :
  ∑ᶠ (z : ℂ) (_ : z ∈ Metric.ball c R), analyticOrderNatAt f z =
    ∑ᶠ (z : ℂ) (_ : z ∈ Metric.ball c R), analyticOrderNatAt (fun w => f w + g w) z

Rouché's theorem as a zero-detection principle, additive form. Formalized in Tau Ceti as TauCeti.rouche_add_exists_eq_zero_iff.

TauCeti.rouche_add_exists_eq_zero_iff {f g : ℂ → ℂ} {c : ℂ} {R : ℝ}
  (hf : AnalyticOnNhd ℂ f (Metric.closedBall c R)) (hg : AnalyticOnNhd ℂ g (Metric.closedBall c R))
  (hs : ∀ z ∈ Metric.sphere c R, ‖g z‖ < ‖f z‖) :
  (∃ z ∈ Metric.ball c R, f z = 0) ↔ ∃ z ∈ Metric.ball c R, f z + g z = 0

Rouché's theorem as a zero-detection principle, classical form. Formalized in Tau Ceti as TauCeti.rouche_exists_eq_zero_iff.

TauCeti.rouche_exists_eq_zero_iff {f g : ℂ → ℂ} {c : ℂ} {R : ℝ}
  (hf : AnalyticOnNhd ℂ f (Metric.closedBall c R)) (hg : AnalyticOnNhd ℂ g (Metric.closedBall c R))
  (hs : ∀ z ∈ Metric.sphere c R, ‖f z - g z‖ < ‖f z‖) :
  (∃ z ∈ Metric.ball c R, f z = 0) ↔ ∃ z ∈ Metric.ball c R, g z = 0

Rouché's theorem as a zero-detection principle, symmetric form. Formalized in Tau Ceti as TauCeti.rouche_symm_exists_eq_zero_iff.

TauCeti.rouche_symm_exists_eq_zero_iff {f g : ℂ → ℂ} {c : ℂ} {R : ℝ}
  (hf : AnalyticOnNhd ℂ f (Metric.closedBall c R)) (hg : AnalyticOnNhd ℂ g (Metric.closedBall c R))
  (hs : ∀ z ∈ Metric.sphere c R, ‖f z - g z‖ < ‖f z‖ + ‖g z‖) :
  (∃ z ∈ Metric.ball c R, f z = 0) ↔ ∃ z ∈ Metric.ball c R, g z = 0

Rouché's theorem as an equality of image winding numbers, classical form. Formalized in Tau Ceti as TauCeti.rouche_windingNumber_comp.

TauCeti.rouche_windingNumber_comp {f g : ℂ → ℂ} {γ : ℝ → ℂ} {a b : ℝ}
  (hγ : TauCeti.IsPiecewiseC1On γ a b) (hclosed : γ a = γ b)
  (hfa : ∀ t ∈ Set.uIcc a b, AnalyticAt ℂ f (γ t)) (hga : ∀ t ∈ Set.uIcc a b, AnalyticAt ℂ g (γ t))
  (hs : ∀ t ∈ Set.uIcc a b, ‖f (γ t) - g (γ t)‖ < ‖f (γ t)‖) :
  TauCeti.Contour.windingNumber (f ∘ γ) a b 0 = TauCeti.Contour.windingNumber (g ∘ γ) a b 0

Rouché's theorem as an equality of image winding numbers, additive form. Formalized in Tau Ceti as TauCeti.rouche_add_windingNumber_comp.

TauCeti.rouche_add_windingNumber_comp {f g : ℂ → ℂ} {γ : ℝ → ℂ} {a b : ℝ}
  (hγ : TauCeti.IsPiecewiseC1On γ a b) (hclosed : γ a = γ b)
  (hfa : ∀ t ∈ Set.uIcc a b, AnalyticAt ℂ f (γ t)) (hga : ∀ t ∈ Set.uIcc a b, AnalyticAt ℂ g (γ t))
  (hs : ∀ t ∈ Set.uIcc a b, ‖g (γ t)‖ < ‖f (γ t)‖) :
  TauCeti.Contour.windingNumber (f ∘ γ) a b 0 =
    TauCeti.Contour.windingNumber ((fun w => f w + g w) ∘ γ) a b 0

Rouché's theorem as an equality of image winding numbers, symmetric form — the "dog on a leash" statement. Formalized in Tau Ceti as TauCeti.rouche_symm_windingNumber_comp.

TauCeti.rouche_symm_windingNumber_comp {f g : ℂ → ℂ} {γ : ℝ → ℂ} {a b : ℝ}
  (hγ : TauCeti.IsPiecewiseC1On γ a b) (hclosed : γ a = γ b)
  (hfa : ∀ t ∈ Set.uIcc a b, AnalyticAt ℂ f (γ t)) (hga : ∀ t ∈ Set.uIcc a b, AnalyticAt ℂ g (γ t))
  (hs : ∀ t ∈ Set.uIcc a b, ‖f (γ t) - g (γ t)‖ < ‖f (γ t)‖ + ‖g (γ t)‖) :
  TauCeti.Contour.windingNumber (f ∘ γ) a b 0 = TauCeti.Contour.windingNumber (g ∘ γ) a b 0

Rouché's theorem for a null-homologous cycle, additive form. Formalized in Tau Ceti as TauCeti.rouche_add_nullHomologous.

TauCeti.rouche_add_nullHomologous {f g : ℂ → ℂ} {U : Set ℂ} {S : Finset ℂ} {γ : ℝ → ℂ} {a b : ℝ}
  (hU : IsOpen U) (hf : AnalyticOnNhd ℂ f U) (hg : AnalyticOnNhd ℂ g U)
  (hfS : ∀ z ∈ U, f z = 0 → z ∈ S) (hsumS : ∀ z ∈ U, f z + g z = 0 → z ∈ S)
  (hγ : TauCeti.IsPiecewiseC1On γ a b) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hclosed : γ a = γ b)
  (hnull : TauCeti.Contour.IsNullHomologous γ a b U)
  (hs : ∀ t ∈ Set.uIcc a b, ‖g (γ t)‖ < ‖f (γ t)‖) :
  ∑ z ∈ S, TauCeti.Contour.windingNumber γ a b z * ↑(analyticOrderNatAt f z) =
    ∑ z ∈ S, TauCeti.Contour.windingNumber γ a b z * ↑(analyticOrderNatAt (fun w => f w + g w) z)

Rouché's theorem for a null-homologous cycle, classical form. Formalized in Tau Ceti as TauCeti.rouche_nullHomologous.

TauCeti.rouche_nullHomologous {f g : ℂ → ℂ} {U : Set ℂ} {S : Finset ℂ} {γ : ℝ → ℂ} {a b : ℝ}
  (hU : IsOpen U) (hf : AnalyticOnNhd ℂ f U) (hg : AnalyticOnNhd ℂ g U)
  (hfS : ∀ z ∈ U, f z = 0 → z ∈ S) (hgS : ∀ z ∈ U, g z = 0 → z ∈ S)
  (hγ : TauCeti.IsPiecewiseC1On γ a b) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hclosed : γ a = γ b)
  (hnull : TauCeti.Contour.IsNullHomologous γ a b U)
  (hs : ∀ t ∈ Set.uIcc a b, ‖f (γ t) - g (γ t)‖ < ‖f (γ t)‖) :
  ∑ z ∈ S, TauCeti.Contour.windingNumber γ a b z * ↑(analyticOrderNatAt f z) =
    ∑ z ∈ S, TauCeti.Contour.windingNumber γ a b z * ↑(analyticOrderNatAt g z)

Rouché's theorem for a null-homologous cycle, holomorphic form. Formalized in Tau Ceti as TauCeti.rouche_symm_nullHomologous_of_analyticOnNhd.

TauCeti.rouche_symm_nullHomologous_of_analyticOnNhd {f g : ℂ → ℂ} {U : Set ℂ} {S : Finset ℂ}
  {γ : ℝ → ℂ} {a b : ℝ} (hU : IsOpen U) (hf : AnalyticOnNhd ℂ f U) (hg : AnalyticOnNhd ℂ g U)
  (hfS : ∀ z ∈ U, f z = 0 → z ∈ S) (hgS : ∀ z ∈ U, g z = 0 → z ∈ S)
  (hγ : TauCeti.IsPiecewiseC1On γ a b) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hclosed : γ a = γ b)
  (hnull : TauCeti.Contour.IsNullHomologous γ a b U)
  (hs : ∀ t ∈ Set.uIcc a b, ‖f (γ t) - g (γ t)‖ < ‖f (γ t)‖ + ‖g (γ t)‖) :
  ∑ z ∈ S, TauCeti.Contour.windingNumber γ a b z * ↑(analyticOrderNatAt f z) =
    ∑ z ∈ S, TauCeti.Contour.windingNumber γ a b z * ↑(analyticOrderNatAt g z)

Rouché's theorem for a null-homologous cycle, symmetric form (Estermann). Formalized in Tau Ceti as TauCeti.rouche_symm_nullHomologous.

TauCeti.rouche_symm_nullHomologous {f g : ℂ → ℂ} {U : Set ℂ} {S : Finset ℂ} {γ : ℝ → ℂ} {a b : ℝ}
  {ordf ordg : ℂ → ℤ} (hU : IsOpen U) (hfoff : ∀ z ∈ U, z ∉ S → AnalyticAt ℂ f z ∧ f z ≠ 0)
  (hgoff : ∀ z ∈ U, z ∉ S → AnalyticAt ℂ g z ∧ g z ≠ 0)
  (hfmero : ∀ s ∈ S, s ∈ U → MeromorphicAt f s) (hgmero : ∀ s ∈ S, s ∈ U → MeromorphicAt g s)
  (hford : ∀ s ∈ S, s ∈ U → meromorphicOrderAt f s = ↑(ordf s))
  (hgord : ∀ s ∈ S, s ∈ U → meromorphicOrderAt g s = ↑(ordg s)) (hγ : TauCeti.IsPiecewiseC1On γ a b)
  (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hclosed : γ a = γ b) (hγoff : ∀ t ∈ Set.uIcc a b, γ t ∉ ↑S)
  (hnull : TauCeti.Contour.IsNullHomologous γ a b U)
  (hs : ∀ t ∈ Set.uIcc a b, ‖f (γ t) - g (γ t)‖ < ‖f (γ t)‖ + ‖g (γ t)‖) :
  ∑ z ∈ S, TauCeti.Contour.windingNumber γ a b z * ↑(ordf z) =
    ∑ z ∈ S, TauCeti.Contour.windingNumber γ a b z * ↑(ordg z)

Rouché's theorem, symmetric form (Estermann). Formalized in Tau Ceti as TauCeti.rouche_symm.

TauCeti.rouche_symm {f g : ℂ → ℂ} {c : ℂ} {R : ℝ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall c R))
  (hg : AnalyticOnNhd ℂ g (Metric.closedBall c R))
  (hs : ∀ z ∈ Metric.sphere c R, ‖f z - g z‖ < ‖f z‖ + ‖g z‖) :
  ∑ᶠ (z : ℂ) (_ : z ∈ Metric.ball c R), analyticOrderNatAt f z =
    ∑ᶠ (z : ℂ) (_ : z ∈ Metric.ball c R), analyticOrderNatAt g z

Sources

• Tau Ceti documentation: TauCeti.rouche
• Source of TauCeti.rouche in TauCeti/Analysis/Complex/Conformal/Rouche.lean

LeanTauCeti.rouche · TauCeti.rouche_add · TauCeti.rouche_add_exists_eq_zero_iff · TauCeti.rouche_exists_eq_zero_iff · TauCeti.rouche_symm_exists_eq_zero_iff · TauCeti.rouche_windingNumber_comp · TauCeti.rouche_add_windingNumber_comp · TauCeti.rouche_symm_windingNumber_comp · TauCeti.rouche_add_nullHomologous · TauCeti.rouche_nullHomologous · TauCeti.rouche_symm_nullHomologous_of_analyticOnNhd · TauCeti.rouche_symm_nullHomologous · TauCeti.rouche_symm

Uses 3 · Used by 18

Statement usesGeneralized winding number (HW Def 2.1)

Proof usesCauchy–Goursat for a pole-free meromorphic function · The classical residue theorem for a null-homologous contour cycle

Used byAnalytic Belyi pairs are classified by finite covers of the thrice-punctured sphere · The superelliptic curve is the analytic Belyi pair of the torus triple · Carathéodory's continuity theorem, as a characterization · Hurwitz's theorem · The Riemann map of a Jordan domain extends to a homeomorphism of the closures · The Riemann mapping theorem · The Schwarz--Christoffel theorem for a bounded polygonal Jordan domain · The Schwarz--Christoffel theorem for an unbounded polygonal Jordan domain · The Schwarz--Christoffel formula · A degree-one map is a biholomorphism · TauCeti.ModularGroup.jBiholomorph · The degree of a finite-index map of compactified Fuchsian quotients is the index · Carathéodory's theorem for the inside of a Jordan curve · The component mapping theorem from one boundary sheet · The disc Schwarz--Christoffel theorem for an unbounded polygonal Jordan domain · The open mapping theorem · Uniqueness in the Riemann mapping theorem, up to a disc automorphism · The uniformization theorem

TheoremThe Schwarz--Christoffel formula#

Let f be holomorphic with nonvanishing derivative on the upper half-plane. Assume that away from the distinct real prevertices a i its boundary values run along affine lines with the upper half-plane on one side, and that each a i is carried to a vertex of one of four kinds: * a finite vertex: f opens the sector of angle (e i + 1) * π at f (a i), with boundary values on the two bounding rays, where -1 < e i < 1; * a vertex at infinity of opening β * π with 0 < β < 2, where e i = -β - 1: the inverted map b / (f - c) extends across a i with value 0, opens the sector of angle β * π there, and has its other boundary values on the two bounding rays; * a vertex at infinity between two parallel sides, where e i = -1: the exponential exp ((f - c) / b) extends across a i with value 0, injectively, with real boundary values and upper half-plane values above the axis; * a vertex at infinity of opening 2 * π, where e i = -3: f is continuous and injective on the closed upper half-disc about a i with a i removed, tends to infinity at a i, and far out the image of the open upper half-disc is the exterior of the closed half-strip {0 ≤ re ((w - c) / b), 0 ≤ im ((w - c) / b) ≤ π}.

Assume finally that z * f''(z) / f'(z) has a finite limit as z tends to infinity in the upper half-plane. Then throughout the upper half-plane

f z = (f'(z₀) / integrand(z₀)) * F z + f z₀,

where F is the normalized Schwarz--Christoffel primitive for the data a and e. So f is an affine image of F, and the two constants are read off from the value and derivative of f at the normalization point z₀.

TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_polygonal_boundary.{u_1} {ι : Type u_1}
  [Fintype ι] (a e : ι → ℝ) (ha : Function.Injective a) (z₀ : UpperHalfPlane) {f : ℂ → ℂ}
  (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet)
  (hfn : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, deriv f z ≠ 0)
  (hside :
    ∀ (x : ℝ),
      (∀ (i : ι), a i ≠ x) →
        ∃ r > 0,
          ∃ q b,
            b ≠ 0 ∧
              ContinuousOn f (Metric.ball (↑x) r ∩ {z | 0 ≤ z.im}) ∧
                Set.InjOn f (Metric.ball (↑x) r ∩ {z | 0 ≤ z.im}) ∧
                  (∀ z ∈ Metric.ball (↑x) r, z.im = 0 → ((f z - q) / b).im = 0) ∧
                    ∀ z ∈ Metric.ball (↑x) r, 0 < z.im → 0 < ((f z - q) / b).im)
  (hvertex :
    ∀ (i : ι),
      (e i ∈ Set.Ioo (-1) 1 ∧
          ∃ r > 0,
            ∃ b,
              b ≠ 0 ∧
                ContinuousOn f (Metric.ball (↑(a i)) r ∩ {z | 0 ≤ z.im}) ∧
                  Set.InjOn f (Metric.ball (↑(a i)) r ∩ {z | 0 ≤ z.im}) ∧
                    (∀ z ∈ Metric.ball (↑(a i)) r,
                        0 < z.im → |((f z - f ↑(a i)) / b).arg| < (e i + 1) * Real.pi / 2) ∧
                      ∀ z ∈ Metric.ball (↑(a i)) r,
                        z.im = 0 →
                          f z ≠ f ↑(a i) → |((f z - f ↑(a i)) / b).arg| = (e i + 1) * Real.pi / 2) ∨
        (e i ∈ Set.Ioo (-3) (-1) ∧
            ∃ r > 0,
              ∃ c b,
                b ≠ 0 ∧
                  ∃ g,
                    Set.EqOn g (fun z => b / (f z - c)) (Metric.ball (↑(a i)) r ∩ {z | 0 < z.im}) ∧
                      g ↑(a i) = 0 ∧
                        ContinuousOn g (Metric.ball (↑(a i)) r ∩ {z | 0 ≤ z.im}) ∧
                          Set.InjOn g (Metric.ball (↑(a i)) r ∩ {z | 0 ≤ z.im}) ∧
                            (∀ z ∈ Metric.ball (↑(a i)) r,
                                0 < z.im → |(g z).arg| < (-e i - 1) * Real.pi / 2) ∧
                              ∀ z ∈ Metric.ball (↑(a i)) r,
                                z.im = 0 → g z ≠ 0 → |(g z).arg| = (-e i - 1) * Real.pi / 2) ∨
          (e i = -1 ∧
              ∃ r > 0,
                ∃ c b,
                  b ≠ 0 ∧
                    ∃ g,
                      Set.EqOn g (fun z => Complex.exp ((f z - c) / b))
                          (Metric.ball (↑(a i)) r ∩ {z | 0 < z.im}) ∧
                        g ↑(a i) = 0 ∧
                          ContinuousOn g (Metric.ball (↑(a i)) r ∩ {z | 0 ≤ z.im}) ∧
                            (∀ z ∈ Metric.ball (↑(a i)) r, z.im = 0 → (g z).im = 0) ∧
                              Set.MapsTo g (Metric.ball (↑(a i)) r ∩ {z | 0 < z.im})
                                  {z | 0 < z.im} ∧
                                Set.InjOn g (Metric.ball (↑(a i)) r ∩ {z | 0 ≤ z.im})) ∨
            e i = -3 ∧
              ∃ r > 0,
                ∃ ρ c b,
                  b ≠ 0 ∧
                    ContinuousOn f ((Metric.closedBall (↑(a i)) r ∩ {z | 0 ≤ z.im}) \ {↑(a i)}) ∧
                      Set.InjOn f ((Metric.closedBall (↑(a i)) r ∩ {z | 0 ≤ z.im}) \ {↑(a i)}) ∧
                        Filter.Tendsto f (nhdsWithin (↑(a i)) ({z | 0 ≤ z.im} \ {↑(a i)}))
                            (Bornology.cobounded ℂ) ∧
                          ∀ (w : ℂ),
                            ρ < ‖w - c‖ →
                              (w ∈
                                  f '' (Metric.ball (↑(a i)) r ∩ UpperHalfPlane.upperHalfPlaneSet) ↔
                                ((w - c) / b).re < 0 ∨ ((w - c) / b).im ∉ Set.Icc 0 Real.pi))
  {L : ℂ}
  (hinfty :
    Filter.Tendsto (fun z => z * logDeriv (deriv f) z)
      (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) (nhds L)) :
  Set.EqOn f
    (fun z =>
      deriv f ↑z₀ / TauCeti.schwarzChristoffelIntegrand a e ↑z₀ *
          TauCeti.schwarzChristoffelPrimitive a e z₀ z +
        f ↑z₀)
    UpperHalfPlane.upperHalfPlaneSet

Lean

Formalized in Tau Ceti as TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_polygonal_boundary.

Other forms

The Schwarz--Christoffel formula for a conformal map onto a polygonal domain. Formalized in Tau Ceti as TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_polygonal_domain.

TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_polygonal_domain.{u_1} {U : Set ℂ}
  {f : ℂ → ℂ} {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (ha : Function.Injective a)
  (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) (z₀ : UpperHalfPlane) {v : ι → ℂ} {p : ℂ}
  (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfc : ContinuousOn f {z | 0 ≤ z.im})
  (hfi : Set.InjOn f {z | 0 ≤ z.im}) (hfU : f '' UpperHalfPlane.upperHalfPlaneSet = U)
  (hfv : ∀ (i : ι), f ↑(a i) = v i)
  (hp : Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 ≤ z.im}) (nhds p))
  (hpf : p ∉ f '' {z | 0 ≤ z.im})
  (hside :
    ∀ w ∈ frontier U,
      (∀ (i : ι), w ≠ v i) →
        ∃ ρ > 0, ∃ q b, b ≠ 0 ∧ ∀ z ∈ Metric.ball w ρ, z ∈ U ↔ 0 < ((z - q) / b).im)
  (hcorner :
    ∀ (i : ι),
      ∃ ρ > 0,
        ∃ b,
          b ≠ 0 ∧
            ∀ z ∈ Metric.ball (v i) ρ,
              z ≠ v i → (z ∈ U ↔ |((z - v i) / b).arg| < (e i + 1) * Real.pi / 2)) :
  Set.EqOn f
    (fun z =>
      deriv f ↑z₀ / TauCeti.schwarzChristoffelIntegrand a e ↑z₀ *
          TauCeti.schwarzChristoffelPrimitive a e z₀ z +
        f ↑z₀)
    UpperHalfPlane.upperHalfPlaneSet

The Schwarz--Christoffel formula for a conformal map onto a polygonal domain whose end is the exterior of a half-strip. Formalized in Tau Ceti as TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_halfStripExterior_polygonal_domain.

TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_halfStripExterior_polygonal_domain.{u_1}
  {U : Set ℂ} {f : ℂ → ℂ} {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (ha : Function.Injective a)
  (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) (z₀ : UpperHalfPlane) {v : ι → ℂ}
  (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfc : ContinuousOn f {z | 0 ≤ z.im})
  (hfi : Set.InjOn f {z | 0 ≤ z.im}) (hfU : f '' UpperHalfPlane.upperHalfPlaneSet = U)
  (hfv : ∀ (i : ι), f ↑(a i) = v i)
  (hp :
    Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 ≤ z.im})
      (Bornology.cobounded ℂ))
  (hside :
    ∀ w ∈ frontier U,
      (∀ (i : ι), w ≠ v i) →
        ∃ ρ > 0, ∃ q b, b ≠ 0 ∧ ∀ z ∈ Metric.ball w ρ, z ∈ U ↔ 0 < ((z - q) / b).im)
  (hcorner :
    ∀ (i : ι),
      ∃ ρ > 0,
        ∃ b,
          b ≠ 0 ∧
            ∀ z ∈ Metric.ball (v i) ρ,
              z ≠ v i → (z ∈ U ↔ |((z - v i) / b).arg| < (e i + 1) * Real.pi / 2))
  (hinfty :
    ∃ ρ c b,
      b ≠ 0 ∧
        ∀ (z : ℂ),
          ρ < ‖z - c‖ → (z ∈ U ↔ ((z - c) / b).re < 0 ∨ ((z - c) / b).im ∉ Set.Icc 0 Real.pi)) :
  Set.EqOn f
    (fun z =>
      deriv f ↑z₀ / TauCeti.schwarzChristoffelIntegrand a e ↑z₀ *
          TauCeti.schwarzChristoffelPrimitive a e z₀ z +
        f ↑z₀)
    UpperHalfPlane.upperHalfPlaneSet

The Schwarz--Christoffel formula for a conformal map onto a polygonal domain with a half-strip end. Formalized in Tau Ceti as TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_halfStrip_polygonal_domain.

TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_halfStrip_polygonal_domain.{u_1}
  {U : Set ℂ} {f : ℂ → ℂ} {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (ha : Function.Injective a)
  (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) (z₀ : UpperHalfPlane) {v : ι → ℂ}
  (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet) (hfc : ContinuousOn f {z | 0 ≤ z.im})
  (hfi : Set.InjOn f {z | 0 ≤ z.im}) (hfU : f '' UpperHalfPlane.upperHalfPlaneSet = U)
  (hfv : ∀ (i : ι), f ↑(a i) = v i)
  (hp :
    Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 ≤ z.im})
      (Bornology.cobounded ℂ))
  (hside :
    ∀ w ∈ frontier U,
      (∀ (i : ι), w ≠ v i) →
        ∃ ρ > 0, ∃ q b, b ≠ 0 ∧ ∀ z ∈ Metric.ball w ρ, z ∈ U ↔ 0 < ((z - q) / b).im)
  (hcorner :
    ∀ (i : ι),
      ∃ ρ > 0,
        ∃ b,
          b ≠ 0 ∧
            ∀ z ∈ Metric.ball (v i) ρ,
              z ≠ v i → (z ∈ U ↔ |((z - v i) / b).arg| < (e i + 1) * Real.pi / 2))
  (hinfty :
    ∃ ρ c b,
      b ≠ 0 ∧
        ∀ (z : ℂ),
          ρ < ‖z - c‖ → (z ∈ U ↔ 0 < ((z - c) / b).re ∧ ((z - c) / b).im ∈ Set.Ioo 0 Real.pi)) :
  Set.EqOn f
    (fun z =>
      deriv f ↑z₀ / TauCeti.schwarzChristoffelIntegrand a e ↑z₀ *
          TauCeti.schwarzChristoffelPrimitive a e z₀ z +
        f ↑z₀)
    UpperHalfPlane.upperHalfPlaneSet

The Schwarz--Christoffel formula for a conformal map onto an unbounded polygonal domain. Formalized in Tau Ceti as TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_unbounded_polygonal_domain.

TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_unbounded_polygonal_domain.{u_1}
  {U : Set ℂ} {f : ℂ → ℂ} {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (ha : Function.Injective a)
  (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) (z₀ : UpperHalfPlane) {v : ι → ℂ} {β : ℝ}
  (hβ : β ∈ Set.Ioo 0 2) (hf : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet)
  (hfc : ContinuousOn f {z | 0 ≤ z.im}) (hfi : Set.InjOn f {z | 0 ≤ z.im})
  (hfU : f '' UpperHalfPlane.upperHalfPlaneSet = U) (hfv : ∀ (i : ι), f ↑(a i) = v i)
  (hp :
    Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 ≤ z.im})
      (Bornology.cobounded ℂ))
  (hside :
    ∀ w ∈ frontier U,
      (∀ (i : ι), w ≠ v i) →
        ∃ ρ > 0, ∃ q b, b ≠ 0 ∧ ∀ z ∈ Metric.ball w ρ, z ∈ U ↔ 0 < ((z - q) / b).im)
  (hcorner :
    ∀ (i : ι),
      ∃ ρ > 0,
        ∃ b,
          b ≠ 0 ∧
            ∀ z ∈ Metric.ball (v i) ρ,
              z ≠ v i → (z ∈ U ↔ |((z - v i) / b).arg| < (e i + 1) * Real.pi / 2))
  (hinfty :
    ∃ ρ c b, b ≠ 0 ∧ ∀ (z : ℂ), ρ < ‖z - c‖ → (z ∈ U ↔ |((z - c) / b).arg| < β * Real.pi / 2)) :
  Set.EqOn f
    (fun z =>
      deriv f ↑z₀ / TauCeti.schwarzChristoffelIntegrand a e ↑z₀ *
          TauCeti.schwarzChristoffelPrimitive a e z₀ z +
        f ↑z₀)
    UpperHalfPlane.upperHalfPlaneSet

Sources

• Tau Ceti documentation: TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_polygonal_boundary
• Source of TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_polygonal_boundary in TauCeti/Analysis/Complex/Conformal/SchwarzChristoffel/Formula.lean

LeanTauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_polygonal_boundary · TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_polygonal_domain · TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_halfStripExterior_polygonal_domain · TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_halfStrip_polygonal_domain · TauCeti.eqOn_const_mul_schwarzChristoffelPrimitive_add_of_unbounded_polygonal_domain

Uses 3 · Used by 3

Proof usesThe converse Schwarz--Christoffel theorem from the prevertex residues · Rouché's theorem for a disc, classical form · Schwarz reflection principle (real axis)

Used byThe Schwarz--Christoffel theorem for a bounded polygonal Jordan domain · The Schwarz--Christoffel theorem for an unbounded polygonal Jordan domain · The disc Schwarz--Christoffel theorem for an unbounded polygonal Jordan domain

TheoremStrict Schwarz lemma#

A holomorphic map of ball c R₁ into closedBall (g c) R₂ that is not injective has ‖deriv g c‖ < R₂ / R₁.

Both radii must be positive: for R₂ = 0 the map is constant, so it is not injective and the strict bound fails.

TauCeti.norm_deriv_lt_div_of_not_injOn.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E]
  [StrictConvexSpace ℝ E] {g : ℂ → E} {c : ℂ} {R₁ R₂ : ℝ} (hR₁ : 0 < R₁) (hR₂ : 0 < R₂)
  (hgd : DifferentiableOn ℂ g (Metric.ball c R₁))
  (hgm : Set.MapsTo g (Metric.ball c R₁) (Metric.closedBall (g c) R₂))
  (hgi : ¬Set.InjOn g (Metric.ball c R₁)) : ‖deriv g c‖ < R₂ / R₁

Lean

Formalized in Tau Ceti as TauCeti.norm_deriv_lt_div_of_not_injOn.

Other forms

Strict Schwarz lemma, equal radii. Formalized in Tau Ceti as TauCeti.norm_deriv_lt_one_of_not_injOn.

TauCeti.norm_deriv_lt_one_of_not_injOn.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E]
  [StrictConvexSpace ℝ E] {g : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 < R)
  (hgd : DifferentiableOn ℂ g (Metric.ball c R))
  (hgm : Set.MapsTo g (Metric.ball c R) (Metric.closedBall (g c) R))
  (hgi : ¬Set.InjOn g (Metric.ball c R)) : ‖deriv g c‖ < 1

Sources

• Tau Ceti documentation: TauCeti.norm_deriv_lt_div_of_not_injOn
• Source of TauCeti.norm_deriv_lt_div_of_not_injOn in TauCeti/Analysis/Complex/Conformal/Schwarz.lean

LeanTauCeti.norm_deriv_lt_div_of_not_injOn · TauCeti.norm_deriv_lt_one_of_not_injOn

Used by 5

Used byCarathéodory's continuity theorem, as a characterization · The Riemann map of a Jordan domain extends to a homeomorphism of the closures · The Riemann mapping theorem · The Schwarz--Christoffel theorem for a bounded polygonal Jordan domain · Carathéodory's theorem for the inside of a Jordan curve

TheoremVitali's convergence theorem#

Let Ω be an open preconnected subset of ℂ. A locally bounded sequence of holomorphic maps from Ω into a proper complex normed space E (for instance ℂ) which converges pointwise on a subset A ⊆ Ω having an accumulation point in Ω converges locally uniformly on Ω to a holomorphic map.

The pointwise limit on A need not be supplied: its existence is enough to determine the holomorphic limit uniquely.

TauCeti.vitali.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {Ω A : Set ℂ}
  [ProperSpace E] {F : ℕ → ℂ → E} (hΩ : IsOpen Ω) (hconn : IsPreconnected Ω)
  (hF : ∀ (n : ℕ), DifferentiableOn ℂ (F n) Ω) (hb : TauCeti.IsLocallyBoundedOn F Ω) (hAΩ : A ⊆ Ω)
  {z₀ : ℂ} (hz₀ : z₀ ∈ Ω) (hacc : AccPt z₀ (Filter.principal A))
  (hpoint : ∀ z ∈ A, ∃ w, Filter.Tendsto (fun n => F n z) Filter.atTop (nhds w)) :
  ∃ g, DifferentiableOn ℂ g Ω ∧ TendstoLocallyUniformlyOn F g Filter.atTop Ω

Lean

Formalized in Tau Ceti as TauCeti.vitali.

Sources

• Tau Ceti documentation: TauCeti.vitali
• Source of TauCeti.vitali in TauCeti/Analysis/Complex/Conformal/Vitali.lean

LeanTauCeti.vitali

Uses 1 · Used by 1

Proof usesMontel's selection theorem

Used byVitali's theorem with prescribed pointwise values

TheoremVitali's theorem with prescribed pointwise values#

Under the hypotheses of vitali, if the sequence converges pointwise on A to a specified function g, its locally uniform holomorphic limit agrees with g throughout A.

No regularity of g away from A is assumed or concluded; when A is all of Ω the limit is g itself, which is TauCeti.tendstoLocallyUniformlyOn_of_isLocallyBoundedOn_of_forall_tendsto.

TauCeti.vitali_of_tendsto.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E]
  {Ω A : Set ℂ} [ProperSpace E] {F : ℕ → ℂ → E} (hΩ : IsOpen Ω) (hconn : IsPreconnected Ω)
  (hF : ∀ (n : ℕ), DifferentiableOn ℂ (F n) Ω) (hb : TauCeti.IsLocallyBoundedOn F Ω) (hAΩ : A ⊆ Ω)
  {z₀ : ℂ} (hz₀ : z₀ ∈ Ω) (hacc : AccPt z₀ (Filter.principal A)) {g : ℂ → E}
  (hpoint : ∀ z ∈ A, Filter.Tendsto (fun n => F n z) Filter.atTop (nhds (g z))) :
  ∃ q, DifferentiableOn ℂ q Ω ∧ Set.EqOn q g A ∧ TendstoLocallyUniformlyOn F q Filter.atTop Ω

Lean

Formalized in Tau Ceti as TauCeti.vitali_of_tendsto.

Sources

• Tau Ceti documentation: TauCeti.vitali_of_tendsto
• Source of TauCeti.vitali_of_tendsto in TauCeti/Analysis/Complex/Conformal/Vitali.lean

LeanTauCeti.vitali_of_tendsto

Uses 1

Proof usesVitali's convergence theorem

TheoremWolff's lemma (TauCeti.exists_circleImageLength_sq_lt)#

If 2 π times the Dirichlet integral of f over s is smaller than c * log (R / r), then some circle of radius ρ between r and R has ℓ ρ ^ 2 < c.

Since log (R / r) grows without bound as the annulus is made longer while the Dirichlet integral stays fixed, this makes ℓ arbitrarily small at arbitrarily small radii; for a holomorphic f that is the geometric statement that a map of finite Dirichlet integral cannot keep every circular arc about ζ long.

TauCeti.exists_circleImageLength_sq_lt {s : Set ℂ} (f : ℂ → ℂ) (hs : MeasurableSet s) (ζ : ℂ)
  {r R : ℝ} (hr : 0 < r) (hrR : r < R) {c : ENNReal}
  (hc :
    ENNReal.ofReal (2 * Real.pi) * ∫⁻ (z : ℂ) in s, ‖deriv f z‖ₑ ^ 2 <
      c * ENNReal.ofReal (Real.log (R / r))) :
  ∃ ρ ∈ Set.Ioo r R, TauCeti.circleImageLength f s ζ ρ ^ 2 < c

Lean

Formalized in Tau Ceti as TauCeti.exists_circleImageLength_sq_lt.

Other forms

Wolff's lemma, area form. Formalized in Tau Ceti as TauCeti.exists_circleImageLength_sq_lt_of_volume_image.

TauCeti.exists_circleImageLength_sq_lt_of_volume_image {U s : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U)
  (hf : DifferentiableOn ℂ f U) (hs : MeasurableSet s) (hsU : s ⊆ U) (hinj : Set.InjOn f s) (ζ : ℂ)
  {r R : ℝ} (hr : 0 < r) (hrR : r < R) {c : ENNReal}
  (hc :
    ENNReal.ofReal (2 * Real.pi) * MeasureTheory.volume (f '' s) <
      c * ENNReal.ofReal (Real.log (R / r))) :
  ∃ ρ ∈ Set.Ioo r R, TauCeti.circleImageLength f s ζ ρ ^ 2 < c

Sources

• Tau Ceti documentation: TauCeti.exists_circleImageLength_sq_lt
• Source of TauCeti.exists_circleImageLength_sq_lt in TauCeti/Analysis/Complex/Conformal/LengthArea.lean

LeanTauCeti.exists_circleImageLength_sq_lt · TauCeti.exists_circleImageLength_sq_lt_of_volume_image

Uses 1

Proof usesWolff's lemma (TauCeti.exists_circleLIntegral_sq_lt)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.