Analytic functions are determined by their restrictions to lines

A function analytic at p vanishes on a neighbourhood of p exactly when its restriction t ↦ f (p + t • v) to every line through p vanishes on a neighbourhood of 0. The nontrivial direction is the identity principle along each line: on a ball around p where f is analytic, the restriction to the line through p and a point y of the ball is analytic on a disc containing 0 and 1, so it vanishes at 1, that is at y.

In several complex variables this is the first step of putting a nonzero germ in general position: some direction v has a restriction that does not vanish identically, and in linear coordinates whose last axis is v the germ becomes regular in the last variable, as Weierstrass preparation requires (AnalyticAt.exists_continuousLinearEquiv_analyticOrderAt_ne_top).

The name follows Mathlib's Mathlib.Analysis.Analytic.Uniqueness, where the identity principle lives.

Main declarations

• AnalyticAt.eventuallyEq_zero_iff_forall_eventuallyEq_zero_comp_add_smul: an analytic function vanishes near p exactly when all its restrictions to lines through p vanish near 0.
• AnalyticAt.exists_continuousLinearEquiv_analyticOrderAt_ne_top: after a linear change of coordinates, a function on E × 𝕜 not vanishing near p has finite order in the last variable.

References

• L. Hörmander, An Introduction to Complex Analysis in Several Variables, §6.1.
• R. C. Gunning, H. Rossi, Analytic Functions of Several Complex Variables, Ch. II, §B.

theorem AnalyticAt.eventuallyEq_zero_iff_forall_eventuallyEq_zero_comp_add_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : E} (hf : AnalyticAt 𝕜 f p) : f =ᶠ[nhds p] 0 ↔ ∀ (v : E), (fun (t : 𝕜) => f (p + t • v)) =ᶠ[nhds 0] 0

An analytic function is determined near a point by its restrictions to lines. A function analytic at p vanishes on a neighbourhood of p exactly when, for every direction v, the restriction t ↦ f (p + t • v) vanishes on a neighbourhood of 0.

theorem AnalyticAt.exists_continuousLinearEquiv_analyticOrderAt_ne_top {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E × 𝕜 → F} {p : E × 𝕜} (hf : AnalyticAt 𝕜 f p) (hf0 : ¬f =ᶠ[nhds p] 0) : ∃ (L : (E × 𝕜) ≃L[𝕜] E × 𝕜) (q : E × 𝕜), L q = p ∧ analyticOrderAt (fun (t : 𝕜) => f (L (q.1, t))) q.2 ≠ ⊤

General position in the last variable. A function analytic at p on E × 𝕜 that does not vanish near p becomes regular in the last variable after a linear change of coordinates: there are a continuous linear automorphism L and a point q with L q = p such that t ↦ f (L (q.1, t)) has finite analytic order at q.2. The last axis is sent to a direction along which the restriction of f does not vanish identically.