Complexification of real analytic functions

A real analytic function of finitely many real variables extends, near each point, to a holomorphic function of the same number of complex variables. This file constructs that extension from a power series.

Let p n be a continuous ℝ-multilinear map on ι → ℝ with values in ℝ, where ι is finite. Expanding each argument in the standard basis, p n v = ∑ r, (∏ k, v k (r k)) * p n (e_r), where r runs over the maps from the arguments to ι and e_r is the tuple of basis vectors it selects. The same formula with complex v defines a continuous ℂ-multilinear map on ι → ℂ, the complexification ContinuousMultilinearMap.complexifyPi. It agrees with p n on real arguments, it commutes with complex conjugation because its coefficients p n (e_r) are real, and its norm is at most (card ι) ^ n times that of p n. Applied to every term of a formal power series, this gives FormalMultilinearSeries.complexifyPi, whose radius of convergence is at least the original radius divided by card ι.

Summing the complexified series of a real analytic function f at a point a gives a function F that is complex analytic on a ball around a (a polydisc, since ι → ℂ carries the sup norm), agrees with f on the real points of that ball, and satisfies F (conj z) = conj (F z) for every z. The same holds coordinatewise for real analytic maps (ι → ℝ) → (κ → ℝ), such as the chart maps of a real analytic submanifold. This is the form in which statements about complex analytic functions, such as the local behaviour of roots of a polynomial with analytic coefficients, are applied to real analytic data.

The complexification is determined by the real function: a complex analytic function vanishing at the real points near a real point vanishes near it. The proof restricts the power series to the real points, where it represents zero, so each homogeneous term vanishes on real vectors; along the complex line through two real vectors such a term is an entire function vanishing on the real axis, hence zero. Consequently every complex analytic extension of a real-valued real analytic germ commutes with complex conjugation near the point, not only the one constructed here.

Main declarations

• ContinuousMultilinearMap.complexifyPi: the complexification of a real multilinear form on ι → ℝ, with complexifyPi_apply_ofReal, eq_complexifyPi_of_forall_ofReal, complexifyPi_apply_star and norm_complexifyPi_le; it is ℝ-linear (complexifyPi_zero, complexifyPi_add, complexifyPi_smul).
• FormalMultilinearSeries.complexifyPi: the termwise complexification of a power series, with FormalMultilinearSeries.le_radius_complexifyPi.
• AnalyticAt.exists_complexification: a real analytic function has, on a polydisc around the point, a complex analytic extension compatible with conjugation.
• AnalyticAt.exists_complexification_pi: the same for real analytic maps to κ → ℝ.
• AnalyticAt.eventually_eq_zero_of_eventually_real, AnalyticAt.eventuallyEq_of_eventually_real: the identity theorem for complex analytic functions on the real points.
• AnalyticAt.eventually_comp_eq_id_of_eventually_real: complex analytic extensions preserve a composition law equal to the identity near a real point.
• AnalyticAt.eventually_apply_star: a complex analytic function that is real at the real points near a real point commutes with conjugation near it.

References

• S. G. Krantz and H. R. Parks, A Primer of Real Analytic Functions, second edition, Birkhäuser, 2002.

noncomputable def ContinuousMultilinearMap.complexifyPi {ν : Type u_1} {ι : Type u_2} [Fintype ν] [Fintype ι] (f : ContinuousMultilinearMap ℝ (fun (x : ν) => ι → ℝ) ℝ) : ContinuousMultilinearMap ℂ (fun (x : ν) => ι → ℂ) ℂ

The complexification of a continuous real multilinear form f on ι → ℝ, for finite ι: the complex multilinear form on ι → ℂ given by v ↦ ∑ r, f (e_r) * ∏ k, v k (r k), where r runs over the maps ν → ι and e_r is the tuple of standard basis vectors Pi.single (r k) 1. It agrees with f on real arguments (complexifyPi_apply_ofReal).

Equations

• f.complexifyPi = ∑ r : ν → ι, ↑(f fun (k : ν) => Pi.single (r k) 1) • (ContinuousMultilinearMap.mkPiAlgebra ℂ ν ℂ).compContinuousLinearMap fun (k : ν) => ContinuousLinearMap.proj (r k)

