English
If f is analytic at z0, then either f is constant in a neighborhood of z0, or the neighborhood is mapped to a neighborhood of f(z0).
Русский
Пусть f аналитична в точке z0; тогда либо она константна в окрестности z0, либо окрестность образуется в окрестность f(z0).
LaTeX
$$$\\text{AnalyticAt } f(z_0) \\Rightarrow (\\forall z \\,\\text{near } z_0, f(z)=f(z_0) \\lor (nhds(f(z_0)) \\le map f (nhds(z_0))))$$$
Lean4
/-- A function `f : ℂ → ℂ` which is analytic at a point `z₀` is either constant in a neighborhood
of `z₀`, or behaves locally like an open function (in the sense that the image of every neighborhood
of `z₀` is a neighborhood of `f z₀`, as in `isOpenMap_iff_nhds_le`). For a function `f : E → ℂ`
the same result holds, see `AnalyticAt.eventually_constant_or_nhds_le_map_nhds`. -/
theorem eventually_constant_or_nhds_le_map_nhds_aux (hf : AnalyticAt ℂ f z₀) :
(∀ᶠ z in 𝓝 z₀, f z = f z₀) ∨ 𝓝 (f z₀) ≤ map f (𝓝 z₀) := by
/- The function `f` is analytic in a neighborhood of `z₀`; by the isolated zeros principle, if `f`
is not constant in a neighborhood of `z₀`, then it is nonzero, and therefore bounded below, on
every small enough circle around `z₀` and then `DiffContOnCl.ball_subset_image_closedBall`
provides an explicit ball centered at `f z₀` contained in the range of `f`. -/
refine or_iff_not_imp_left.mpr fun h => ?_
refine (nhds_basis_ball.le_basis_iff (nhds_basis_closedBall.map f)).mpr fun R hR => ?_
have h1 := (hf.eventually_eq_or_eventually_ne analyticAt_const).resolve_left h
have h2 : ∀ᶠ z in 𝓝 z₀, AnalyticAt ℂ f z := (isOpen_analyticAt ℂ f).eventually_mem hf
obtain ⟨ρ, hρ, h3, h4⟩ : ∃ ρ > 0, AnalyticOnNhd ℂ f (closedBall z₀ ρ) ∧ ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀ :=
by
simpa only [setOf_and, subset_inter_iff] using
nhds_basis_closedBall.mem_iff.mp (h2.and (eventually_nhdsWithin_iff.mp h1))
replace h3 : DiffContOnCl ℂ f (ball z₀ ρ) :=
⟨h3.differentiableOn.mono ball_subset_closedBall, (closure_ball z₀ hρ.lt.ne.symm).symm ▸ h3.continuousOn⟩
let r := ρ ⊓ R
have hr : 0 < r := lt_inf_iff.mpr ⟨hρ, hR⟩
have h5 : closedBall z₀ r ⊆ closedBall z₀ ρ := closedBall_subset_closedBall inf_le_left
have h6 : DiffContOnCl ℂ f (ball z₀ r) := h3.mono (ball_subset_ball inf_le_left)
have h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀ := fun z hz =>
h4 z (h5 (sphere_subset_closedBall hz)) (ne_of_mem_sphere hz hr.ne.symm)
have h8 : (sphere z₀ r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
have h9 : ContinuousOn (fun x => ‖f x - f z₀‖) (sphere z₀ r) :=
continuous_norm.comp_continuousOn ((h6.sub_const (f z₀)).continuousOn_ball.mono sphere_subset_closedBall)
obtain ⟨x, hx, hfx⟩ := (isCompact_sphere z₀ r).exists_isMinOn h8 h9
refine ⟨‖f x - f z₀‖ / 2, half_pos (norm_sub_pos_iff.mpr (h7 x hx)), ?_⟩
exact
(h6.ball_subset_image_closedBall hr (fun z hz => hfx hz) (not_eventually.mp h)).trans
(by gcongr; exact inf_le_right)
