English
If f: M → F is complex differentiable near c and ||f|| attains a local maximum at c, then ||f|| is locally constant near c.
Русский
Если f: M → F комплексно дифференцируема около c и ||f|| достигает локального максимума в c, то ||f|| локально константна около c.
LaTeX
$$$\forall f: M \to F, \; \forall c: M,\; (\forall^\infty z \text{ in } 𝓝 c, MDifferentiableAt I 𝓘(\mathbb{C}, F) f z) \land IsLocalMax(\|f\|) c \Rightarrow \forall^\infty y \text{ in } 𝓝 c, \|f(y)\| = \|f(c)\|$$$
Lean4
/-- **Maximum modulus principle**: if `f : M → F` is complex differentiable in a neighborhood of `c`
and the norm `‖f z‖` has a local maximum at `c`, then `‖f z‖` is locally constant in a neighborhood
of `c`. This is a manifold version of `Complex.norm_eventually_eq_of_isLocalMax`. -/
theorem norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax {f : M → F} {c : M}
(hd : ∀ᶠ z in 𝓝 c, MDifferentiableAt I 𝓘(ℂ, F) f z) (hc : IsLocalMax (norm ∘ f) c) : ∀ᶠ y in 𝓝 c, ‖f y‖ = ‖f c‖ :=
by
set e := extChartAt I c
have hI : range I = univ := ModelWithCorners.Boundaryless.range_eq_univ
have H₁ : 𝓝[range I] (e c) = 𝓝 (e c) := by rw [hI, nhdsWithin_univ]
have H₂ : map e.symm (𝓝 (e c)) = 𝓝 c := by rw [← map_extChartAt_symm_nhdsWithin_range (I := I) c, H₁]
rw [← H₂, eventually_map]
replace hd : ∀ᶠ y in 𝓝 (e c), DifferentiableAt ℂ (f ∘ e.symm) y :=
by
have : e.target ∈ 𝓝 (e c) := H₁ ▸ extChartAt_target_mem_nhdsWithin c
filter_upwards [this, Tendsto.eventually H₂.le hd] with y hyt hy₂
have hys : e.symm y ∈ (chartAt H c).source :=
by
rw [← extChartAt_source I c]
exact (extChartAt I c).map_target hyt
have hfy : f (e.symm y) ∈ (chartAt F (0 : F)).source := mem_univ _
rw [mdifferentiableAt_iff_of_mem_source hys hfy, hI, differentiableWithinAt_univ, e.right_inv hyt] at hy₂
exact hy₂.2
convert norm_eventually_eq_of_isLocalMax hd _
· exact congr_arg f (extChartAt_to_inv _).symm
· simpa only [e, IsLocalMax, IsMaxFilter, ← H₂, (· ∘ ·), extChartAt_to_inv] using hc
