AnalyticOn.eq_of_eventuallyEq
theorem AnalyticOn.eq_of_eventuallyEq :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace š F] {f g : E ā F}
[inst_5 : PreconnectedSpace E],
AnalyticOn š f Set.univ ā AnalyticOn š g Set.univ ā ā {zā : E}, (nhds zā).EventuallyEq f g ā f = g
The theorem, known as the *identity principle* for analytic functions, states that in a normed space, if two analytic functions coincide in a neighborhood of a point `zā`, then they are equal everywhere. This theorem applies to functions that are analytic on the universal set, i.e., every point in the space. The principle is validated by the premise that the space is preconnected. Furthermore, this theorem specifies that the equality of the two analytic functions in a neighborhood of `zā` is an eventuality, meaning that it holds at all points beyond a certain distance from `zā`. For a version of this theorem in one dimension where the functions only need to coincide at points arbitrarily close to `zā`, one should refer to `eq_of_frequently_eq`.
More concisely: In a preconnected normed space, if two analytic functions are equal in a neighborhood of a point, then they are equal everywhere.
|
AnalyticOn.eqOn_zero_of_preconnected_of_eventuallyEq_zero
theorem AnalyticOn.eqOn_zero_of_preconnected_of_eventuallyEq_zero :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace š F] {f : E ā F}
{U : Set E},
AnalyticOn š f U ā IsPreconnected U ā ā {zā : E}, zā ā U ā (nhds zā).EventuallyEq f 0 ā Set.EqOn f 0 U
The theorem, known as the *identity principle* for analytic functions, states that if a function `f`, which is analytic on a set `U`, becomes zero in a neighborhood of a point `zā` within `U`, then the function `f` is uniformly zero across the entire preconnected set `U`. This theorem is a one-dimensional version, which assumes that the function `f` is zero at points arbitrarily close to `zā`.
More concisely: If a function `f` analytic on a set `U` is zero in a neighborhood of a point `zā` in `U`, then `f` is uniformly zero on all of `U`.
|
AnalyticOn.eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux
theorem AnalyticOn.eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace š F]
[inst_5 : CompleteSpace F] {f : E ā F} {U : Set E},
AnalyticOn š f U ā IsPreconnected U ā ā {zā : E}, zā ā U ā (nhds zā).EventuallyEq f 0 ā Set.EqOn f 0 U
This theorem states that for any nontrivially normed field `š`, normed additive commutative groups `E` and `F` and normed space over `š` for `E` and `F`, where `F` is a complete space. If a function `f : E ā F` is analytic on a set `U`, and `U` is preconnected, then if `f` vanishes around a point `zā` in `U` (i.e., `f` equals to `0` on the neighborhood of `zā`), then `f` is uniformly zero on the entire set `U`. In other words, `f` equals `0` for all points in `U`. This theorem has been superseded by `eqOn_zero_of_preconnected_of_locally_zero` which does not require the completeness of the target space `F`.
More concisely: If `f : E -> F` is an analytic function on the preconnected set `U` in the nontrivially normed field `š`, and `f` equals `0` on the neighborhood of a point `zā` in `U`, then `f` is identically `0` on `U` for normed additive commutative groups `E` and `F`, where `F` is complete.
|
AnalyticOn.eqOn_of_preconnected_of_eventuallyEq
theorem AnalyticOn.eqOn_of_preconnected_of_eventuallyEq :
ā {š : Type u_1} [inst : NontriviallyNormedField š] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace š E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace š F] {f g : E ā F}
{U : Set E},
AnalyticOn š f U ā
AnalyticOn š g U ā IsPreconnected U ā ā {zā : E}, zā ā U ā (nhds zā).EventuallyEq f g ā Set.EqOn f g U
The *identity principle* for analytic functions states that if two analytic functions coincide on a neighborhood of a point `zā`, then they must coincide on any set that is connected to this neighborhood. More specifically, given two functions `f` and `g` from a non-trivially normed field `š` to normed add-commutative groups `E` and `F` respectively, and a set `U` that is preconnected, if `f` and `g` are both analytic on `U`, `zā` is an element of `U`, and `f` and `g` are equal in the neighborhood of `zā`, then `f` and `g` are equal on the whole set `U`.
More concisely: If analytic functions `f` and `g` are equal in a preconnected neighborhood, then they are equal on the entire set where they are defined.
|