mathlib documentation

analysis.analytic.uniqueness

Uniqueness principle for analytic functions #

We show that two analytic functions which coincide around a point coincide on whole connected sets, in analytic_on.eq_on_of_preconnected_of_eventually_eq.

theorem analytic_on.eq_on_zero_of_preconnected_of_eventually_eq_zero_aux {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] [complete_space F] {f : E β†’ F} {U : set E} (hf : analytic_on π•œ f U) (hU : is_preconnected U) {zβ‚€ : E} (hβ‚€ : zβ‚€ ∈ U) (hfzβ‚€ : f =αΆ [nhds zβ‚€] 0) :
set.eq_on f 0 U

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

theorem analytic_on.eq_on_zero_of_preconnected_of_eventually_eq_zero {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] {f : E β†’ F} {U : set E} (hf : analytic_on π•œ f U) (hU : is_preconnected U) {zβ‚€ : E} (hβ‚€ : zβ‚€ ∈ U) (hfzβ‚€ : f =αΆ [nhds zβ‚€] 0) :
set.eq_on 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 eq_on_zero_of_preconnected_of_frequently_eq_zero.

theorem analytic_on.eq_on_of_preconnected_of_eventually_eq {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] {f g : E β†’ F} {U : set E} (hf : analytic_on π•œ f U) (hg : analytic_on π•œ g U) (hU : is_preconnected U) {zβ‚€ : E} (hβ‚€ : zβ‚€ ∈ U) (hfg : f =αΆ [nhds zβ‚€] g) :
set.eq_on 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 eq_on_of_preconnected_of_frequently_eq.

theorem analytic_on.eq_of_eventually_eq {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_3} [normed_add_comm_group F] [normed_space π•œ F] {f g : E β†’ F} [preconnected_space E] (hf : analytic_on π•œ f set.univ) (hg : analytic_on π•œ 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.