Documentation

TauCeti.Analysis.Complex.Conformal.UnitDisc.Automorphism.Basic

Standard automorphisms of the complex unit disc #

This file adds the rotation factor in the standard disc-automorphism formula z ↦ u * (z - a) / (1 - conj a * z), with u on the unit circle and a in the unit disc. The previous Moebius file supplies the factor sending a to 0; this file composes it with Mathlib's Circle action on Complex.UnitDisc.

This advances the conformal-mapping roadmap's L2 disc-automorphism target. It reuses Mathlib's Circle action on Complex.UnitDisc and Tau Ceti's unitDiscMoebiusEquiv.

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.

source
noncomputable def TauCeti.unitDiscStandardAutomorphismEquiv (u : Circle) (a : Complex.UnitDisc) :
Complex.UnitDisc ≃ Complex.UnitDisc

The standard automorphism of the complex unit disc z ↦ u * (z - a) / (1 - conj a * z).

The center-removing factor is unitDiscMoebiusEquiv a; the circle element u supplies the rotation factor in the usual classification formula for disc automorphisms.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.unitDiscStandardAutomorphismEquiv_apply (u : Circle) (a z : Complex.UnitDisc) :
    (unitDiscStandardAutomorphismEquiv u a) z = u • unitDiscMoebius a z

    The standard automorphism applies by first sending a to 0, then rotating.

    source
    theorem TauCeti.coe_unitDiscStandardAutomorphismEquiv_apply (u : Circle) (a z : Complex.UnitDisc) :
    ↑((unitDiscStandardAutomorphismEquiv u a) z) = ↑u * ((↑z - ↑a) / (1 - (starRingEnd ℂ) ↑a * ↑z))

    The scalar formula for the standard disc automorphism.

    source
    @[simp]
    theorem TauCeti.unitDiscStandardAutomorphismEquiv_zero (u : Circle) :
    unitDiscStandardAutomorphismEquiv u 0 = MulAction.toPerm u

    With zero center, the standard automorphism is just rotation.

    source
    @[simp]
    theorem TauCeti.unitDiscStandardAutomorphismEquiv_one (a : Complex.UnitDisc) :
    unitDiscStandardAutomorphismEquiv 1 a = unitDiscMoebiusEquiv a

    With unit rotation factor, the standard automorphism is the Moebius equivalence.

    source
    theorem TauCeti.unitDiscStandardAutomorphismEquiv_self (u : Circle) (a : Complex.UnitDisc) :
    (unitDiscStandardAutomorphismEquiv u a) a = 0

    The standard automorphism sends its center to zero.

    source
    theorem TauCeti.unitDiscStandardAutomorphismEquiv_apply_zero (u : Circle) (a : Complex.UnitDisc) :
    (unitDiscStandardAutomorphismEquiv u a) 0 = u • -a

    The standard automorphism sends zero to -u * a.

    source
    theorem TauCeti.norm_unitDiscStandardAutomorphismEquiv (u : Circle) (a z : Complex.UnitDisc) :
    ‖↑((unitDiscStandardAutomorphismEquiv u a) z)‖ = pseudoHyperbolicExpr ↑z ↑a

    The norm of a standard automorphism value is the pseudo-hyperbolic expression.

    source
    theorem TauCeti.unitDiscStandardAutomorphismEquiv_eq_zero_iff (u : Circle) (a z : Complex.UnitDisc) :
    (unitDiscStandardAutomorphismEquiv u a) z = 0 ↔ z = a

    A standard disc automorphism vanishes exactly at its center.

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

    The scalar formula of a standard automorphism is holomorphic on the unit disc.

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

    The scalar formula of the standard automorphism is holomorphic on the unit disc.

    source
    theorem TauCeti.eq_zero_and_eq_one_of_unitDiscStandardAutomorphismFormula_eq_self {u c w₁ w₂ w₃ : ℂ} (h₁₂ : w₁ ≠ w₂) (h₁₃ : w₁ ≠ w₃) (h₂₃ : w₂ ≠ w₃) (hd₁ : 1 - (starRingEnd ℂ) c * w₁ ≠ 0) (hd₂ : 1 - (starRingEnd ℂ) c * w₂ ≠ 0) (hd₃ : 1 - (starRingEnd ℂ) c * w₃ ≠ 0) (h₁ : u * ((w₁ - c) / (1 - (starRingEnd ℂ) c * w₁)) = w₁) (h₂ : u * ((w₂ - c) / (1 - (starRingEnd ℂ) c * w₂)) = w₂) (h₃ : u * ((w₃ - c) / (1 - (starRingEnd ℂ) c * w₃)) = w₃) :
    c = 0 ∧ u = 1

    A standard disc-automorphism formula w ↦ u * (w - c) / (1 - conj c * w) that fixes three distinct points at which its denominator does not vanish is the identity: c = 0 and u = 1.

    source
    @[simp]
    theorem TauCeti.unitDiscStandardAutomorphismEquiv_symm (u : Circle) (a : Complex.UnitDisc) :
    (unitDiscStandardAutomorphismEquiv u a).symm = Equiv.trans (MulAction.toPerm u⁻¹) (unitDiscMoebiusEquiv (-a))

    The inverse of a standard automorphism as a composition of the inverse rotation and the inverse Moebius factor.