English
If a function f: C → E is differentiable on a ball B(c, R1), maps B(c, R1) into B(f(c), R2), and there exists a point z0 in B(c, R1) with ‖dslope f c z0‖ = R2/R1, then f coincides on B(c, R1) with an affine map based at c with slope C = dslope f c z0, i.e. f(z) = f(c) + (z − c)·C for all z in B(c, R1).
Русский
Пусть f: ℂ → E дифференцируема на окрестности Ball(c, R1), отображает Ball(c, R1) в Ball(f(c), R2), и существует z0 ∈ Ball(c, R1) такое, что ‖dslope f c z0‖ = R2/R1. Тогда на Ball(c, R1) функция f совпадает с афинной картой f(c) + (z − c)·C, где ‖C‖ = R2/R1.
LaTeX
$$$\exists C \in E, \|C\| = \dfrac{R_2}{R_1} \land \text{EqOn } f (\lambda z \mapsto f(c) + (z - c) \cdot C) (\text{ball } c R_1)$$$
Lean4
theorem affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div' [CompleteSpace E] [StrictConvexSpace ℝ E]
(hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : Set.MapsTo f (ball c R₁) (ball (f c) R₂))
(h_z₀ : ∃ z₀ ∈ ball c R₁, ‖dslope f c z₀‖ = R₂ / R₁) :
∃ C : E, ‖C‖ = R₂ / R₁ ∧ Set.EqOn f (fun z => f c + (z - c) • C) (ball c R₁) :=
let ⟨z₀, h_z₀, h_eq⟩ := h_z₀
⟨dslope f c z₀, h_eq, affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div hd h_maps h_z₀ h_eq⟩