theorem ContinuousMultilinearMap.complexifyPi_apply {ν : Type u_1} {ι : Type u_2} [Fintype ν] [Fintype ι] (f : ContinuousMultilinearMap ℝ (fun (x : ν) => ι → ℝ) ℝ) [DecidableEq ν] [DecidableEq ι] (v : ν → ι → ℂ) : f.complexifyPi v = ∑ r : ν → ι, ↑(f fun (k : ν) => Pi.single (r k) 1) * ∏ k : ν, v k (r k)

The complexification of f evaluates to ∑ r, f (e_r) * ∏ k, v k (r k).

@[simp]

theorem ContinuousMultilinearMap.complexifyPi_apply_ofReal {ν : Type u_1} {ι : Type u_2} [Fintype ν] [Fintype ι] (f : ContinuousMultilinearMap ℝ (fun (x : ν) => ι → ℝ) ℝ) (v : ν → ι → ℝ) : (f.complexifyPi fun (k : ν) (i : ι) => ↑(v k i)) = ↑(f v)

The complexification of a real multilinear form agrees with it on real arguments.

theorem ContinuousMultilinearMap.eq_complexifyPi_of_forall_ofReal {ν : Type u_1} {ι : Type u_2} [Fintype ν] [Fintype ι] (f : ContinuousMultilinearMap ℝ (fun (x : ν) => ι → ℝ) ℝ) {g : ContinuousMultilinearMap ℂ (fun (x : ν) => ι → ℂ) ℂ} (hg : ∀ (v : ν → ι → ℝ), (g fun (k : ν) (i : ι) => ↑(v k i)) = ↑(f v)) : g = f.complexifyPi

The complexification of a real multilinear form is the only complex multilinear form on ι → ℂ that agrees with it on real arguments.

@[simp]

theorem ContinuousMultilinearMap.complexifyPi_apply_star {ν : Type u_1} {ι : Type u_2} [Fintype ν] [Fintype ι] (f : ContinuousMultilinearMap ℝ (fun (x : ν) => ι → ℝ) ℝ) (v : ν → ι → ℂ) : f.complexifyPi (star v) = star (f.complexifyPi v)

The complexification of a real multilinear form commutes with complex conjugation.

@[simp]

theorem ContinuousMultilinearMap.complexifyPi_zero {ν : Type u_1} {ι : Type u_2} [Fintype ν] [Fintype ι] : complexifyPi 0 = 0

The complexification of the zero form is zero.

@[simp]

theorem ContinuousMultilinearMap.complexifyPi_add {ν : Type u_1} {ι : Type u_2} [Fintype ν] [Fintype ι] (f g : ContinuousMultilinearMap ℝ (fun (x : ν) => ι → ℝ) ℝ) : (f + g).complexifyPi = f.complexifyPi + g.complexifyPi

Complexification is additive.

@[simp]

theorem ContinuousMultilinearMap.complexifyPi_smul {ν : Type u_1} {ι : Type u_2} [Fintype ν] [Fintype ι] (f : ContinuousMultilinearMap ℝ (fun (x : ν) => ι → ℝ) ℝ) (c : ℝ) : (c • f).complexifyPi = ↑c • f.complexifyPi

Complexification commutes with real scalar multiplication.

theorem ContinuousMultilinearMap.norm_complexifyPi_le {ν : Type u_1} {ι : Type u_2} [Fintype ν] [Fintype ι] (f : ContinuousMultilinearMap ℝ (fun (x : ν) => ι → ℝ) ℝ) : ‖f.complexifyPi‖ ≤ ↑(Fintype.card ι) ^ Fintype.card ν * ‖f‖

Complexification multiplies the norm of a real multilinear form on ι → ℝ by at most (card ι) ^ (card ν).

