Unit-disc Moebius factors

This file packages the standard Moebius factor z ↦ (z - a) / (1 - conj a * z) as a bundled self-map of the complex unit disc. It is the elementary automorphism API used by the Schwarz--Pick and disc-automorphism layer of the conformal-mapping roadmap: the map sends a to 0, its norm is the pseudo-hyperbolic expression from z to a, and the inverse is the factor with center -a. The same map is also bundled as an equivalence and as a homeomorphism of the unit disc.

This L2 material is coordinated with the upstream Mathlib RMT effort in leanprover-community/mathlib4#33505. Mathlib already contains the preceding human-curated work in Analysis/Complex/RiemannMapping.lean and Analysis/Complex/BranchLogRoot.lean; this file only adds the small discoverable API around Complex.UnitDisc.

noncomputable def TauCeti.unitDiscMoebius (a z : Complex.UnitDisc) : Complex.UnitDisc

The standard Moebius factor of the unit disc sending a to 0.

Equations

• TauCeti.unitDiscMoebius a z = Complex.UnitDisc.mk ((↑z - ↑a) / (1 - (starRingEnd ℂ) ↑a * ↑z)) ⋯

@[simp]

theorem TauCeti.coe_unitDiscMoebius (a z : Complex.UnitDisc) : ↑(unitDiscMoebius a z) = (↑z - ↑a) / (1 - (starRingEnd ℂ) ↑a * ↑z)

The defining formula for the unit-disc Moebius factor.

@[simp]

theorem TauCeti.unitDiscMoebius_zero (z : Complex.UnitDisc) : unitDiscMoebius 0 z = z

The unit-disc Moebius factor centered at zero is the identity.

@[simp]

theorem TauCeti.unitDiscMoebius_self (a : Complex.UnitDisc) : unitDiscMoebius a a = 0

The unit-disc Moebius factor sends its center to zero.

@[simp]

theorem TauCeti.unitDiscMoebius_apply_zero (a : Complex.UnitDisc) : unitDiscMoebius a 0 = -a

The unit-disc Moebius factor sends zero to the negative of its center.

theorem TauCeti.norm_unitDiscMoebius (a z : Complex.UnitDisc) : ‖↑(unitDiscMoebius a z)‖ = pseudoHyperbolicExpr ↑z ↑a

The norm of the Moebius factor is the pseudo-hyperbolic expression.

@[simp]

theorem TauCeti.unitDiscMoebius_eq_zero_iff (a z : Complex.UnitDisc) : unitDiscMoebius a z = 0 ↔ z = a

A unit-disc Moebius factor vanishes exactly at its center.

theorem TauCeti.mapsTo_ball_unitDiscMoebiusFormula_of_norm_lt_one {a : ℂ} (ha : ‖a‖ < 1) : Set.MapsTo (fun (z : ℂ) => (z - a) / (1 - (starRingEnd ℂ) a * z)) (Metric.ball 0 1) (Metric.ball 0 1)

The scalar unit-disc Moebius formula maps the open unit disc to itself.

theorem TauCeti.mapsTo_ball_unitDiscMoebiusFormula (a : Complex.UnitDisc) : Set.MapsTo (fun (z : ℂ) => (z - ↑a) / (1 - (starRingEnd ℂ) ↑a * z)) (Metric.ball 0 1) (Metric.ball 0 1)

The scalar formula of a unit-disc Moebius factor maps the open unit disc to itself.

theorem TauCeti.differentiableOn_unitDiscMoebiusFormula_of_norm_lt_one {a : ℂ} (ha : ‖a‖ < 1) : DifferentiableOn ℂ (fun (z : ℂ) => (z - a) / (1 - (starRingEnd ℂ) a * z)) (Metric.ball 0 1)

The scalar Moebius formula with center of norm less than one is holomorphic on the unit disc.

theorem TauCeti.hasDerivAt_unitDiscMoebiusFormula (a p : ℂ) (hp : 1 - (starRingEnd ℂ) a * p ≠ 0) : HasDerivAt (fun (z : ℂ) => (z - a) / (1 - (starRingEnd ℂ) a * z)) ((1 - (starRingEnd ℂ) a * a) / (1 - (starRingEnd ℂ) a * p) ^ 2) p

The complex derivative of the scalar unit-disc Moebius factor z ↦ (z - a) / (1 - conj a * z) at a point p where the denominator is nonzero. Its value at p = 0 (with center -z) is 1 - ‖z‖ ^ 2, and at p = a it is 1 / (1 - ‖a‖ ^ 2), the two factors that appear in the infinitesimal Schwarz--Pick estimate.

