English
Under analytic continuation and punctured differentiability, differentiability on s is equivalent to differentiability on s ∪ {c} under mild hypotheses.
Русский
При аналитическом продолжении и дифференцируемости на пунктированной области, дифференцируемость на s эквивалентна дифференцируемости на s ∪ {c} при слабых предпосылках.
LaTeX
$$$\text{DifferentiableOn } f \text{ on } s \iff \text{DifferentiableOn } f \text{ on } s \cup \{c\}$ under suitable hypotheses.$$
Lean4
/-- Equality case in the **Schwarz Lemma**: in the setup of `norm_dslope_le_div_of_mapsTo_ball`, if
`‖dslope f c z₀‖ = R₂ / R₁` holds at a point in the ball then the map `f` is affine. -/
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₁)
(h_eq : ‖dslope f c z₀‖ = R₂ / R₁) : Set.EqOn f (fun z => f c + (z - c) • dslope f c z₀) (ball c R₁) :=
by
set g := dslope f c
rintro z hz
by_cases h : z = c; · simp [h]
have h_R₁ : 0 < R₁ := nonempty_ball.mp ⟨_, h_z₀⟩
have g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁ := fun z hz => norm_dslope_le_div_of_mapsTo_ball hd h_maps hz
have g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀ := isMaxOn_iff.mpr fun z hz => by simpa [h_eq] using g_le_div z hz
have g_diff : DifferentiableOn ℂ g (ball c R₁) :=
(differentiableOn_dslope (isOpen_ball.mem_nhds (mem_ball_self h_R₁))).mpr hd
have : g z = g z₀ :=
eqOn_of_isPreconnected_of_isMaxOn_norm (convex_ball c R₁).isPreconnected isOpen_ball g_diff h_z₀ g_max hz
simp only [g] at this
simp [g, ← this]
