AnalyticOn.is_constant_or_isOpen
theorem AnalyticOn.is_constant_or_isOpen :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {U : Set E} {g : E → ℂ},
AnalyticOn ℂ g U → IsPreconnected U → (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen s → IsOpen (g '' s)
The Open Mapping Theorem for holomorphic functions in a global context, states that for a given function `g` that goes from a normed additive commutative group `E` to the complex numbers `ℂ`, if this function is analytic over a preconnected set `U`, then the function is either constant on `U`, or it is an open map on `U`. This means that it maps any open subset `s` of `U` to an open set in `ℂ`. A set `U` is preconnected if there is no non-trivial open partition of it, and a function is analytic on a set if it is analytic at every point in the set.
More concisely: If `g` is an analytic function from a preconnected set `U` in a normed additive commutative group `E` to the complex numbers `ℂ`, then `g` is either constant on `U` or it maps every open subset of `U` to an open set in `ℂ`.
|
AnalyticAt.eventually_constant_or_nhds_le_map_nhds
theorem AnalyticAt.eventually_constant_or_nhds_le_map_nhds :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {g : E → ℂ} {z₀ : E},
AnalyticAt ℂ g z₀ → (∀ᶠ (z : E) in nhds z₀, g z = g z₀) ∨ nhds (g z₀) ≤ Filter.map g (nhds z₀)
The open mapping theorem for holomorphic functions, in a local context, posits the following: if a function `g` from `E` to complex numbers is analytic at a particular point `z₀`, the function `g` is either a constant value within a neighborhood of `z₀`, or every neighborhood of `z₀` is mapped to a neighborhood of `g(z₀)`. In other words, for each point `z` eventually in the neighborhood of `z₀`, `g(z)` equals `g(z₀)` or the neighborhood of `g(z₀)` is less than or equal to the image under `g` of the neighborhood of `z₀`. For the specific case of a holomorphic function on the complex plane, refer to `AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux`.
More concisely: If a holomorphic function `g` is analytic at `z₀` in a complex domain `E`, then for every neighborhood `n` of `z₀`, either `g` is constant on `n` or the image `g(n)` contains a neighborhood of `g(z₀)`.
|
DiffContOnCl.ball_subset_image_closedBall
theorem DiffContOnCl.ball_subset_image_closedBall :
∀ {f : ℂ → ℂ} {z₀ : ℂ} {ε r : ℝ},
DiffContOnCl ℂ f (Metric.ball z₀ r) →
0 < r →
(∀ z ∈ Metric.sphere z₀ r, ε ≤ ‖f z - f z₀‖) →
(∃ᶠ (z : ℂ) in nhds z₀, f z ≠ f z₀) → Metric.ball (f z₀) (ε / 2) ⊆ f '' Metric.closedBall z₀ r
This theorem states that if we have a holomorphic function `f` from complex numbers to complex numbers, and a complex number `z₀`, as well as real numbers `ε` and `r`, such that `f` is differentiable and continuous on the open ball centered at `z₀` with radius `r`, and `r` is greater than zero. Furthermore, if the modulus of `f` is greater than or equal to `ε` on the sphere centered at `z₀` with radius `r`, and there exists a sequence of complex numbers converging to `z₀` such that their image under `f` are not equal to `f z₀`, then it is guaranteed that the open ball centered at `f z₀` with radius `ε / 2` is a subset of the image of the closed ball centered at `z₀` with radius `r` under `f`.
In simpler terms, if a complex function has a lower bound on its magnitude around a circle, then its values include all points in a disk of certain radius, given that there are points near the center of the circle that don't map to the same point.
More concisely: If a holomorphic function `f` has a minimum modulus `ε` on the sphere of radius `r` around `z₀`, and there exists a sequence in the open ball of radius `r` around `z₀` whose images under `f` are distinct from `f(z₀)`, then the open disk of radius `ε/2` around `f(z₀)` is contained in the image of the closed disk of radius `r` around `z₀`.
|
AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux
theorem AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux :
∀ {f : ℂ → ℂ} {z₀ : ℂ},
AnalyticAt ℂ f z₀ → (∀ᶠ (z : ℂ) in nhds z₀, f z = f z₀) ∨ nhds (f z₀) ≤ Filter.map f (nhds z₀)
This theorem states that if a function `f` from complex numbers to complex numbers is analytic at a point `z₀`, then either `f` is constant within a neighborhood of `z₀`, or `f` behaves like an open function in the vicinity of `z₀`. This "open function" behavior is characterized by the property that the image of any neighborhood of `z₀` under `f` is a neighborhood of `f(z₀)`. The same result also applies to a function `f` from any normed vector space `E` to the complex numbers.
More concisely: If a complex analytic function `f` at a point `z₀` is not constant, then it maps every neighborhood of `z₀` to a neighborhood of `f(z₀)` in the complex numbers or in any normed vector space `E`.
|