Topology of the upper half-plane

Every real point lies in the closure of the open upper half-plane, so limits taken along the half-plane at a real point are well posed. The half-plane is also unbounded, so the filter along which it approaches infinity is nontrivial and limits taken along it are unique.

For a function conjugation-symmetric near infinity, decay along the upper half-plane implies decay along the whole plane, provided it is continuous at sufficiently distant real points.

A continuous injection of the closed upper half-plane sends every real point to the frontier of the image of the open half-plane. The inversion w ↦ -w⁻¹ preserves the closed upper half-plane, and so transfers limits at infinity in it to limits at 0.

A function on the upper half-plane, extended to ℂ by ofComplex, is periodic with a real period exactly when the original function is invariant under the corresponding translation.

The real-part map re : ℍ → ℝ is continuous and open, so taking closures commutes with taking preimages under it. In particular the closure of the open half-plane {z | a < z.re} is the closed half-plane {z | a ≤ z.re}, and likewise for {z | z.re < a}; transported by the PSL(2, ℝ)-action, this identifies the boundary of a half-plane bounded by a geodesic line.

Main declarations

• Real.nhdsWithin_upperHalfPlaneSet_neBot.
• TauCeti.mem_closedBall_and_eq_of_tendsto — transport a boundary limit through a map continuous on the closed unit disc.
• TauCeti.cobounded_inf_principal_upperHalfPlaneSet_neBot.
• TauCeti.tendsto_zero_cobounded_of_tendsto_upperHalfPlaneSet.
• TauCeti.tendsto_zero_cobounded_of_tendsto_mul_upperHalfPlaneSet.
• TauCeti.mem_frontier_image_upperHalfPlaneSet_of_im_eq_zero.
• TauCeti.not_mem_image_upperHalfPlaneSet_of_im_eq_zero.
• TauCeti.im_neg_inv_nonneg.
• TauCeti.tendsto_comp_neg_inv_cobounded.
• TauCeti.UpperHalfPlane.periodic_comp_ofComplex_iff.
• TauCeti.UpperHalfPlane.closure_preimage_re, closure_setOfPred_lt_re, closure_setOfPred_re_lt.

References

• Mathlib PR #39083 (Chris Birkbeck) — the upstream draft the periodicity criterion ports onto the current Mathlib pin.

theorem Real.nhdsWithin_upperHalfPlaneSet_neBot (x : ℝ) : (nhdsWithin (↑x) UpperHalfPlane.upperHalfPlaneSet).NeBot

Every real point is in the closure of the open upper half-plane, so limits along the half-plane at a real point are well posed.

theorem TauCeti.mem_closedBall_and_eq_of_tendsto {G h f : ℂ → ℂ} {x : ℝ} {w : ℂ} (hGc : ContinuousOn G (Metric.closedBall 0 1)) (hh : ContinuousAt h ↑x) (hmaps : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, h z ∈ Metric.ball 0 1) (hf : ∀ z ∈ UpperHalfPlane.upperHalfPlaneSet, f z = G (h z)) (hfw : Filter.Tendsto f (nhdsWithin (↑x) UpperHalfPlane.upperHalfPlaneSet) (nhds w)) : h ↑x ∈ Metric.closedBall 0 1 ∧ G (h ↑x) = w

Along the upper half-plane, a limit of f = G ∘ h at a real point x is G (h x), when h is continuous at x and maps the upper half-plane into the disc, on whose closure G is continuous.

instance TauCeti.cobounded_inf_principal_upperHalfPlaneSet_neBot : (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet).NeBot

The upper half-plane is unbounded, so the filter along which it approaches infinity is nontrivial and limits taken along it are unique.

theorem TauCeti.tendsto_zero_cobounded_of_tendsto_upperHalfPlaneSet {φ : ℂ → ℂ} (hcont : ∀ᶠ (z : ℂ) in Bornology.cobounded ℂ, z.im = 0 → ContinuousAt φ z) (hconj : ∀ᶠ (z : ℂ) in Bornology.cobounded ℂ, φ ((starRingEnd ℂ) z) = (starRingEnd ℂ) (φ z)) (hlim : Filter.Tendsto φ (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) (nhds 0)) : Filter.Tendsto φ (Bornology.cobounded ℂ) (nhds 0)

For a function conjugation-symmetric near infinity and continuous at all sufficiently distant real points, decay along the upper half-plane implies decay along the whole plane.

