English
AnalyticWithinAt 𝕜 f s x is equivalent to there exists a g with f x = g x, EqOn f g (insert x s) and AnalyticAt 𝕜 g x.
Русский
AnalyticWithinAt 𝕜 f s x эквивалентно существованию g such that f x = g x, EqOn f g (insert x s) и AnalyticAt 𝕜 g x.
LaTeX
$$$AnalyticWithinAt 𝕜 f s x \iff \exists g, f x = g x \land EqOn f g (insert x s) \land AnalyticAt 𝕜 g x$$$
Lean4
/-- `f` is analytic within `s` at `x` iff some local extension of `f` is analytic at `x`. In this
version, we make sure that the extension coincides with `f` on all of `insert x s`. -/
theorem analyticWithinAt_iff_exists_analyticAt' [CompleteSpace F] {f : E → F} {s : Set E} {x : E} :
AnalyticWithinAt 𝕜 f s x ↔ ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x := by
classical
simp only [analyticWithinAt_iff_exists_analyticAt]
refine ⟨?_, ?_⟩
· rintro ⟨g, hf, hg⟩
rcases mem_nhdsWithin.1 hf with ⟨u, u_open, xu, hu⟩
let g' := Set.piecewise u g f
refine ⟨g', ?_, ?_, ?_⟩
· have : x ∈ u ∩ insert x s := ⟨xu, by simp⟩
simpa [g', xu, this] using hu this
· intro y hy
by_cases h'y : y ∈ u
· have : y ∈ u ∩ insert x s := ⟨h'y, hy⟩
simpa [g', h'y, this] using hu this
· simp [g', h'y]
· apply hg.congr
filter_upwards [u_open.mem_nhds xu] with y hy using by simp [g', hy]
· rintro ⟨g, -, hf, hg⟩
exact ⟨g, by filter_upwards [self_mem_nhdsWithin] using hf, hg⟩
