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.

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

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.

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.

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.

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

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.

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.

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 𝕜.

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 eqOn_zero_of_preconnected_of_locally_zero which does not assume completeness of the target space.

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 eqOn_zero_of_preconnected_of_frequently_eq_zero.

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 eqOn_of_preconnected_of_frequently_eq.

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 eq_of_frequently_eq.