Basic API for the complex unit disc

This file collects small API lemmas for Mathlib's Complex.UnitDisc. It covers the transport between a self-map of the bundled disc and a scalar representative ℂ → ℂ of it — such a representative maps Metric.ball 0 1 into itself, and bijectively onto itself when the bundled map is an equivalence — together with the basic properties of the Circle action on the disc: the disc is nontrivial, a rotation is determined by its value at any one nonzero point, and hence the circle acts faithfully. It also records the slit-plane criterion TauCeti.one_sub_div_mem_slitPlane for a disc point and a circle point. It also records that a point of the open disc differs from every point of norm one.

theorem TauCeti.hasDerivAt_one_sub_div (w ζ : ℂ) : HasDerivAt (fun (ξ : ℂ) => 1 - ξ / w) (-w⁻¹) ζ

The derivative of the affine factor 1 - ξ / w for a complex number w.

theorem TauCeti.ne_of_mem_ball_of_norm_eq_one {ζ w : ℂ} (hζ : ζ ∈ Metric.ball 0 1) (hw : ‖w‖ = 1) : ζ ≠ w

A point of the open unit disc differs from every point of norm one.

theorem TauCeti.one_sub_div_mem_slitPlane (w : Circle) {ζ : ℂ} (hζ : ζ ∈ Metric.ball 0 1) : 1 - ζ / ↑w ∈ Complex.slitPlane

For w on the unit circle and ζ in the open unit disc, 1 - ζ / w lies in the slit plane, since ζ / w has norm less than one.

@[simp]

theorem TauCeti.Complex.UnitDisc.circle_smul_zero (u : Circle) : u • 0 = 0

Rotating the disc origin by a circle element fixes it. This is the smul_zero normalization for Mathlib's Circle action on Complex.UnitDisc, which is a bare MulAction and so does not get the generic smul_zero simp lemma.

@[simp]

theorem TauCeti.Complex.UnitDisc.circle_smul_eq_zero_iff (u : Circle) {z : Complex.UnitDisc} : u • z = 0 ↔ z = 0

A circle rotation of a disc point vanishes exactly when the point does. This is the smul_eq_zero normalization for Mathlib's Circle action on Complex.UnitDisc.

theorem TauCeti.Complex.UnitDisc.isCompact_setOf_norm_le {ρ : ℝ} (hρ : ρ < 1) : IsCompact {z : Complex.UnitDisc | ‖↑z‖ ≤ ρ}

The set of unit-disc points of Euclidean norm at most ρ < 1 is compact: it is carried by the embedding into ℂ onto the closed Euclidean ball of radius ρ, which the hypothesis ρ < 1 places inside the open disc.

theorem TauCeti.mapsTo_ball_of_forall_unitDisc_coe_eq {e : Complex.UnitDisc → Complex.UnitDisc} {f : ℂ → ℂ} (hf : ∀ (z : Complex.UnitDisc), ↑(e z) = f ↑z) : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)

A scalar representative of a self-map of the disc maps the open unit ball into itself.

theorem TauCeti.bijOn_ball_of_unitDiscEquiv (E : Complex.UnitDisc ≃ Complex.UnitDisc) {φ : ℂ → ℂ} (hφ : ∀ (z : Complex.UnitDisc), ↑(E z) = φ ↑z) : Set.BijOn φ (Metric.ball 0 1) (Metric.ball 0 1)

A self-equivalence of Complex.UnitDisc, read through a scalar representative, is a bijection of Metric.ball 0 1 onto itself.

theorem TauCeti.continuous_circle_smul_unitDisc (u : Circle) : Continuous fun (z : Complex.UnitDisc) => u • z

A fixed circle rotation is continuous on the bundled open disc.

instance TauCeti.instContinuousConstSMulCircleUnitDisc : ContinuousConstSMul Circle Complex.UnitDisc

Circle rotations act continuously on the bundled open unit disc.

instance TauCeti.instNontrivialUnitDisc : Nontrivial Complex.UnitDisc

The open unit disc has more than one point: 0 and 1 / 2 are both in it.

theorem TauCeti.circle_smul_left_injective {z : Complex.UnitDisc} (hz : z ≠ 0) : Function.Injective fun (u : Circle) => u • z

A rotation is determined by its value at a single nonzero point of the disc. Multiplication by a nonzero complex number is injective, and the disc inherits that from ℂ.

instance TauCeti.instFaithfulSMulCircleUnitDisc : FaithfulSMul Circle Complex.UnitDisc

The circle acts faithfully on the unit disc. Only the trivial rotation fixes the whole disc, because the disc contains a nonzero point.