English
If a differentiable function on a normed space is bounded, it must be constant.
Русский
Если функция, дифференцируемая на нормированном пространстве, ограничена, то она должна быть постоянной.
LaTeX
$$$\\exists c\\in F, \\forall z\\in E, f(z)=c$$$
Lean4
/-- An auxiliary lemma for Liouville's theorem `Differentiable.apply_eq_apply_of_bounded`. -/
theorem liouville_theorem_aux {f : ℂ → F} (hf : Differentiable ℂ f) (hb : IsBounded (range f)) (z w : ℂ) : f z = f w :=
by
suffices ∀ c, deriv f c = 0 from is_const_of_deriv_eq_zero hf this z w
clear z w; intro c
obtain ⟨C, C₀, hC⟩ : ∃ C > (0 : ℝ), ∀ z, ‖f z‖ ≤ C :=
by
rcases isBounded_iff_forall_norm_le.1 hb with ⟨C, hC⟩
exact ⟨max C 1, lt_max_iff.2 (Or.inr zero_lt_one), fun z => (hC (f z) (mem_range_self _)).trans (le_max_left _ _)⟩
refine norm_le_zero_iff.1 (le_of_forall_gt_imp_ge_of_dense fun ε ε₀ => ?_)
calc
‖deriv f c‖ ≤ C / (C / ε) :=
norm_deriv_le_of_forall_mem_sphere_norm_le (div_pos C₀ ε₀) hf.diffContOnCl fun z _ => hC z
_ = ε := div_div_cancel₀ C₀.lt.ne'
