Holomorphic self-maps of the upper half-plane

TheoremSchwarz lemma on the upper half-plane#●ready to prove

Let \(\mathbb{H}=\{z\in\mathbb{C} : \mathrm{Im}\,z>0\}\) be the upper half-plane, and let \(F\) be a complex function that is holomorphic on \(\mathbb{H}\), satisfies \(|F(z)|\le 1\) for every \(z\in\mathbb{H}\), and vanishes at \(i\). Then for every \(z\in\mathbb{H}\),

\[|F(z)|\le\left|\frac{z-i}{z+i}\right|.\]

public theorem_wanted norm_le_norm_cayley_of_upperHalfPlane_bounded_vanishing_at_I (F : ℂ → ℂ)
    (hHolo : DifferentiableOn ℂ F {z : ℂ | 0 < z.im})
    (hBound : ∀ z, 0 < z.im → norm (F z) ≤ 1)
    (hFi : F Complex.I = 0) :
    ∀ z : ℂ, 0 < z.im →
      norm (F z) ≤ norm ((z - Complex.I) / (z + Complex.I))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functions of a complex variable; Geometric function theory), problem ma_proofbench_l1_20.

TheoremDerivative bound at \(i\) for a self-map of the upper half-plane#●ready to prove

Let \(\mathbb{H}=\{z\in\mathbb{C} : \mathrm{Im}\,z>0\}\) be the upper half-plane, and let \(f\) be a complex function that is holomorphic on \(\mathbb{H}\), maps \(\mathbb{H}\) into \(\mathbb{H}\), and satisfies \(f(i)=e^{2\pi i/3}\). Then \(|f'(i)|\le\sqrt{3/2}\).

public theorem_wanted norm_deriv_I_le_sqrt_three_halves_of_mapsTo_upperHalfPlane
    (f : ℂ → ℂ)
    (hf_holo : DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet)
    (hf_maps : Set.MapsTo f UpperHalfPlane.upperHalfPlaneSet UpperHalfPlane.upperHalfPlaneSet)
    (hpoint : f Complex.I = Complex.exp ((2 * Real.pi * Complex.I) / 3)) :
    ‖deriv f Complex.I‖ ≤ Real.sqrt (3 / 2 : ℝ)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functions of a complex variable; Geometric function theory), problem ma_proofbench_l2_62.

TheoremIterates of a self-map of the upper half-plane fixing \(i\)#●ready to prove

Let \(\mathbb{H}=\{z\in\mathbb{C} : \mathrm{Im}\,z>0\}\) be the upper half-plane, and let \(f\) be a complex function that is holomorphic on \(\mathbb{H}\), maps \(\mathbb{H}\) into \(\mathbb{H}\), and satisfies \(f(i)=i\) and \(f(2i)=\frac{15}{8}i\). Then the iterates \(f^{\circ n}(2i)\) converge to \(i\) as \(n\to\infty\), where \(f^{\circ n}\) is the \(n\)-fold composite of \(f\) with itself.

public theorem_wanted tendsto_iterate_two_mul_I_of_fixed_I
    (f : ℂ → ℂ)
    (hf_maps : ∀ z : ℂ, 0 < z.im → 0 < (f z).im)
    (hf_holo : DifferentiableOn ℂ f {z : ℂ | 0 < z.im})
    (hfi : f Complex.I = Complex.I)
    (hf2i : f (2 * Complex.I) = ((15 / (8 : ℂ)) * Complex.I)) :
    Filter.Tendsto (fun n : ℕ => (f^[n]) (2 * Complex.I)) Filter.atTop (nhds Complex.I)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functions of a complex variable; Geometric function theory), problem ma_proofbench_l2_34.

TheoremSurjectivity for half-plane self-maps that are real on the real axis#●ready to prove

Let \(\mathbb{C}_{+} = \{z \in \mathbb{C} : \operatorname{Im} z > 0\}\) be the open upper half-plane and \(\overline{\mathbb{C}_{+}} = \{z \in \mathbb{C} : \operatorname{Im} z \ge 0\}\) the closed one. Let \(f : \mathbb{C} \to \mathbb{C}\) be continuous on \(\overline{\mathbb{C}_{+}}\) with \(f(\overline{\mathbb{C}_{+}}) \subseteq \overline{\mathbb{C}_{+}}\), suppose \(f(x)\) is real for every real \(x\), and suppose \(f\) is holomorphic on \(\mathbb{C}_{+}\) and not constant on \(\mathbb{C}_{+}\). Then \(f(\mathbb{C}_{+}) = \mathbb{C}_{+}\).

public theorem_wanted image_upperHalfPlane_eq_of_real_on_real
  (f : ℂ → ℂ)
  (hcont : ContinuousOn f {z : ℂ | 0 ≤ z.im})
  (hupper : ∀ z : ℂ, 0 ≤ z.im → 0 ≤ (f z).im)
  (hreal : ∀ x : ℝ, (f x).im = 0)
  (hhol : DifferentiableOn ℂ f {z : ℂ | 0 < z.im})
  (hnconst : ¬ ∃ c : ℂ, ∀ z : ℂ, 0 < z.im → f z = c) :
  f '' {z : ℂ | 0 < z.im} = {w : ℂ | 0 < w.im}

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functions of a complex variable; Geometric function theory), problem ma_proofbench_l2_71.

4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.