theorem ContinuousMultilinearMap.apply_const_eq_zero_of_forall_ofReal {ν : Type u_1} {ι : Type u_2} {E : Type u_3} [Finite ν] [Finite ι] [NormedAddCommGroup E] [NormedSpace ℂ E] {Q : ContinuousMultilinearMap ℂ (fun (x : ν) => ι → ℂ) E} (h : ∀ (y : ι → ℝ), (Q fun (x : ν) (i : ι) => ↑(y i)) = 0) (z : ι → ℂ) : (Q fun (x : ν) => z) = 0

A complex multilinear map on ι → ℂ whose values on constant tuples of real vectors vanish also vanishes on constant tuples of complex vectors.

noncomputable def FormalMultilinearSeries.complexifyPi {ι : Type u_1} [Fintype ι] (p : FormalMultilinearSeries ℝ (ι → ℝ) ℝ) : FormalMultilinearSeries ℂ (ι → ℂ) ℂ

The termwise complexification of a real formal power series on ι → ℝ with values in ℝ.

Equations

• p.complexifyPi n = (p n).complexifyPi

@[simp]

theorem FormalMultilinearSeries.complexifyPi_apply {ι : Type u_1} [Fintype ι] (p : FormalMultilinearSeries ℝ (ι → ℝ) ℝ) (n : ℕ) : p.complexifyPi n = (p n).complexifyPi

The terms of the complexified series are the complexified terms.

@[simp]

theorem FormalMultilinearSeries.complexifyPi_zero {ι : Type u_1} [Fintype ι] : complexifyPi 0 = 0

The complexification of the zero series is zero.

@[simp]

theorem FormalMultilinearSeries.complexifyPi_add {ι : Type u_1} [Fintype ι] (p q : FormalMultilinearSeries ℝ (ι → ℝ) ℝ) : (p + q).complexifyPi = p.complexifyPi + q.complexifyPi

Termwise complexification is additive.

@[simp]

theorem FormalMultilinearSeries.complexifyPi_smul {ι : Type u_1} [Fintype ι] (p : FormalMultilinearSeries ℝ (ι → ℝ) ℝ) (c : ℝ) : (c • p).complexifyPi = ↑c • p.complexifyPi

Termwise complexification commutes with real scalar multiplication.

theorem FormalMultilinearSeries.le_radius_complexifyPi {ι : Type u_1} [Fintype ι] (p : FormalMultilinearSeries ℝ (ι → ℝ) ℝ) {r : NNReal} (hr : ↑(↑(Fintype.card ι) * r) < p.radius) : ↑r ≤ p.complexifyPi.radius

Complexification divides the radius of convergence by at most card ι.

@[simp]

theorem FormalMultilinearSeries.complexifyPi_sum_ofReal {ι : Type u_1} [Fintype ι] (p : FormalMultilinearSeries ℝ (ι → ℝ) ℝ) (y : ι → ℝ) : (p.complexifyPi.sum fun (i : ι) => ↑(y i)) = ↑(p.sum y)

On real arguments, the sum of the complexified series is the sum of the real series.

@[simp]

theorem FormalMultilinearSeries.complexifyPi_sum_star {ι : Type u_1} [Fintype ι] (p : FormalMultilinearSeries ℝ (ι → ℝ) ℝ) (z : ι → ℂ) : p.complexifyPi.sum (star z) = star (p.complexifyPi.sum z)

The sum of the complexified series commutes with complex conjugation.

theorem AnalyticAt.eventually_eq_zero_of_eventually_real {ι : Type u_1} [Fintype ι] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : (ι → ℂ) → E} {a : ι → ℝ} (hF : AnalyticAt ℂ F fun (i : ι) => ↑(a i)) (h : ∀ᶠ (x : ι → ℝ) in nhds a, (F fun (i : ι) => ↑(x i)) = 0) : ∀ᶠ (z : ι → ℂ) in nhds fun (i : ι) => ↑(a i), F z = 0

Identity theorem on the real points. A complex analytic function of finitely many variables that vanishes at the real points near a real point vanishes near that point.

