Holomorphic functions and their values on the real line

Two entire functions with values in a complex normed space that agree at every real point are equal. This is the identity principle AnalyticOnNhd.eq_of_frequently_eq, applied at the accumulation point 0 of the real axis. It is the uniqueness statement behind analytic continuation of real one-parameter orbits to complex time. On the complex slit plane, agreement on the positive real axis likewise determines a holomorphic function uniquely.

At a real point, the order of vanishing of a holomorphic function equals the order of vanishing of its restriction to the real line (AnalyticAt.analyticOrderAt_comp_ofReal). This lets the order of a real analytic function be read off any holomorphic extension of it.

theorem Differentiable.eq_of_ofReal_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} (hf : Differentiable ℂ f) (hg : Differentiable ℂ g) (h : ∀ (t : ℝ), f ↑t = g ↑t) : f = g

Two entire functions agreeing on the real line are equal.

theorem AnalyticOnNhd.eqOn_slitPlane_of_ofReal_pos_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} (hf : AnalyticOnNhd ℂ f Complex.slitPlane) (hg : AnalyticOnNhd ℂ g Complex.slitPlane) (h : ∀ (t : ℝ), 0 < t → f ↑t = g ↑t) : Set.EqOn f g Complex.slitPlane

Two holomorphic functions on the slit plane agreeing on the positive real axis agree throughout the slit plane.

theorem AnalyticAt.analyticOrderAt_comp_ofReal {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} {t : ℝ} (hf : AnalyticAt ℂ f ↑t) : analyticOrderAt (fun (s : ℝ) => f ↑s) t = analyticOrderAt f ↑t

At a real point t, a holomorphic function f and its restriction s ↦ f s to the real line vanish to the same order.