The angle condition of… to The Herglotz formula on a disc

TheoremThe angle condition of Poincaré's theorem#

If every angle of P is π / m for a natural number m, then at each finite vertex of the double the order of the cycle transformation times the cycle angle sum is 2π.

TauCeti.UpperHalfPlane.ConvexPolygon.orderOf_doubleTriangleSidePairing_cycleMap_mul_cycleAngleSum
  {P : TauCeti.UpperHalfPlane.ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2}
  {h₁ : P.interiorAngle 1 < Real.pi / 2} (hP : ∀ (i : Fin 3), ∃ m, P.interiorAngle i = Real.pi / ↑m)
  (j : Fin 4) (z : UpperHalfPlane) (hz : (P.doubleTriangle h₀ h₁).vertex j = Sum.inl z) :
  ↑(orderOf ((P.doubleTriangleSidePairing h₀ h₁).cycleMap j)) *
      (P.doubleTriangleSidePairing h₀ h₁).cycleAngleSum j =
    2 * Real.pi
Lean

Formalized in Tau Ceti as TauCeti.UpperHalfPlane.ConvexPolygon.orderOf_doubleTriangleSidePairing_cycleMap_mul_cycleAngleSum.

Sources
LeanTauCeti.UpperHalfPlane.ConvexPolygon.orderOf_doubleTriangleSidePairing_cycleMap_mul_cycleAngleSum

TheoremThe Apollonius identity for the Moebius factor#

For every z : ℂ,

‖z - a‖ ^ 2 - t ^ 2 * ‖1 - conj a * z‖ ^ 2 = (1 - t ^ 2 * ‖a‖ ^ 2) * (‖z - pseudoHyperbolicCenter a t‖ ^ 2 - pseudoHyperbolicRadius a t ^ 2).

Both sides are real quadratics in z.re and z.im with the same leading coefficient 1 - t ^ 2 * ‖a‖ ^ 2, and the definitions of TauCeti.pseudoHyperbolicCenter and TauCeti.pseudoHyperbolicRadius are exactly what completes the square. No hypothesis is placed on z, and the disc hypothesis on a enters only through the nonvanishing of the denominator.

TauCeti.sq_norm_sub_sub_mul_sq_norm_one_sub_conj_mul (a z : ℂ) (t : ℝ)
  (hD : 1 - t ^ 2 * ‖a‖ ^ 2 ≠ 0) :
  ‖z - a‖ ^ 2 - t ^ 2 * ‖1 - (starRingEnd ℂ) a * z‖ ^ 2 =
    (1 - t ^ 2 * ‖a‖ ^ 2) *
      (‖z - TauCeti.pseudoHyperbolicCenter a t‖ ^ 2 - TauCeti.pseudoHyperbolicRadius a t ^ 2)
Lean

Formalized in Tau Ceti as TauCeti.sq_norm_sub_sub_mul_sq_norm_one_sub_conj_mul.

Sources
LeanTauCeti.sq_norm_sub_sub_mul_sq_norm_one_sub_conj_mul

TheoremThe bounded-image form of the small-Jordan-curve theorem#

A holomorphic injection of a disc onto a bounded domain has finite Dirichlet integral by the conformal area formula, so for every positive tolerance and radius bound, some closed image crosscut can be chosen on a Jordan curve in the closure of the image domain whose diameter is at most the tolerance.

This is the form used for the Riemann map of a bounded Jordan domain.

TauCeti.exists_isJordanCurve_superset_closure_image_ball_inter_sphere_diam_le_of_isBounded
  {f : ℂ → ℂ} {c ζ : ℂ} {r : ℝ} (hζ : dist ζ c = r) (hr : 0 < r)
  (hf : DifferentiableOn ℂ f (Metric.ball c r)) (hinj : Set.InjOn f (Metric.ball c r))
  (hb : Bornology.IsBounded (f '' Metric.ball c r))
  (hfrontier : TauCeti.IsJordanCurve (frontier (f '' Metric.ball c r))) {ε R : ℝ} (hε : 0 < ε)
  (hR : 0 < R) :
  ∃ ρ ∈ Set.Ioo 0 R,
    ρ < 2 * r ∧
      ∃ J,
        TauCeti.IsJordanCurve J ∧
          closure (f '' (Metric.ball c r ∩ Metric.sphere ζ ρ)) ⊆ J ∧
            J ⊆
                closure (f '' (Metric.ball c r ∩ Metric.sphere ζ ρ)) ∪
                  frontier (f '' Metric.ball c r) ∧
              J ⊆ closure (f '' Metric.ball c r) ∧ Metric.diam J ≤ ε
Lean

Formalized in Tau Ceti as TauCeti.exists_isJordanCurve_superset_closure_image_ball_inter_sphere_diam_le_of_isBounded.

