English
On open sets, AnalyticOn and AnalyticOnNhd coincide; i.e., AnalyticOn 𝕜 f s is equivalent to AnalyticOnNhd 𝕜 f s whenever s is open.
Русский
На открытых множествам аналитичность по функции совпадает с аналитичностью в ближайших окрестностях: AnalyticOn 𝕜 f s ⇔ AnalyticOnNhd 𝕜 f s при IsOpen s.
LaTeX
$$$IsOpen(s) \Rightarrow (AnalyticOn 𝕜 f s \;\Leftrightarrow\; AnalyticOnNhd 𝕜 f s)$$$
Lean4
/-- On open sets, `AnalyticOnNhd` and `AnalyticOn` coincide -/
theorem analyticOn_iff_analyticOnNhd {f : E → F} {s : Set E} (hs : IsOpen s) : AnalyticOn 𝕜 f s ↔ AnalyticOnNhd 𝕜 f s :=
by
refine ⟨?_, AnalyticOnNhd.analyticOn⟩
intro hf x m
rcases Metric.mem_nhds_iff.mp (hs.mem_nhds m) with ⟨r, r0, rs⟩
rcases hf x m with ⟨p, t, fp⟩
exact
⟨p, min (.ofReal r) t,
{ r_pos := lt_min (by positivity) fp.r_pos
r_le := min_le_of_right_le fp.r_le
hasSum := by
intro y ym
simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at ym
refine fp.hasSum ?_ ym.2
apply mem_insert_of_mem
apply rs
simp only [Metric.mem_ball, dist_self_add_left, ym.1] }⟩
