Reflection in a circle

This file connects Mathlib's Euclidean inversion to the conjugate-reciprocal formula for reflection in a circle in ℂ. It also packages the restriction to the punctured plane as a homeomorphism and records the inside/outside behavior needed for Schwarz reflection.

theorem TauCeti.inversion_eq_conj_reciprocal (c : ℂ) (r : ℝ) (z : ℂ) : EuclideanGeometry.inversion c r z = c + ↑r ^ 2 / (starRingEnd ℂ) (z - c)

Euclidean inversion in ℂ is given by the standard conjugate-reciprocal formula for reflection in a circle.

noncomputable def TauCeti.circleReflectionHomeomorph (c : ℂ) (r : ℝ) (hr : r ≠ 0) : ↑{c}ᶜ ≃ₜ ↑{c}ᶜ

Euclidean inversion restricts to a self-homeomorphism of the punctured complex plane.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coe_circleReflectionHomeomorph_apply (c : ℂ) (r : ℝ) (hr : r ≠ 0) (z : ↑{c}ᶜ) : ↑((circleReflectionHomeomorph c r hr) z) = EuclideanGeometry.inversion c r ↑z

The punctured-plane circle-reflection homeomorphism acts by Euclidean inversion.

@[simp]

theorem TauCeti.circleReflectionHomeomorph_symm (c : ℂ) (r : ℝ) (hr : r ≠ 0) : (circleReflectionHomeomorph c r hr).symm = circleReflectionHomeomorph c r hr

The punctured-plane circle-reflection homeomorphism is its own inverse.

@[simp]

theorem TauCeti.dist_inversion_center_lt_iff {c z : ℂ} {r : ℝ} (hr : 0 < r) (hz : z ≠ c) : dist (EuclideanGeometry.inversion c r z) c < r ↔ r < dist z c

Inversion in a positive-radius circle sends a point into its open ball exactly when the original point is in the exterior of its closed ball.

@[simp]

theorem TauCeti.lt_dist_inversion_center_iff {c z : ℂ} {r : ℝ} (hr : 0 < r) (hz : z ≠ c) : r < dist (EuclideanGeometry.inversion c r z) c ↔ dist z c < r

Inversion in a positive-radius circle sends a point outside its closed ball exactly when the original point is in its open ball.