LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Analytic.IsolatedZeros

`AnalyticAt.eventually_eq_zero_or_eventually_ne_zero` theorem AnalyticAt.eventually_eq_zero_or_eventually_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜}, AnalyticAt 𝕜 f z₀ → (∀ᶠ (z : 𝕜) in nhds z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ 0 This theorem is a local version of the "Principle of Isolated Zeros" for an analytic function. It states that for a given function `f` that is analytic at a point `z₀`, one of the following two conditions will hold: either the function is identically zero in a neighborhood of `z₀`, or the function does not vanish in a punctured neighborhood of `z₀`. Here, a neighborhood of `z₀` encompasses points `z` that are arbitrarily close to `z₀`, and a punctured neighborhood of `z₀` is a neighborhood of `z₀` excluding `z₀` itself. More concisely: If a function `f` is analytic at a point `z₀`, then either `f` is identically zero or doesn't vanish in a punctured neighborhood of `z₀`.
`AnalyticOn.eqOn_of_preconnected_of_frequently_eq` theorem AnalyticOn.eqOn_of_preconnected_of_frequently_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} {U : Set 𝕜}, AnalyticOn 𝕜 f U → AnalyticOn 𝕜 g U → IsPreconnected U → z₀ ∈ U → (∃ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = g z) → Set.EqOn f g U This theorem, referred to as the identity principle for analytic functions in a global version, states that: if two functions `f` and `g` are analytic on a connected set `U` and they coincide at points which accumulate to a point `z₀` in the set `U`, then these two functions are equal throughout the set `U`. This is valid in the field `𝕜` with a nontrivial norm, and where `f` and `g` are functions from `𝕜` to a normed additive commutative group `E` with a normed space over `𝕜`. For higher-dimensional versions of the theorem, where the functions are required to coincide in a neighborhood of `z₀`, see `AnalyticOn.eqOn_of_preconnected_of_eventuallyEq`. More concisely: If two analytic functions defined on a connected set with a nontrivial normed field agree at all accumulation points, then they are equal throughout the set.
`AnalyticOn.eq_of_frequently_eq` theorem AnalyticOn.eq_of_frequently_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} [inst_3 : ConnectedSpace 𝕜], AnalyticOn 𝕜 f Set.univ → AnalyticOn 𝕜 g Set.univ → (∃ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = g z) → f = g This theorem, which is a global version of the identity principle for analytic functions, states that if two functions on a nontrivially normed field `𝕜` are analytic everywhere, and they coincide at points which frequently occur in the neighborhood of a point `z₀` excluding `z₀` itself, then these two functions are globally identical. In other words, if two functions behave the same way in a certain frequently occurring subset around a point, they behave the same way everywhere. This theorem does not apply to higher-dimensional scenarios where the functions need to coincide in a neighborhood of `z₀`; for these cases, the theorem `AnalyticOn.eq_of_eventuallyEq` should be consulted. More concisely: If two analytic functions on a nontrivially normed field agree everywhere densely around a point except at the point itself, then they are globally equal.
`AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero` theorem AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} {U : Set 𝕜}, AnalyticOn 𝕜 f U → IsPreconnected U → z₀ ∈ U → (∃ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = 0) → Set.EqOn f 0 U This theorem is known as the principle of isolated zeros for an analytic function, in its global version. It states that if a function is analytic on a connected set `U` and it vanishes frequently (meaning, it equals zero) within the set of all elements excluding a point `z₀` in the neighborhood of `z₀` in `U`, then the function is identically zero in `U`. This theorem applies to any function `f` mapping from a nontrivially normed field `𝕜` to a normed space `E` (with 𝕜 and E being any types), under the conditions that `f` is analytic on `U`, `U` is preconnected, and `z₀` belongs to `U`. Variations of this theorem for higher dimensions require that the function vanishes in a neighborhood of `z₀`. More concisely: If an analytic function on a connected and preconnected set in a nontrivially normed field equals zero in a neighborhood of a point in the set, then the function is identically zero on the set.
`AnalyticAt.unique_eventuallyEq_pow_smul_nonzero` theorem AnalyticAt.unique_eventuallyEq_pow_smul_nonzero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} {m n : ℕ}, (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in nhds z₀, f z = (z - z₀) ^ m • g z) → (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in nhds z₀, f z = (z - z₀) ^ n • g z) → m = n The theorem `AnalyticAt.unique_eventuallyEq_pow_smul_nonzero` states that for a given function `f` defined on a non-trivially normed field `𝕜` and a point `z₀` in `𝕜`, there can exist at most one natural number `n` such that in a neighborhood of `z₀`, the function `f` can be represented as `(z - z₀) ^ n • g z`, where `g` is another function that is analytic and non-vanishing at `z₀`. In other words, if there are two such representations with natural numbers `m` and `n`, then `m` must equal `n`. This signifies the uniqueness of the power in the power series representation of a function around a point in its domain, given that the function accompanying the power in the series is analytic and doesn't vanish at the given point. More concisely: Given a non-trivially normed field and a point in it, there can be at most one natural number such that in a neighborhood of that point, the function can be represented as the product of a power of the difference between the point and a constant, and an analytic and non-vanishing function.
`Mathlib.Analysis.Analytic.IsolatedZeros._auxLemma.3` theorem Mathlib.Analysis.Analytic.IsolatedZeros._auxLemma.3 : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, (a - b = 0) = (a = b) This theorem, `Mathlib.Analysis.Analytic.IsolatedZeros._auxLemma.3`, states that for any type `G` that has an addition group structure, the difference of any two elements `a` and `b` of this type is zero if and only if `a` equals `b`. In mathematical terms, it says that for all `a`, `b` in a group `G`, `a - b = 0` is equivalent to `a = b`. More concisely: For any group `G`, the element `a - b` is equal to zero if and only if `a` is equal to `b`.
`AnalyticAt.exists_eventuallyEq_pow_smul_nonzero_iff` theorem AnalyticAt.exists_eventuallyEq_pow_smul_nonzero_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜}, AnalyticAt 𝕜 f z₀ → ((∃ n g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in nhds z₀, f z = (z - z₀) ^ n • g z) ↔ ¬∀ᶠ (z : 𝕜) in nhds z₀, f z = 0) This theorem states that given a function `f` that is analytic at a point `z₀`, one of two possibilities must occur. Either `f` vanishes identically near `z₀`, meaning that for every point `z` in a neighborhood of `z₀`, `f(z) = 0`, or there exists an integer `n` and a function `g`, which is both analytic and non-vanishing at `z₀`, such that in a neighborhood of `z₀`, `f(z)` can be expressed as `(z - z₀)^n * g(z)`. In other words, locally around `z₀`, `f` behaves like the `n`th power of `(z - z₀)` multiplied by `g`. These two possibilities are mutually exclusive. More concisely: Given an analytic function `f` at a point `z₀`, either it is identically zero in a neighborhood of `z₀`, or there exists an integer `n` and a non-vanishing analytic function `g` such that `f(z) = (z - z₀)^n * g(z)` in a neighborhood of `z₀`.