English
A ball subset image lemma: if certain lower bounds hold for the modulus of a holomorphic function on a circle, then a ball around f(z0) is contained in the image of a closed ball under f.
Русский
Лемма о преобразовании шара в образ: если модуль функции достигает нижней границы на окружности, то шар вокруг f(z0) содержится в образе выпуклого шара под действием f.
LaTeX
$$$\\mathbb{B}(f(z_0), \\varepsilon/2) \\subset f(\\overline{\\mathbb{B}}(z_0, r))$ при заданных условиях$$
Lean4
/-- If the modulus of a holomorphic function `f` is bounded below by `ε` on a circle, then its range
contains a disk of radius `ε / 2`. -/
theorem ball_subset_image_closedBall (h : DiffContOnCl ℂ f (ball z₀ r)) (hr : 0 < r)
(hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖) (hz₀ : ∃ᶠ z in 𝓝 z₀, f z ≠ f z₀) :
ball (f z₀) (ε / 2) ⊆ f '' closedBall z₀ r := by
/- This is a direct application of the maximum principle. Pick `v` close to `f z₀`, and look at
the function `fun z ↦ ‖f z - v‖`: it is bounded below on the circle, and takes a small value
at `z₀` so it is not constant on the disk, which implies that its infimum is equal to `0` and
hence that `v` is in the range of `f`. -/
rintro v hv
have h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r) := h.sub_const v
have h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r) :=
continuous_norm.comp_continuousOn (closure_ball z₀ hr.ne.symm ▸ h1.continuousOn)
have h3 : AnalyticOnNhd ℂ f (ball z₀ r) := h.differentiableOn.analyticOnNhd isOpen_ball
have h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖ := fun z hz => by
linarith [hf z hz, show ‖v - f z₀‖ < ε / 2 from mem_ball.mp hv, norm_sub_sub_norm_sub_le_norm_sub (f z) v (f z₀)]
have h5 : ‖f z₀ - v‖ < ε / 2 := by simpa [← dist_eq_norm, dist_comm] using mem_ball.mp hv
obtain ⟨z, hz1, hz2⟩ : ∃ z ∈ ball z₀ r, IsLocalMin (fun z => ‖f z - v‖) z :=
exists_isLocalMin_mem_ball h2 (mem_closedBall_self hr.le) fun z hz => h5.trans_le (h4 z hz)
refine ⟨z, ball_subset_closedBall hz1, sub_eq_zero.mp ?_⟩
have h6 := h1.differentiableOn.eventually_differentiableAt (isOpen_ball.mem_nhds hz1)
refine (eventually_eq_or_eq_zero_of_isLocalMin_norm h6 hz2).resolve_left fun key => ?_
have h7 : ∀ᶠ w in 𝓝 z, f w = f z := by filter_upwards [key] with h; simp
replace h7 : ∃ᶠ w in 𝓝[≠] z, f w = f z := (h7.filter_mono nhdsWithin_le_nhds).frequently
have h8 : IsPreconnected (ball z₀ r) := (convex_ball z₀ r).isPreconnected
have h9 := h3.eqOn_of_preconnected_of_frequently_eq analyticOnNhd_const h8 hz1 h7
have h10 : f z = f z₀ := (h9 (mem_ball_self hr)).symm
exact not_eventually.mpr hz₀ (mem_of_superset (ball_mem_nhds z₀ hr) (h10 ▸ h9))