Sources
LeanTauCeti.exists_isJordanCurve_superset_closure_image_ball_inter_sphere_diam_le_of_isBounded
Uses 1
Proof usesWolff's lemma (TauCeti.exists_circleLIntegral_sq_lt)

TheoremThe Calderón–Zygmund inequality for the Cauchy–Riemann operator#

Let 1 < p < ∞. There is a constant C with

‖Du‖_{Lᵖ} ≤ C ‖\bar∂u‖_{Lᵖ}

for every Schwartz function u on ℂ with values in a complex Hilbert space, where Du is the real derivative of u and \bar∂u = (∂ₓu + I ∂ᵧu) / 2 its conjugate Wirtinger derivative.

TauCeti.exists_eLpNorm_fderiv_le_eLpNorm_conjWirtingerDeriv.{u_1} {F : Type u_1}
  [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] {p : ENNReal} (hp : 1 < p)
  (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ (u : SchwartzMap ℂ F),
      MeasureTheory.eLpNorm (fderiv ℝ ⇑u) p MeasureTheory.volume ≤
        ↑C *
          MeasureTheory.eLpNorm (fun z => (TauCeti.conjWirtingerDeriv (⇑u) z) 1) p
            MeasureTheory.volume
Lean

Formalized in Tau Ceti as TauCeti.exists_eLpNorm_fderiv_le_eLpNorm_conjWirtingerDeriv.

Other forms

The Calderón–Zygmund inequality for smooth compactly supported maps. Formalized in Tau Ceti as TauCeti.exists_eLpNorm_fderiv_le_eLpNorm_conjWirtingerDeriv_of_hasCompactSupport.

TauCeti.exists_eLpNorm_fderiv_le_eLpNorm_conjWirtingerDeriv_of_hasCompactSupport.{u_1}
  {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] {p : ENNReal}
  (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ (u : ℂ → F),
      ContDiff ℝ (↑⊤) u →
        HasCompactSupport u →
          MeasureTheory.eLpNorm (fderiv ℝ u) p MeasureTheory.volume ≤
            ↑C *
              MeasureTheory.eLpNorm (fun z => (TauCeti.conjWirtingerDeriv u z) 1) p
                MeasureTheory.volume
Sources
LeanTauCeti.exists_eLpNorm_fderiv_le_eLpNorm_conjWirtingerDeriv · TauCeti.exists_eLpNorm_fderiv_le_eLpNorm_conjWirtingerDeriv_of_hasCompactSupport
Uses 1
Proof usesThe Mihlin–Hörmander multiplier theorem on Lᵖ

TheoremCarathéodory's theorem for the inside of a Jordan curve#

For a Jordan curve C ⊆ ℂ and a point p of its inside filledHull C \ C, there is a map g, holomorphic on the open unit disc with g 0 = p, carrying the disc bijectively onto the inside and the unit circle bijectively onto C, which restricts to a homeomorphism of the closed disc onto filledHull C.

TauCeti.IsJordanCurve.exists_homeomorph_closedBall_filledHull {C : Set ℂ} {p : ℂ}
  (hC : TauCeti.IsJordanCurve C) (hp : p ∈ TauCeti.filledHull C \ C) :
  ∃ g,
    ContinuousOn g (Metric.closedBall 0 1) ∧
      DifferentiableOn ℂ g (Metric.ball 0 1) ∧
        Set.BijOn g (Metric.ball 0 1) (TauCeti.filledHull C \ C) ∧
          Set.BijOn g (Metric.sphere 0 1) C ∧
            g 0 = p ∧ ∃ e, ∀ (z : ↑(Metric.closedBall 0 1)), ↑(e z) = g ↑z
Lean

Formalized in Tau Ceti as TauCeti.IsJordanCurve.exists_homeomorph_closedBall_filledHull.

Other forms

Carathéodory's theorem for the outside of a Jordan curve. Formalized in Tau Ceti as TauCeti.IsJordanCurve.exists_homeomorph_compl_ball_compl_filledHull_sdiff.

TauCeti.IsJordanCurve.exists_homeomorph_compl_ball_compl_filledHull_sdiff {C : Set ℂ}
  (hC : TauCeti.IsJordanCurve C) :
  ∃ h,
    ContinuousOn h (Metric.ball 0 1)ᶜ ∧
      DifferentiableOn ℂ h (Metric.closedBall 0 1)ᶜ ∧
        Set.BijOn h (Metric.closedBall 0 1)ᶜ (TauCeti.filledHull C)ᶜ ∧
          Set.BijOn h (Metric.sphere 0 1) C ∧
            Filter.Tendsto h (Bornology.cobounded ℂ) (Bornology.cobounded ℂ) ∧
              ∃ e, ∀ (z : ↑(Metric.ball 0 1)ᶜ), ↑(e z) = h ↑z

Carathéodory's theorem on the closed upper half-plane for an unbounded Jordan domain. Formalized in Tau Ceti as TauCeti.exists_continuousOn_bijOn_upperHalfPlaneSet_of_isJordanCurve_insert_infty.

TauCeti.exists_continuousOn_bijOn_upperHalfPlaneSet_of_isJordanCurve_insert_infty {U : Set ℂ}
  (hUo : IsOpen U) (hUc : IsConnected U)
  (hUJ : TauCeti.IsJordanCurve (insert OnePoint.infty (OnePoint.some '' frontier U))) :
  ∃ f,
    ContinuousOn f {z | 0 ≤ z.im} ∧
      DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet ∧
        Set.BijOn f UpperHalfPlane.upperHalfPlaneSet U ∧
          Set.BijOn f {z | 0 ≤ z.im} (closure U) ∧
            Set.BijOn f {z | z.im = 0} (frontier U) ∧
              Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 ≤ z.im})
                (Bornology.cobounded ℂ)
