English
If a complex-valued function f is continuous on a ball and attains a maximum of the norm on the boundary, then the boundary value equals the center value in norm.
Русский
Если функция f непрерывна на шаре и достигает максимума нормы на границе, то нормa значения на границе равна норме в центре.
LaTeX
$$$$\\text{Let } f: \\mathbb{C} \\to F \\text{ be as above; if } f \\text{ attains its maximum of } \\|f\\| \\text{ on a ball, then } \\|f(w)\\| = \\|f(z)\\|.$$$$
Lean4
theorem norm_max_aux₁ [CompleteSpace F] {f : ℂ → F} {z w : ℂ} (hd : DiffContOnCl ℂ f (ball z (dist w z)))
(hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z) : ‖f w‖ = ‖f z‖ := by
-- Consider a circle of radius `r = dist w z`.
set r : ℝ := dist w z
have hw : w ∈ closedBall z r := mem_closedBall.2 le_rfl
refine (isMaxOn_iff.1 hz _ hw).antisymm (not_lt.1 ?_)
rintro hw_lt : ‖f w‖ < ‖f z‖
have hr : 0 < r :=
dist_pos.2
(ne_of_apply_ne (norm ∘ f) hw_lt.ne)
-- Due to Cauchy integral formula, it suffices to prove the following inequality.
suffices ‖∮ ζ in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * ‖f z‖
by
refine this.ne ?_
have A : (∮ ζ in C(z, r), (ζ - z)⁻¹ • f ζ) = (2 * π * I : ℂ) • f z :=
hd.circleIntegral_sub_inv_smul (mem_ball_self hr)
simp [A, norm_smul, Real.pi_pos.le]
suffices ‖∮ ζ in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * r * (‖f z‖ / r) by
rwa [mul_assoc, mul_div_cancel₀ _ hr.ne'] at this
have hsub : sphere z r ⊆ closedBall z r := sphere_subset_closedBall
refine circleIntegral.norm_integral_lt_of_norm_le_const_of_lt hr ?_ ?_ ⟨w, rfl, ?_⟩
· show ContinuousOn (fun ζ : ℂ => (ζ - z)⁻¹ • f ζ) (sphere z r)
refine ((continuousOn_id.sub continuousOn_const).inv₀ ?_).smul (hd.continuousOn_ball.mono hsub)
exact fun ζ hζ => sub_ne_zero.2 (ne_of_mem_sphere hζ hr.ne')
· show ∀ ζ ∈ sphere z r, ‖(ζ - z)⁻¹ • f ζ‖ ≤ ‖f z‖ / r
rintro ζ (hζ : ‖ζ - z‖ = r)
rw [le_div_iff₀ hr, norm_smul, norm_inv, hζ, mul_comm, mul_inv_cancel_left₀ hr.ne']
exact hz (hsub hζ)
show ‖(w - z)⁻¹ • f w‖ < ‖f z‖ / r
rw [norm_smul, norm_inv, ← div_eq_inv_mul]
exact (div_lt_div_iff_of_pos_right hr).2 hw_lt
