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.

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.

Main declarations

• Real.nhdsWithin_upperHalfPlaneSet_neBot.
• TauCeti.UpperHalfPlane.periodic_comp_ofComplex_iff.

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.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.