Sources
LeanTauCeti.IsJordanCurve.exists_homeomorph_closedBall_filledHull · TauCeti.IsJordanCurve.exists_homeomorph_compl_ball_compl_filledHull_sdiff · TauCeti.exists_continuousOn_bijOn_upperHalfPlaneSet_of_isJordanCurve_insert_infty
Uses 14 · Used by 4
Proof usesCarathéodory's continuity theorem, as a characterization · Cauchy estimate · The converse of Cauchy's theorem · The frontier of a complementary component of a Jordan curve is the whole curve · Generalized winding number (HW Def 2.1) · The homology Cauchy theorem (roadmap homologyCauchyTheorem, Layer 3) · Hurwitz's theorem · Janiszewski's theorem · The Jordan curve theorem · The Jordan separation theorem · Montel's selection theorem · The Riemann mapping theorem · Rouché's theorem for a disc, classical form · Strict Schwarz lemma
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 · The Schoenflies theorem

TheoremCauchy estimate#

On a ball of radius R inside U, a bounded holomorphic map f is Lipschitz at the centre with constant 2 * ‖f‖ / R.

TauCeti.BoundedHolomorphicFunctions.dist_apply_le_of_ball_subset.{u_1, u_2} {V : Type u_1}
  {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E]
  {U : TopologicalSpace.Opens V} (f : ↥(TauCeti.boundedHolomorphicFunctions E U)) {x z : ↥U} {R : ℝ}
  (hR : Metric.ball (↑x) R ⊆ ↑U) (hz : dist z x < R) : dist (↑f z) (↑f x) ≤ 2 * ‖f‖ / R * dist z x
Lean

Formalized in Tau Ceti as TauCeti.BoundedHolomorphicFunctions.dist_apply_le_of_ball_subset.

Other forms

Cauchy's estimate on a ball in a complex normed space. Formalized in Tau Ceti as TauCeti.norm_fderiv_le_of_forall_mem_ball_norm_le.

TauCeti.norm_fderiv_le_of_forall_mem_ball_norm_le.{u_1, u_2} {V : Type u_1} {E : Type u_2}
  [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {f : V → E}
  {c : V} {r M : ℝ} (hd : DifferentiableOn ℂ f (Metric.ball c r)) (hr : 0 < r)
  (hM : ∀ y ∈ Metric.ball c r, ‖f y‖ ≤ M) : ‖fderiv ℂ f c‖ ≤ 2 * M / r

Cauchy's estimate on a closed ball. Formalized in Tau Ceti as TauCeti.norm_deriv_le_of_forall_mem_closedBall_norm_le.

TauCeti.norm_deriv_le_of_forall_mem_closedBall_norm_le.{u_2} {E : Type u_2} {U : Set ℂ} {f : ℂ → E}
  [NormedAddCommGroup E] [NormedSpace ℂ E] (hf : DifferentiableOn ℂ f U) {c : ℂ} {r M : ℝ}
  (hr : 0 < r) (hsub : Metric.closedBall c r ⊆ U) (hM : ∀ w ∈ Metric.closedBall c r, ‖f w‖ ≤ M) :
  ‖deriv f c‖ ≤ M / r

Cauchy's estimate, uniformly on a ball. Formalized in Tau Ceti as TauCeti.norm_deriv_le_of_forall_mem_closedBall_two_mul_norm_le.

TauCeti.norm_deriv_le_of_forall_mem_closedBall_two_mul_norm_le.{u_2} {E : Type u_2} {U : Set ℂ}
  {f : ℂ → E} [NormedAddCommGroup E] [NormedSpace ℂ E] (hf : DifferentiableOn ℂ f U) {c : ℂ}
  {r M : ℝ} (hr : 0 < r) (hsub : Metric.closedBall c (2 * r) ⊆ U)
  (hM : ∀ w ∈ Metric.closedBall c (2 * r), ‖f w‖ ≤ M) {z : ℂ} (hz : z ∈ Metric.ball c r) :
  ‖deriv f z‖ ≤ M / r
Sources
LeanTauCeti.BoundedHolomorphicFunctions.dist_apply_le_of_ball_subset · TauCeti.norm_fderiv_le_of_forall_mem_ball_norm_le · TauCeti.norm_deriv_le_of_forall_mem_closedBall_norm_le · TauCeti.norm_deriv_le_of_forall_mem_closedBall_two_mul_norm_le
Used by 7
Used byCarathéodory's continuity theorem, as a characterization · The equicontinuity half of Montel'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 · Carathéodory's theorem for the inside of a Jordan curve · Montel's theorem as an equivalence

TheoremCauchy-Laurent coefficient formula#

For any convergent Laurent series on Metric.eball c R \ Metric.closedBall c r and any interior circle radius ρ ∈ (r, R), the n-th Laurent coefficient is circleLaurentCoeff f c ρ n.

TauCeti.HasLaurentSeriesOnAnnulus.circleLaurentCoeff_eq.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r ρ : ℝ} {R : ENNReal}
  (h : TauCeti.HasLaurentSeriesOnAnnulus f a c r R) (hrρ : r < ρ) (hρR : ENNReal.ofReal ρ < R)
  (n : ℤ) : TauCeti.circleLaurentCoeff f c ρ n = a n
