Complexification of real analytic functions on open sets

A real analytic function on an open set U ⊆ ι → ℝ, with ι finite, extends to a holomorphic function on an open neighborhood W ⊆ ι → ℂ of the real points of U. The neighborhood can be chosen invariant under complex conjugation and with real points exactly those of U, and the extension commutes with conjugation. Such an extension is unique near the real points: two holomorphic functions on an open neighborhood of the real points of U that agree at those points agree on a smaller conjugation-invariant open neighborhood of them.

The pointwise statement AnalyticAt.exists_complexification gives a holomorphic extension on a polydisc (a ball for the sup norm) centred at each real point of U. The extensions on two such polydiscs agree on their intersection: the intersection is convex, it contains the real part of each of its points, and near such a real point both extensions agree with the original function on the real points, hence agree by the identity theorem on the real points (AnalyticAt.eventuallyEq_of_eventually_real). The extensions therefore glue to a function on the union of the polydiscs. Shrinking each polydisc so that its real points lie in U makes the real points of the union exactly U, and polydiscs centred at real points are invariant under conjugation.

Main declarations

• AnalyticOnNhd.exists_complexification: a real analytic function on an open set extends to a holomorphic function on a conjugation-invariant open neighborhood of its real points.
• AnalyticOnNhd.exists_complexification_pi: the same for real analytic maps to κ → ℝ.
• AnalyticOnNhd.exists_eqOn_of_forall_real: uniqueness of such an extension on a conjugation-invariant open neighborhood of the real points.

References

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

theorem AnalyticOnNhd.exists_complexification {ι : Type u_1} [Fintype ι] {f : (ι → ℝ) → ℝ} {U : Set (ι → ℝ)} (hf : AnalyticOnNhd ℝ f U) (hU : IsOpen U) : ∃ (W : Set (ι → ℂ)), IsOpen W ∧ (∀ (x : ι → ℝ), (fun (i : ι) => ↑(x i)) ∈ W ↔ x ∈ U) ∧ (∀ (z : ι → ℂ), star z ∈ W ↔ z ∈ W) ∧ ∃ (F : (ι → ℂ) → ℂ), AnalyticOnNhd ℂ F W ∧ (∀ x ∈ U, (F fun (i : ι) => ↑(x i)) = ↑(f x)) ∧ ∀ (z : ι → ℂ), F (star z) = star (F z)

Complexification of a real analytic function on an open set. A function of finitely many real variables that is analytic on an open set U extends to a function F of as many complex variables that is complex analytic on an open set W whose real points are exactly those of U. The set W is invariant under complex conjugation, F agrees with f at the real points of U, and F commutes with complex conjugation.

theorem AnalyticOnNhd.exists_complexification_pi {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {f : (ι → ℝ) → κ → ℝ} {U : Set (ι → ℝ)} (hf : AnalyticOnNhd ℝ f U) (hU : IsOpen U) : ∃ (W : Set (ι → ℂ)), IsOpen W ∧ (∀ (x : ι → ℝ), (fun (i : ι) => ↑(x i)) ∈ W ↔ x ∈ U) ∧ (∀ (z : ι → ℂ), star z ∈ W ↔ z ∈ W) ∧ ∃ (F : (ι → ℂ) → κ → ℂ), AnalyticOnNhd ℂ F W ∧ (∀ x ∈ U, (F fun (i : ι) => ↑(x i)) = fun (k : κ) => ↑(f x k)) ∧ ∀ (z : ι → ℂ), F (star z) = star (F z)

Complexification of a real analytic map on an open set. A map from ι → ℝ to κ → ℝ, with ι and κ finite, that is analytic on an open set U extends to a map F : (ι → ℂ) → (κ → ℂ) that is complex analytic on an open set W whose real points are exactly those of U. The set W is invariant under complex conjugation, F agrees with f at the real points of U, and F commutes with complex conjugation.

theorem AnalyticOnNhd.exists_eqOn_of_forall_real {ι : Type u_1} [Fintype ι] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {F G : (ι → ℂ) → E} {U : Set (ι → ℝ)} {W : Set (ι → ℂ)} (hF : AnalyticOnNhd ℂ F W) (hG : AnalyticOnNhd ℂ G W) (hU : IsOpen U) (hW : IsOpen W) (hUW : ∀ x ∈ U, (fun (i : ι) => ↑(x i)) ∈ W) (hFG : ∀ x ∈ U, (F fun (i : ι) => ↑(x i)) = G fun (i : ι) => ↑(x i)) : ∃ V ⊆ W, IsOpen V ∧ (∀ (x : ι → ℝ), (fun (i : ι) => ↑(x i)) ∈ V ↔ x ∈ U) ∧ (∀ (z : ι → ℂ), star z ∈ V ↔ z ∈ V) ∧ Set.EqOn F G V

Uniqueness of complexifications. Two complex analytic functions of finitely many variables on an open neighborhood W of the real points of an open set U, agreeing at those real points, agree on a smaller open set V ⊆ W that is invariant under complex conjugation and whose real points are exactly those of U.