Complex conjugation: invariant discs, symmetric norms and unit-norm quotients

Complex conjugation is an isometry fixing the real axis (Mathlib's Complex.dist_conj_conj), so it maps every open or closed disc centred on the real axis to itself. Such discs are the natural domains for reflection across the real axis, for instance the even reflection TauCeti.evenReflection. Conjugation maps the real axis into itself (TauCeti.mapsTo_conj_setOf_im_eq_zero), whereas the rotation z ↦ I z does not (TauCeti.not_mapsTo_I_mul_setOf_im_eq_zero).

Conjugation also preserves norms (Mathlib's Complex.norm_conj), so the norm of 1 - conj w * z is symmetric in z and w (Complex.norm_one_sub_conj_mul_comm). This expression is the denominator of the Möbius automorphisms of the unit disc and of the pseudo-hyperbolic expression.

Inversion preserves the open right half-plane: z⁻¹ has positive real part exactly when z does (Complex.inv_re_pos).

The scalar Cayley expression 1 + (z - conj z) / (r - z) has unit norm for real r. When z ≠ r, it is the quotient (r - conj z) / (r - z) of a complex number's conjugate by itself; at z = r, Lean's totalized inverse gives value one.

Two integers whose images in ℂ are at distance less than 1 are equal.

theorem Complex.inv_re_pos {z : ℂ} : 0 < z⁻¹.re ↔ 0 < z.re

A complex number and its inverse lie in the open right half-plane together.

theorem Complex.norm_one_add_sub_conj_mul_inv_ofReal_sub (z : ℂ) (r : ℝ) : ‖1 + (z - (starRingEnd ℂ) z) * (↑r - z)⁻¹‖ = 1

The scalar Cayley expression has unit norm at real r, including when z = r under the totalized inverse convention.

theorem TauCeti.conj_mem_ball_of_im_eq_zero {x₀ z : ℂ} {r : ℝ} (hx₀ : x₀.im = 0) (hz : z ∈ Metric.ball x₀ r) : (starRingEnd ℂ) z ∈ Metric.ball x₀ r

Conjugation maps an open disc centred on the real axis to itself.

theorem TauCeti.conj_mem_closedBall_of_im_eq_zero {x₀ z : ℂ} {r : ℝ} (hx₀ : x₀.im = 0) (hz : z ∈ Metric.closedBall x₀ r) : (starRingEnd ℂ) z ∈ Metric.closedBall x₀ r

Conjugation maps a closed disc centred on the real axis to itself.

theorem TauCeti.mapsTo_conj_setOf_im_eq_zero : Set.MapsTo (fun (x : ℂ) => (starRingEnd ℂ) x) {z : ℂ | z.im = 0} {z : ℂ | z.im = 0}

Complex conjugation maps the real axis into itself.

theorem TauCeti.not_mapsTo_I_mul_setOf_im_eq_zero : ¬Set.MapsTo (fun (z : ℂ) => Complex.I * z) {z : ℂ | z.im = 0} {z : ℂ | z.im = 0}

The rotation z ↦ I z does not preserve the real axis, so it is not admissible on half-discs.

theorem TauCeti.continuousOn_mapsTo_prodMap_conj {E : Type u_1} [TopologicalSpace E] {τ : E → E} {U : Set E} {ρ : ℝ} (hτ : ContinuousOn τ U) (hτU : Set.MapsTo τ U U) : ContinuousOn (fun (b : E × ℂ) => (τ b.1, (starRingEnd ℂ) b.2)) (U ×ˢ Metric.ball 0 ρ) ∧ Set.MapsTo (fun (b : E × ℂ) => (τ b.1, (starRingEnd ℂ) b.2)) (U ×ˢ Metric.ball 0 ρ) (U ×ˢ Metric.ball 0 ρ) ∧ Set.MapsTo (fun (b : E × ℂ) => (τ b.1, (starRingEnd ℂ) b.2)) (U ×ˢ (Metric.ball 0 ρ \ {0})) (U ×ˢ (Metric.ball 0 ρ \ {0}))

The parameter map τ composed with conjugation of the disc coordinate is continuous on the product of U with a disc centred at zero, and maps this product and its punctured version to themselves.

theorem TauCeti.eq_of_dist_intCast_lt_one {m n : ℤ} (h : dist ↑m ↑n < 1) : m = n

Two integers whose complex images are closer than 1 are equal.

theorem Complex.norm_one_sub_conj_mul_comm (z w : ℂ) : ‖1 - (starRingEnd ℂ) w * z‖ = ‖1 - (starRingEnd ℂ) z * w‖

The norm of 1 - conj w * z is symmetric in z and w: conjugation swaps the two expressions and preserves norms.