English
If a function is differentiable in a disc and satisfies the mean value property on the circle, then its values inside equal the center value.
Русский
Если функция дифференцируема на диске и удовлетворяет тождественному среднему по окружности, то её значение в центре равно среднему значению во внутренности.
LaTeX
$$$ circleAverage f c R = f(c) $$$
Lean4
/-- **Liouville's theorem**: a complex differentiable bounded function `f : E → F` is a constant. -/
theorem apply_eq_apply_of_bounded {f : E → F} (hf : Differentiable ℂ f) (hb : IsBounded (range f)) (z w : E) :
f z = f w := by
set g : ℂ → F := f ∘ fun t : ℂ => t • (w - z) + z
suffices g 0 = g 1 by simpa [g]
apply liouville_theorem_aux
exacts [hf.comp ((differentiable_id.smul_const (w - z)).add_const z), hb.subset (range_comp_subset_range _ _)]