theorem TauCeti.unitDiscMoebiusFormula_sub_unitDiscMoebiusFormula (a : ℂ) {s t : ℂ} (hs : 1 - (starRingEnd ℂ) a * s ≠ 0) (ht : 1 - (starRingEnd ℂ) a * t ≠ 0) : (s - a) / (1 - (starRingEnd ℂ) a * s) - (t - a) / (1 - (starRingEnd ℂ) a * t) = (1 - (starRingEnd ℂ) a * a) * (s - t) / ((1 - (starRingEnd ℂ) a * s) * (1 - (starRingEnd ℂ) a * t))

The scalar unit-disc Moebius factor z ↦ (z - a) / (1 - conj a * z) has the difference quotient (1 - conj a * a) / ((1 - conj a * s) * (1 - conj a * t)).

theorem TauCeti.differentiableOn_unitDiscMoebiusFormula (a : Complex.UnitDisc) : DifferentiableOn ℂ (fun (z : ℂ) => (z - ↑a) / (1 - (starRingEnd ℂ) ↑a * z)) (Metric.ball 0 1)

The scalar formula of the unit-disc Moebius factor is holomorphic on the unit disc.

@[simp]

theorem TauCeti.unitDiscMoebius_neg_comp_unitDiscMoebius (a : Complex.UnitDisc) : unitDiscMoebius (-a) ∘ unitDiscMoebius a = id

The inverse of the unit-disc Moebius factor centered at a is the factor centered at -a.

@[simp]

theorem TauCeti.unitDiscMoebius_comp_unitDiscMoebius_neg (a : Complex.UnitDisc) : unitDiscMoebius a ∘ unitDiscMoebius (-a) = id

The unit-disc Moebius factors centered at a and -a compose in the other order too.

theorem TauCeti.leftInvOn_unitDiscMoebiusFormula_of_norm_lt_one {a : ℂ} (ha : ‖a‖ < 1) : Set.LeftInvOn (fun (z : ℂ) => (z - -a) / (1 - (starRingEnd ℂ) (-a) * z)) (fun (z : ℂ) => (z - a) / (1 - (starRingEnd ℂ) a * z)) (Metric.ball 0 1)

The scalar unit-disc Moebius formula centered at -a is a left inverse for the scalar formula centered at a on the open unit disc.

noncomputable def TauCeti.unitDiscMoebiusEquiv (a : Complex.UnitDisc) : Complex.UnitDisc ≃ Complex.UnitDisc

The standard Moebius self-equivalence of the unit disc sending a to 0.

Equations

• TauCeti.unitDiscMoebiusEquiv a = { toFun := TauCeti.unitDiscMoebius a, invFun := TauCeti.unitDiscMoebius (-a), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.unitDiscMoebiusEquiv_apply (a z : Complex.UnitDisc) : (unitDiscMoebiusEquiv a) z = unitDiscMoebius a z

The equivalence applies by the unit-disc Moebius formula.

@[simp]

theorem TauCeti.unitDiscMoebiusEquiv_symm (a : Complex.UnitDisc) : (unitDiscMoebiusEquiv a).symm = unitDiscMoebiusEquiv (-a)

The inverse equivalence is the Moebius equivalence centered at -a.

theorem TauCeti.continuous_unitDiscMoebius (a : Complex.UnitDisc) : Continuous (unitDiscMoebius a)

The unit-disc Moebius factor is continuous as a map of the bundled open disc.

noncomputable def TauCeti.unitDiscMoebiusHomeomorph (a : Complex.UnitDisc) : Complex.UnitDisc ≃ₜ Complex.UnitDisc

The standard Moebius self-map of the unit disc, bundled as a homeomorphism.

Equations

• TauCeti.unitDiscMoebiusHomeomorph a = { toEquiv := TauCeti.unitDiscMoebiusEquiv a, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.unitDiscMoebiusHomeomorph_apply (a z : Complex.UnitDisc) : (unitDiscMoebiusHomeomorph a) z = unitDiscMoebius a z

The Moebius homeomorphism applies by the existing Moebius factor.

@[simp]

theorem TauCeti.unitDiscMoebiusHomeomorph_toEquiv (a : Complex.UnitDisc) : (unitDiscMoebiusHomeomorph a).toEquiv = unitDiscMoebiusEquiv a

The underlying equivalence of the Moebius homeomorphism is the existing equivalence.

@[simp]

theorem TauCeti.unitDiscMoebiusHomeomorph_symm (a : Complex.UnitDisc) : (unitDiscMoebiusHomeomorph a).symm = unitDiscMoebiusHomeomorph (-a)

The inverse Moebius homeomorphism is the Moebius homeomorphism centered at -a.

theorem TauCeti.coe_unitDiscMoebiusHomeomorph_apply (a z : Complex.UnitDisc) : ↑((unitDiscMoebiusHomeomorph a) z) = (↑z - ↑a) / (1 - (starRingEnd ℂ) ↑a * ↑z)

The scalar formula for the Moebius homeomorphism.