theorem TauCeti.tendsto_zero_cobounded_of_tendsto_mul_upperHalfPlaneSet {φ ψ : ℂ → ℂ} {c : ℂ} (h : Filter.Tendsto (fun (z : ℂ) => z * ψ z) (Bornology.cobounded ℂ ⊓ Filter.principal UpperHalfPlane.upperHalfPlaneSet) (nhds c)) (hφcont : ∀ᶠ (z : ℂ) in Bornology.cobounded ℂ, z.im = 0 → ContinuousAt φ z) (hφconj : ∀ᶠ (z : ℂ) in Bornology.cobounded ℂ, φ ((starRingEnd ℂ) z) = (starRingEnd ℂ) (φ z)) (hφ : Set.EqOn φ ψ UpperHalfPlane.upperHalfPlaneSet) : Filter.Tendsto φ (Bornology.cobounded ℂ) (nhds 0)

A conjugation-symmetric continuation agreeing with ψ above the real axis tends to zero at infinity if z * ψ z has a finite limit there within the upper half-plane.

theorem TauCeti.mem_frontier_image_upperHalfPlaneSet_of_im_eq_zero {f : ℂ → ℂ} {z : ℂ} (hfc : ContinuousWithinAt f {z : ℂ | 0 ≤ z.im} z) (hz : z.im = 0) (hnot : f z ∉ f '' UpperHalfPlane.upperHalfPlaneSet) : f z ∈ frontier (f '' UpperHalfPlane.upperHalfPlaneSet)

A boundary point of the closed upper half-plane whose image avoids the open half-plane image maps to the frontier when the map is continuous there.

theorem TauCeti.not_mem_image_upperHalfPlaneSet_of_im_eq_zero {f : ℂ → ℂ} (hfi : Set.InjOn f {z : ℂ | 0 ≤ z.im}) {z : ℂ} (hz : z.im = 0) : f z ∉ f '' UpperHalfPlane.upperHalfPlaneSet

An injection on the closed upper half-plane cannot send a real point into the image of the open upper half-plane.

theorem TauCeti.im_neg_inv_nonneg {w : ℂ} : 0 ≤ (-w⁻¹).im ↔ 0 ≤ w.im

The inversion w ↦ -w⁻¹ sends w into the closed upper half-plane exactly when w lies in it.

theorem TauCeti.im_neg_inv_pos {w : ℂ} : 0 < (-w⁻¹).im ↔ 0 < w.im

The inversion w ↦ -w⁻¹ preserves the open upper half-plane.

theorem TauCeti.tendsto_comp_neg_inv_cobounded {α : Type u_1} {l : Filter α} {f : ℂ → α} (hp : Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 ≤ z.im}) l) : Filter.Tendsto (fun (w : ℂ) => f (-w⁻¹)) (nhdsWithin 0 ({w : ℂ | 0 ≤ w.im} \ {0})) l

w ↦ -w⁻¹ carries the closed upper half-plane near 0 to the closed upper half-plane near infinity, so a limit of f at infinity in the closed upper half-plane is a limit of w ↦ f (-w⁻¹) at 0 in the punctured closed upper half-plane.

theorem TauCeti.UpperHalfPlane.periodic_comp_ofComplex_iff {α : Type u_1} {f : UpperHalfPlane → α} {c : ℝ} : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑c ↔ ∀ (τ : UpperHalfPlane), f (c +ᵥ τ) = f τ

A function ℍ → α, extended to ℂ via ofComplex, is periodic with real period c iff the original function is invariant under translation by c.

theorem TauCeti.UpperHalfPlane.closure_preimage_re (s : Set ℝ) : closure (UpperHalfPlane.re ⁻¹' s) = UpperHalfPlane.re ⁻¹' closure s

UpperHalfPlane.re's closures and preimages commute, the ℍ analogue of Complex.closure_preimage_re.

@[simp]

theorem TauCeti.UpperHalfPlane.closure_setOfPred_lt_re (a : ℝ) : closure {z : UpperHalfPlane | a < z.re} = {z : UpperHalfPlane | a ≤ z.re}

The closure of an open right half-plane of ℍ, the analogue for ℍ of Complex.closure_setOfPred_lt_re for ℂ.

@[simp]

theorem TauCeti.UpperHalfPlane.closure_setOfPred_re_lt (a : ℝ) : closure {z : UpperHalfPlane | z.re < a} = {z : UpperHalfPlane | z.re ≤ a}

The closure of an open left half-plane of ℍ, the analogue for ℍ of Complex.closure_setOfPred_re_lt for ℂ.