Heights above a semicircle centred on the real axis

Let z ∈ ℍ lie on or above the semicircle of centre m ∈ ℝ and radius ρ, that is ρ² ≤ |z - m|². This file bounds the height Im z from below when Re z lies between m and an endpoint of an arc of that semicircle.

• If the endpoint is a point p ∈ ℍ of the semicircle, then Im p ≤ Im z (TauCeti.UpperHalfPlane.im_le_im_of_normSq_sub_eq).
• If the endpoint is the real point x where the semicircle meets ℝ, the height is not bounded below near x, but it satisfies ρ |Re z - x| ≤ (Im z)². Hence it is bounded below outside a horodisc at x: if Im z ≤ K |z - x|² with K > 0, then min ρ (1 / (2K)) ≤ Im z (TauCeti.UpperHalfPlane.min_le_im_of_sq_sub_eq).

These are the estimates that make a convex polygon truncated at its ideal vertices compact.

theorem TauCeti.UpperHalfPlane.im_le_im_of_normSq_sub_eq {m ρ : ℝ} {p z : UpperHalfPlane} (hp : Complex.normSq (↑p - ↑m) = ρ ^ 2) (hz : ρ ^ 2 ≤ Complex.normSq (↑z - ↑m)) (hre : (z.re - p.re) * (z.re - m) ≤ 0) : p.im ≤ z.im

Above a semicircle of centre m through the point p ∈ ℍ, the height of a point whose real part lies between Re p and m is at least that of p.

theorem TauCeti.UpperHalfPlane.min_le_im_of_sq_sub_eq {m ρ x K : ℝ} {z : UpperHalfPlane} (hρ : 0 < ρ) (hK : 0 < K) (hx : (x - m) ^ 2 = ρ ^ 2) (hz : ρ ^ 2 ≤ Complex.normSq (↑z - ↑m)) (hre : (z.re - x) * (z.re - m) ≤ 0) (hh : z.im ≤ K * Complex.normSq (↑z - ↑x)) : min ρ (1 / (2 * K)) ≤ z.im

Above a semicircle of centre m and radius ρ ending at the real point x, a point z whose real part lies between x and m, and which lies outside the horodisc Im z > K |z - x|² at x, has height at least min ρ (1 / (2K)).