Lean

Formalized in Tau Ceti as TauCeti.HasLaurentSeriesOnAnnulus.circleLaurentCoeff_eq.

Sources
LeanTauCeti.HasLaurentSeriesOnAnnulus.circleLaurentCoeff_eq

TheoremThe Cauchy–Pompeiu formula for a compactly supported C¹ map u : ℂ → F#

u is the Cauchy transform of ∂ₓ u + i ∂ᵧ u = 2 \bar∂ u, u w = (2π)⁻¹ ∫ (w - z)⁻¹ • (∂ₓ u z + i ∂ᵧ u z), the integral being over the whole plane.

HasCompactSupport.two_pi_inv_smul_integral_sub_inv_smul_fderiv_apply_one_add_I_smul_apply_I.{u_1}
  {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {u : ℂ → F}
  (hc : HasCompactSupport u) (hu : ContDiff ℝ 1 u) (w : ℂ) :
  (2 * ↑Real.pi)⁻¹ •
      ∫ (z : ℂ), (w - z)⁻¹ • ((fderiv ℝ u z) 1 + Complex.I • (fderiv ℝ u z) Complex.I) =
    u w
Lean

Formalized in Tau Ceti as HasCompactSupport.two_pi_inv_smul_integral_sub_inv_smul_fderiv_apply_one_add_I_smul_apply_I.

Sources
LeanHasCompactSupport.two_pi_inv_smul_integral_sub_inv_smul_fderiv_apply_one_add_I_smul_apply_I
Used by 1
Used byThe Dolbeault lemma on a disc

TheoremComplex analytic Weierstrass division theorem#

Let f, g : E × ℂ → ℂ be analytic at (x₀, w₀) on the product of a finite-dimensional complex normed space E with ℂ, and suppose the vertical slice w ↦ f (x₀, w) has finite order of vanishing d at w₀. Then there exist q analytic at (x₀, w₀) and r : Fin d → E → ℂ analytic at x₀ such that near (x₀, w₀), g (x, w) = f (x, w) * q (x, w) + ∑ i : Fin d, r i x * (w - w₀) ^ (i : ℕ).

AnalyticAt.exists_weierstrassDivision.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E]
  [FiniteDimensional ℂ E] {f g : E × ℂ → ℂ} {x₀ : E} {w₀ : ℂ} {d : ℕ} (hg : AnalyticAt ℂ g (x₀, w₀))
  (hf : AnalyticAt ℂ f (x₀, w₀)) (hd : analyticOrderAt (fun w => f (x₀, w)) w₀ = ↑d) :
  ∃ q r,
    AnalyticAt ℂ q (x₀, w₀) ∧
      (∀ (i : Fin d), AnalyticAt ℂ (r i) x₀) ∧
        g =ᶠ[nhds (x₀, w₀)] fun p => f p * q p + ∑ i, r i p.1 * (p.2 - w₀) ^ ↑i
Lean

Formalized in Tau Ceti as AnalyticAt.exists_weierstrassDivision.

Sources
LeanAnalyticAt.exists_weierstrassDivision
Uses 2
Proof usesComplex analytic Weierstrass preparation theorem · Osgood's lemma

TheoremComplex analytic Weierstrass preparation theorem#

Let f : E × ℂ → ℂ be analytic at (x₀, w₀) on the product of a finite-dimensional complex normed space E with ℂ, and suppose the vertical slice w ↦ f (x₀, w) has finite order of vanishing d at w₀. Then there exist analytic coefficient functions c : Fin d → E → ℂ vanishing at x₀ and an analytic function u nonvanishing at (x₀, w₀) such that near (x₀, w₀), f (x, w) = (TauCeti.Polynomial.monicOfCoeff (fun i ↦ c i x)).eval (w - w₀) * u (x, w).

