Extend a real analytic function to a complex analytic

Stream: Is there code for X?

[Yury G. Kudryashov]

If $f\colon \mathbb R^n\to \mathbb R^m$ is real analytic at the origin, then there exists a function $g\colon \mathbb C^n\to\mathbb C^m$ such that it is complex analytic at the origin and its restriction to real numbers is f.

• Do we have something like this?
• If no, then what is the right way to state this?

In practice, I need the versions for m=1 and n=1 or n=2.

[Heather Macbeth]

@Yury G. Kudryashov I think we should have both a version starting from a general real vector space and extending to its tensoring-with-$\mathbb{C}$, and a version extending to a general complex vector space starting from a "totally real subspace" of it:

import Mathlib.Analysis.Complex.Basic

variable {V : Type*} [AddCommGroup V] [Module ℝ V] [Module ℂ V]
  [IsScalarTower ℝ ℂ V]

structure TotallyReal (W : Submodule ℝ V) : Prop where
  invariant : ∀ v ∈ W, v ≠ 0 → Complex.I • v ∉ W
  spans : Submodule.span ℂ (W : Set V) = ⊤

(alternate definition: rephrase spans in terms of maximality).

[Heather Macbeth]

In fact, to go literally from $\mathbb{R}^n$ to $\mathbb{C}^n$, neither of these works exactly; maybe we need the trick of considering functions rather than sets, so consider a notion of a "totally real embedding" of a real vector space into a complex vector space, rather than just a totally real subspace.

[Kevin Buzzard]

We have both "the localisation" (the concrete construction) and "is a localisation" (the characteristic predicate) in commutative algebra and people have certainly talked about making an analogous "is a tensor product" predicate but I'm not sure if it ever happened.

[Yury G. Kudryashov]

Thank you! In my current project, I'll assume that the input functions are complex analytic and preserve real numbers right away.

[Yury G. Kudryashov]

(I want to have it done in a week or two)

[Eric Wieser]

We have docs#IsTensorProduct, but we might want a special case for IsBaseChange

[Antoine Chambert-Loir]

This is a strange statement because it is voluntarily meaningless outside of the origin. Isn't it better to start from an open subset of R^n an which f is analytic and ask for an open subset of C^n containing U and an analytic function g on V that extends V?

[Yury G. Kudryashov]

Of course, I formulated this for the origin to avoid technical details and the actual Mathlib lemma should deal with them (have a lemma for a germ at any point and a lemma about an open set).