# Uniqueness principle for analytic functions #

We show that two analytic functions which coincide around a point coincide on whole connected sets, in `AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq`.

### Uniqueness of power series #

If a function `f : E → F` has two representations as power series at a point `x : E`, corresponding to formal multilinear series `p₁` and `p₂`, then these representations agree term-by-term. That is, for any `n : ℕ` and `y : E`, `p₁ n (fun i ↦ y) = p₂ n (fun i ↦ y)`. In the one-dimensional case, when `f : 𝕜 → E`, the continuous multilinear maps `p₁ n` and `p₂ n` are given by `ContinuousMultilinearMap.mkPiRing`, and hence are determined completely by the value of `p₁ n (fun i ↦ 1)`, so `p₁ = p₂`. Consequently, the radius of convergence for one series can be transferred to the other.

source
theorem Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {p : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) F} (h : (fun (y : E) => p fun (x : Fin n) => y) =O[nhds 0] fun (y : E) => ‖y‖ ^ (n + 1)) (y : E) :
(p fun (x : Fin n) => y) = 0
source
theorem HasFPowerSeriesAt.apply_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {x : E} (h : HasFPowerSeriesAt 0 p x) (n : ℕ) (y : E) :
((p n) fun (x : Fin n) => y) = 0

If a formal multilinear series `p` represents the zero function at `x : E`, then the terms `p n (fun i ↦ y)` appearing in the sum are zero for any `n : ℕ`, `y : E`.

source
theorem HasFPowerSeriesAt.eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {x : 𝕜} (h : HasFPowerSeriesAt 0 p x) :
p = 0

A one-dimensional formal multilinear series representing the zero function is zero.

source
theorem HasFPowerSeriesAt.eq_formalMultilinearSeries {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {x : 𝕜} (h₁ : HasFPowerSeriesAt f p₁ x) (h₂ : HasFPowerSeriesAt f p₂ x) :
p₁ = p₂

One-dimensional formal multilinear series representing the same function are equal.

source
theorem HasFPowerSeriesAt.eq_formalMultilinearSeries_of_eventually {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p q : FormalMultilinearSeries 𝕜 𝕜 E} {f g : 𝕜 → E} {x : 𝕜} (hp : HasFPowerSeriesAt f p x) (hq : HasFPowerSeriesAt g q x) (heq : ∀ᶠ (z : 𝕜) in nhds x, f z = g z) :
p = q
source
theorem HasFPowerSeriesAt.eq_zero_of_eventually {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {x : 𝕜} (hp : HasFPowerSeriesAt f p x) (hf : f =ᶠ[nhds x] 0) :
p = 0

A one-dimensional formal multilinear series representing a locally zero function is zero.

source
theorem HasFPowerSeriesOnBall.exchange_radius {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {r₁ r₂ : ENNReal} {x : 𝕜} (h₁ : HasFPowerSeriesOnBall f p₁ x r₁) (h₂ : HasFPowerSeriesOnBall f p₂ x r₂) :
HasFPowerSeriesOnBall f p₁ x r₂

If a function `f : 𝕜 → E` has two power series representations at `x`, then the given radii in which convergence is guaranteed may be interchanged. This can be useful when the formal multilinear series in one representation has a particularly nice form, but the other has a larger radius.

source
theorem HasFPowerSeriesOnBall.r_eq_top_of_exists {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {r : ENNReal} {x : 𝕜} {p : FormalMultilinearSeries 𝕜 𝕜 E} (h : HasFPowerSeriesOnBall f p x r) (h' : ∀ (r' : NNReal), 0 < r' → ∃ (p' : FormalMultilinearSeries 𝕜 𝕜 E), HasFPowerSeriesOnBall f p' x ↑r') :
HasFPowerSeriesOnBall f p x ⊤

If a function `f : 𝕜 → E` has power series representation `p` on a ball of some radius and for each positive radius it has some power series representation, then `p` converges to `f` on the whole `𝕜`.

source
theorem AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {U : Set E} (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[nhds z₀] 0) :
Set.EqOn f 0 U

If an analytic function vanishes around a point, then it is uniformly zero along a connected set. Superseded by `AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero` which does not assume completeness of the target space.

source
theorem AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {U : Set E} (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[nhds z₀] 0) :
Set.EqOn f 0 U

The identity principle for analytic functions: If an analytic function vanishes in a whole neighborhood of a point `z₀`, then it is uniformly zero along a connected set. For a one-dimensional version assuming only that the function vanishes at some points arbitrarily close to `z₀`, see `AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero`.

source
theorem AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {U : Set E} (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfg : f =ᶠ[nhds z₀] g) :
Set.EqOn f g U

The identity principle for analytic functions: If two analytic functions coincide in a whole neighborhood of a point `z₀`, then they coincide globally along a connected set. For a one-dimensional version assuming only that the functions coincide at some points arbitrarily close to `z₀`, see `AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq`.

source
theorem AnalyticOnNhd.eq_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} [PreconnectedSpace E] (hf : AnalyticOnNhd 𝕜 f Set.univ) (hg : AnalyticOnNhd 𝕜 g Set.univ) {z₀ : E} (hfg : f =ᶠ[nhds z₀] g) :
f = g

The identity principle for analytic functions: If two analytic functions on a normed space coincide in a neighborhood of a point `z₀`, then they coincide everywhere. For a one-dimensional version assuming only that the functions coincide at some points arbitrarily close to `z₀`, see `AnalyticOnNhd.eq_of_frequently_eq`.