AnalyticAt.exists_weierstrassPreparation.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] [FiniteDimensional ℂ E] {f : E × ℂ → ℂ} {x₀ : E} {w₀ : ℂ} {d : ℕ}
  (hf : AnalyticAt ℂ f (x₀, w₀)) (hd : analyticOrderAt (fun w => f (x₀, w)) w₀ = ↑d) :
  ∃ c u,
    (∀ (i : Fin d), AnalyticAt ℂ (c i) x₀) ∧
      (∀ (i : Fin d), c i x₀ = 0) ∧
        AnalyticAt ℂ u (x₀, w₀) ∧
          u (x₀, w₀) ≠ 0 ∧
            f =ᶠ[nhds (x₀, w₀)] fun p =>
              Polynomial.eval (p.2 - w₀) (TauCeti.Polynomial.monicOfCoeff fun i => c i p.1) * u p
Lean

Formalized in Tau Ceti as AnalyticAt.exists_weierstrassPreparation.

Sources
LeanAnalyticAt.exists_weierstrassPreparation
Uses 3 · Used by 3
Proof usesThe classical residue theorem on a circle · Newton's identities for a multiset · Osgood's lemma
Used byReal analytic Weierstrass preparation theorem · Complex analytic Weierstrass division theorem · Weierstrass preparation theorem in holomorphic stalks

TheoremThe component mapping theorem from one boundary sheet#

Under boundary avoidance, one uniquely parametrized regular boundary value makes the primitive a bijection onto the complementary component of the finite boundary trace containing its base-point image. Neither simple connectivity of that component nor global boundary injectivity is assumed.

TauCeti.bijOn_schwarzChristoffelPrimitive_connectedComponentIn_of_unique_boundary_value.{u_1}
  {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane)
  (hfinite : ∀ (j : ι), -1 ≤ ∑ i with a i = a j, e i)
  (havoid :
    Disjoint (TauCeti.schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet)
      (TauCeti.schwarzChristoffelFiniteBoundary a e z₀))
  {p q x : ℝ} (ha : ∀ (i : ι), e i ≠ 0 → a i ∉ Set.Ioo p q) (hx : x ∈ Set.Ioo p q)
  (hunique :
    ∀ (t : OnePoint ℝ),
      TauCeti.schwarzChristoffelSphereBoundary a e z₀ t =
          TauCeti.schwarzChristoffelSphereBoundary a e z₀ ↑x →
        t = ↑x) :
  Set.BijOn (TauCeti.schwarzChristoffelPrimitive a e z₀) UpperHalfPlane.upperHalfPlaneSet
    (connectedComponentIn (TauCeti.schwarzChristoffelFiniteBoundary a e z₀)ᶜ
      (TauCeti.schwarzChristoffelPrimitive a e z₀ ↑z₀))
Lean

Formalized in Tau Ceti as TauCeti.bijOn_schwarzChristoffelPrimitive_connectedComponentIn_of_unique_boundary_value.

Sources
LeanTauCeti.bijOn_schwarzChristoffelPrimitive_connectedComponentIn_of_unique_boundary_value
Uses 1
Proof usesRouché's theorem for a disc, classical form

TheoremThe cusp condition of Poincaré's theorem#

The cycle transformations at the ideal vertices of the double are parabolic.

TauCeti.UpperHalfPlane.ConvexPolygon.isParabolic_doubleTriangleSidePairing_cycleMap
  {P : TauCeti.UpperHalfPlane.ConvexPolygon 3} {h₀ : P.interiorAngle 0 < Real.pi / 2}
  {h₁ : P.interiorAngle 1 < Real.pi / 2} (j : Fin 4) (ξ : OnePoint ℝ)
  (hξ : (P.doubleTriangle h₀ h₁).vertex j = Sum.inr ξ) :
  ((P.doubleTriangleSidePairing h₀ h₁).cycleMap j).IsParabolic
Lean

Formalized in Tau Ceti as TauCeti.UpperHalfPlane.ConvexPolygon.isParabolic_doubleTriangleSidePairing_cycleMap.

Sources
LeanTauCeti.UpperHalfPlane.ConvexPolygon.isParabolic_doubleTriangleSidePairing_cycleMap

TheoremThe disc Schwarz--Christoffel theorem for an unbounded polygonal Jordan domain#

Suppose a connected open set has Jordan frontier on the Riemann sphere, finitely many distinct corners of angles (e i + 1) * π, straight sides away from those corners, and a sector of opening β * π at infinity. Then it is the bijective image of the unit disc under an affine image of a disc Schwarz--Christoffel primitive. The finite prevertices have exponents e i and tend to the prescribed vertices; the additional prevertex 1 has exponent -β - 1 and tends to infinity.