theorem AnalyticAt.eventuallyEq_of_eventually_real {ι : Type u_1} [Fintype ι] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {F G : (ι → ℂ) → E} {a : ι → ℝ} (hF : AnalyticAt ℂ F fun (i : ι) => ↑(a i)) (hG : AnalyticAt ℂ G fun (i : ι) => ↑(a i)) (h : ∀ᶠ (x : ι → ℝ) in nhds a, (F fun (i : ι) => ↑(x i)) = G fun (i : ι) => ↑(x i)) : F =ᶠ[nhds fun (i : ι) => ↑(a i)] G

Two complex analytic functions of finitely many variables that agree at the real points near a real point agree near that point.

theorem AnalyticAt.eventually_comp_eq_id_of_eventually_real {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {f : (ι → ℝ) → κ → ℝ} {g : (κ → ℝ) → ι → ℝ} {a : ι → ℝ} {F : (ι → ℂ) → κ → ℂ} {G : (κ → ℂ) → ι → ℂ} (hF : AnalyticAt ℂ F fun (i : ι) => ↑(a i)) (hG : AnalyticAt ℂ G fun (i : κ) => ↑(f a i)) (hFr : ∀ᶠ (x : ι → ℝ) in nhds a, (F fun (i : ι) => ↑(x i)) = fun (i : κ) => ↑(f x i)) (hGr : ∀ᶠ (y : κ → ℝ) in nhds (f a), (G fun (i : κ) => ↑(y i)) = fun (i : ι) => ↑(g y i)) (hgf : ∀ᶠ (x : ι → ℝ) in nhds a, g (f x) = x) : ∀ᶠ (z : ι → ℂ) in nhds fun (i : ι) => ↑(a i), G (F z) = z

If real maps have composition g ∘ f equal to the identity near a real point, their complex analytic extensions compose to the identity near the corresponding complex point.

theorem AnalyticAt.exists_complexification {ι : Type u_1} [Fintype ι] {f : (ι → ℝ) → ℝ} {a : ι → ℝ} (hf : AnalyticAt ℝ f a) : ∃ r > 0, ∃ (F : (ι → ℂ) → ℂ), AnalyticOnNhd ℂ F (Metric.ball (fun (i : ι) => ↑(a i)) r) ∧ (∀ x ∈ Metric.ball a r, (F fun (i : ι) => ↑(x i)) = ↑(f x)) ∧ ∀ (z : ι → ℂ), F (star z) = star (F z)

Complexification of a real analytic function. A function of finitely many real variables that is analytic at a extends to a function F of as many complex variables that is complex analytic on a ball (a polydisc) around a, agrees with f at the real points of that ball, and commutes with complex conjugation.

theorem AnalyticAt.exists_complexification_pi {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {f : (ι → ℝ) → κ → ℝ} {a : ι → ℝ} (hf : AnalyticAt ℝ f a) : ∃ r > 0, ∃ (F : (ι → ℂ) → κ → ℂ), AnalyticOnNhd ℂ F (Metric.ball (fun (i : ι) => ↑(a i)) r) ∧ (∀ x ∈ Metric.ball a r, (F fun (i : ι) => ↑(x i)) = fun (k : κ) => ↑(f x k)) ∧ ∀ (z : ι → ℂ), F (star z) = star (F z)

Complexification of a real analytic map. A map from ι → ℝ to κ → ℝ, with ι and κ finite, that is analytic at a extends to a map F : (ι → ℂ) → (κ → ℂ) that is complex analytic on a ball (a polydisc) around a, agrees with f at the real points of that ball, and commutes with complex conjugation.

theorem AnalyticAt.eventually_apply_star {ι : Type u_1} [Fintype ι] {F : (ι → ℂ) → ℂ} {a : ι → ℝ} (hF : AnalyticAt ℂ F fun (i : ι) => ↑(a i)) (hreal : ∀ᶠ (x : ι → ℝ) in nhds a, (F fun (i : ι) => ↑(x i)).im = 0) : ∀ᶠ (z : ι → ℂ) in nhds fun (i : ι) => ↑(a i), F (star z) = star (F z)

Conjugation compatibility of complexifications. A complex analytic function of finitely many variables that takes real values at the real points near a real point a commutes with complex conjugation near a.