TauCeti.exists_bijOn_const_mul_schwarzChristoffelDiscPrimitive_add_of_isJordanCurve_insert_infty.{u_1}
  {ι : Type u_1} [Fintype ι] (e : ι → ℝ) (he : ∀ (i : ι), e i ∈ Set.Ioo (-1) 1) {β : ℝ}
  (hβ : β ∈ Set.Ioo 0 2) {U : Set ℂ} (hUo : IsOpen U) (hUc : IsConnected U)
  (hUJ : TauCeti.IsJordanCurve (insert OnePoint.infty (OnePoint.some '' frontier U))) {v : ι → ℂ}
  (hv : Function.Injective v)
  (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)) :
  ∃ a,
    Function.Injective a ∧
      ∃ A,
        A ≠ 0 ∧
          ∃ B,
            Set.BijOn
                (fun ζ =>
                  A *
                      TauCeti.schwarzChristoffelDiscPrimitive
                        (Option.elim' 1 fun i => TauCeti.boundaryCayley (a i))
                        (Option.elim' (-β - 1) e) ζ +
                    B)
                (Metric.ball 0 1) U ∧
              (∀ (i : ι),
                  Filter.Tendsto
                    (fun ζ =>
                      A *
                          TauCeti.schwarzChristoffelDiscPrimitive
                            (Option.elim' 1 fun j => TauCeti.boundaryCayley (a j))
                            (Option.elim' (-β - 1) e) ζ +
                        B)
                    (nhdsWithin (↑(TauCeti.boundaryCayley (a i))) (Metric.ball 0 1)) (nhds (v i))) ∧
                Filter.Tendsto
                  (fun ζ =>
                    A *
                        TauCeti.schwarzChristoffelDiscPrimitive
                          (Option.elim' 1 fun i => TauCeti.boundaryCayley (a i))
                          (Option.elim' (-β - 1) e) ζ +
                      B)
                  (nhdsWithin 1 (Metric.ball 0 1)) (Bornology.cobounded ℂ)
Lean

Formalized in Tau Ceti as TauCeti.exists_bijOn_const_mul_schwarzChristoffelDiscPrimitive_add_of_isJordanCurve_insert_infty.

Sources
LeanTauCeti.exists_bijOn_const_mul_schwarzChristoffelDiscPrimitive_add_of_isJordanCurve_insert_infty
Uses 6
Proof usesCarathéodory's theorem for the inside of a Jordan curve · Rigidity of the pre-Schwarzian derivative · Rouché's theorem for a disc, classical form · Schwarz reflection principle (real axis) · The Schwarz--Christoffel formula · The Schwarz--Christoffel theorem for an unbounded polygonal Jordan domain

TheoremThe discreteness part of Poincaré's polygon theorem#

If a side-paired polygon satisfies the angle condition at every finite vertex cycle and has parabolic cycle transformations at its ideal vertices, then the group generated by its side-pairing maps is a cofinite Fuchsian group: it is discrete and has finite covolume.

TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isCofinite_of_isParabolic {n : ℕ} [NeZero n]
  {P : TauCeti.UpperHalfPlane.ConvexPolygon n} (σ : P.SidePairing)
  (hcyc :
    ∀ (j : Fin n) (z : UpperHalfPlane),
      P.vertex j = Sum.inl z → ↑(orderOf (σ.cycleMap j)) * σ.cycleAngleSum j = 2 * Real.pi)
  (hpar : ∀ (j : Fin n) (ξ : OnePoint ℝ), P.vertex j = Sum.inr ξ → (σ.cycleMap j).IsParabolic) :
  (Subgroup.closure (Set.range σ.map)).IsCofinite
Lean

Formalized in Tau Ceti as TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isCofinite_of_isParabolic.

Sources
LeanTauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isCofinite_of_isParabolic
Uses 2
Proof usesThe Gauss–Bonnet formula · TauCeti.IsLocalTiling

TheoremThe Dolbeault lemma on a disc#

Let f be Cⁿ, n ≥ 1, on the open disc eball c R of radius R ≤ ∞. Then there is a function g, Cⁿ on the disc, with \bar∂ g = f on the disc.

TauCeti.exists_contDiffOn_conjWirtingerDeriv_apply_one_eq_of_eball.{u_1} {W : Type u_1}
  [NormedAddCommGroup W] [NormedSpace ℂ W] [CompleteSpace W] {n : ℕ∞} {f : ℂ → W} {c : ℂ}
  {R : ENNReal} (hn : 1 ≤ n) (hf : ContDiffOn ℝ (↑n) f (Metric.eball c R)) :
  ∃ g,
    ContDiffOn ℝ (↑n) g (Metric.eball c R) ∧
      ∀ z ∈ Metric.eball c R, (TauCeti.conjWirtingerDeriv g z) 1 = f z
Lean

Formalized in Tau Ceti as TauCeti.exists_contDiffOn_conjWirtingerDeriv_apply_one_eq_of_eball.

Other forms

The Dolbeault lemma on a disc of real radius. Formalized in Tau Ceti as TauCeti.exists_contDiffOn_conjWirtingerDeriv_apply_one_eq_of_ball.

TauCeti.exists_contDiffOn_conjWirtingerDeriv_apply_one_eq_of_ball.{u_1} {W : Type u_1}
  [NormedAddCommGroup W] [NormedSpace ℂ W] [CompleteSpace W] {n : ℕ∞} {f : ℂ → W} {c : ℂ} {R : ℝ}
  (hn : 1 ≤ n) (hf : ContDiffOn ℝ (↑n) f (Metric.ball c R)) :
  ∃ g,
    ContDiffOn ℝ (↑n) g (Metric.ball c R) ∧
      ∀ z ∈ Metric.ball c R, (TauCeti.conjWirtingerDeriv g z) 1 = f z

The Dolbeault lemma on the plane. Formalized in Tau Ceti as TauCeti.exists_contDiff_conjWirtingerDeriv_apply_one_eq.

TauCeti.exists_contDiff_conjWirtingerDeriv_apply_one_eq.{u_1} {W : Type u_1} [NormedAddCommGroup W]
  [NormedSpace ℂ W] [CompleteSpace W] {n : ℕ∞} {f : ℂ → W} (hn : 1 ≤ n) (hf : ContDiff ℝ (↑n) f) :
  ∃ g, ContDiff ℝ (↑n) g ∧ ∀ (z : ℂ), (TauCeti.conjWirtingerDeriv g z) 1 = f z
Sources
LeanTauCeti.exists_contDiffOn_conjWirtingerDeriv_apply_one_eq_of_eball · TauCeti.exists_contDiffOn_conjWirtingerDeriv_apply_one_eq_of_ball · TauCeti.exists_contDiff_conjWirtingerDeriv_apply_one_eq
Uses 1
Proof usesThe Cauchy–Pompeiu formula for a compactly supported C¹ map u : ℂ → F

TheoremThe explicit Schwarz--Christoffel formula for a strip#

Two distinct prevertices of exponent -1 give the principal logarithm of their fractional-linear ratio, after scaling by their separation and translating by the value at the base point.

TauCeti.const_mul_schwarzChristoffelPrimitive_two_neg_one_add_eq_log (a : Fin 2 → ℝ)
  (ha : a 0 ≠ a 1) (z₀ : UpperHalfPlane) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) :
  (↑(a 1) - ↑(a 0)) * TauCeti.schwarzChristoffelPrimitive a (fun x => -1) z₀ z +
      Complex.log ((↑z₀ - ↑(a 1)) / (↑z₀ - ↑(a 0))) =
    Complex.log ((z - ↑(a 1)) / (z - ↑(a 0)))
Lean

Formalized in Tau Ceti as TauCeti.const_mul_schwarzChristoffelPrimitive_two_neg_one_add_eq_log.

Sources
LeanTauCeti.const_mul_schwarzChristoffelPrimitive_two_neg_one_add_eq_log

TheoremThe fundamental-set part of Poincaré's polygon theorem#

If a side-paired polygon satisfies the angle condition at every finite vertex cycle and has parabolic cycle transformations at its ideal vertices, then it is a measurable fundamental domain for the group generated by its side-pairing maps.

TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isFundamentalDomain_carrier_of_isParabolic {n : ℕ}
  [NeZero n] {P : TauCeti.UpperHalfPlane.ConvexPolygon n} (σ : P.SidePairing)
  (hcyc :
    ∀ (j : Fin n) (z : UpperHalfPlane),
      P.vertex j = Sum.inl z → ↑(orderOf (σ.cycleMap j)) * σ.cycleAngleSum j = 2 * Real.pi)
  (hpar : ∀ (j : Fin n) (ξ : OnePoint ℝ), P.vertex j = Sum.inr ξ → (σ.cycleMap j).IsParabolic) :
  MeasureTheory.IsFundamentalDomain (↥(Subgroup.closure (Set.range σ.map))) P.carrier
    MeasureTheory.volume
Lean

Formalized in Tau Ceti as TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isFundamentalDomain_carrier_of_isParabolic.

Sources
LeanTauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isFundamentalDomain_carrier_of_isParabolic
Uses 1
Proof usesTauCeti.IsLocalTiling

TheoremGauss–Bonnet for the triangles of the fan from ∞#

If vertex 0 is ∞, the part of the carrier between the verticals through vertex i and vertex (i + 1), for an side i not ending at ∞, has area π minus the angles at vertex i and vertex (i + 1) of the triangle with vertices ∞, vertex i, vertex (i + 1). That part of the carrier is this triangle by exists_carrier_inter_strip_eq.

TauCeti.UpperHalfPlane.ConvexPolygon.volume_carrier_inter_strip {n : ℕ} [NeZero n]
  (P : TauCeti.UpperHalfPlane.ConvexPolygon n) (h₀ : P.vertex 0 = Sum.inr OnePoint.infty)
  {i : Fin n} (hi : i ≠ 0) (hi' : i + 1 ≠ 0) :
  MeasureTheory.volume
      (P.carrier ∩
        {z |
          (TauCeti.UpperHalfPlane.toComplex (P.vertex i)).re ≤ z.re ∧
            z.re ≤ (TauCeti.UpperHalfPlane.toComplex (P.vertex (i + 1))).re}) =
    ENNReal.ofReal
      (Real.pi -
          TauCeti.UpperHalfPlane.vertexAngle (P.vertex i) (Sum.inr OnePoint.infty)
            (P.vertex (i + 1)) -
        TauCeti.UpperHalfPlane.vertexAngle (P.vertex (i + 1)) (P.vertex i) (Sum.inr OnePoint.infty))
Lean

Formalized in Tau Ceti as TauCeti.UpperHalfPlane.ConvexPolygon.volume_carrier_inter_strip.

Sources
LeanTauCeti.UpperHalfPlane.ConvexPolygon.volume_carrier_inter_strip
Used by 1
Used byThe Gauss–Bonnet formula

TheoremThe Gauss–Bonnet formula#

the invariant area of a hyperbolic triangle is its angular defect π - α - β - γ.

TauCeti.UpperHalfPlane.volume_triangle {A B C : UpperHalfPlane} (hAB : A ≠ B)
  (hC :
    C ∉
      Set.range
        (TauCeti.UpperHalfPlane.geodesicLine (TauCeti.UpperHalfPlane.geodesicBetween A B))) :
  MeasureTheory.volume (A.triangle B C) =
    ENNReal.ofReal (Real.pi - A.interiorAngle B C - B.interiorAngle C A - C.interiorAngle A B)
Lean

Formalized in Tau Ceti as TauCeti.UpperHalfPlane.volume_triangle.

Other forms

The Gauss–Bonnet formula for compact convex hyperbolic polygons. Formalized in Tau Ceti as TauCeti.UpperHalfPlane.CompactConvexPolygon.volume_carrier.

TauCeti.UpperHalfPlane.CompactConvexPolygon.volume_carrier {n : ℕ} [NeZero n]
  (P : TauCeti.UpperHalfPlane.CompactConvexPolygon n) :
  MeasureTheory.volume P.carrier = ENNReal.ofReal ((↑n - 2) * Real.pi - ∑ i, P.interiorAngle i)

The Gauss–Bonnet formula for convex hyperbolic polygons with ideal vertices. Formalized in Tau Ceti as TauCeti.UpperHalfPlane.ConvexPolygon.volume_carrier.

TauCeti.UpperHalfPlane.ConvexPolygon.volume_carrier {n : ℕ} [NeZero n]
  (P : TauCeti.UpperHalfPlane.ConvexPolygon n) :
  MeasureTheory.volume P.carrier = ENNReal.ofReal ((↑n - 2) * Real.pi - ∑ i, P.interiorAngle i)
Sources
LeanTauCeti.UpperHalfPlane.volume_triangle · TauCeti.UpperHalfPlane.CompactConvexPolygon.volume_carrier · TauCeti.UpperHalfPlane.ConvexPolygon.volume_carrier
Uses 1 · Used by 5
Proof usesGauss–Bonnet for the triangles of the fan from ∞
Used byCompactness from a Dirichlet domain with a bounded cusp truncation · Dirichlet presentations of cocompact Fuchsian groups · The converse of Poincaré's polygon theorem · The orbifold area formula for a fundamental polygon · The discreteness part of Poincaré's polygon theorem

TheoremThe Herglotz formula on a disc#

a function holomorphic on a disc and continuous up to its boundary is the Herglotz–Riesz integral of its boundary real part, plus the imaginary constant (f c).im * I. Unlike the Poisson formula, which recovers f from all of its boundary values, this recovers f from the boundary values of its real part alone.

DiffContOnCl.circleAverage_herglotzRieszKernel_smul_re_add {f : ℂ → ℂ} {c w : ℂ} {R : ℝ}
  (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hw : w ∈ Metric.ball c R) :
  Real.circleAverage (fun ζ => herglotzRieszKernel c w ζ • ↑(f ζ).re) c R + ↑(f c).im * Complex.I =
    f w
Lean

Formalized in Tau Ceti as DiffContOnCl.circleAverage_herglotzRieszKernel_smul_re_add.

Sources
LeanDiffContOnCl.circleAverage_herglotzRieszKernel_smul_re_add
Used by 1
Used byThe Herglotz representation theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.