English
EqOn f 0 on a set follows from analyticity on Nhd and a local zero around a point.
Русский
Из анализа на окрестности и локального нуля следует, что f нулевой на множество.
LaTeX
$$$\\text{EqOn } f\\ 0\\ U$ под условием аналитичности и локального нуля.$$
Lean4
/-- If an analytic function vanishes around a point, then it is uniformly zero along
a connected set. Superseded by `AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero` which
does not assume completeness of the target space. -/
theorem eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux [CompleteSpace F] {f : E → F} {U : Set E}
(hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[𝓝 z₀] 0) : EqOn f 0 U := by
/- Let `u` be the set of points around which `f` vanishes. It is clearly open. We have to show
that its limit points in `U` still belong to it, from which the inclusion `U ⊆ u` will follow
by connectedness. -/
let u := {x | f =ᶠ[𝓝 x] 0}
suffices main : closure u ∩ U ⊆ u
by
have Uu : U ⊆ u := hU.subset_of_closure_inter_subset isOpen_setOf_eventually_nhds ⟨z₀, h₀, hfz₀⟩ main
intro z hz
simpa using
mem_of_mem_nhds
(Uu hz)
/- Take a limit point `x`, then a ball `B (x, r)` on which it has a power series expansion, and
then `y ∈ B (x, r/2) ∩ u`. Then `f` has a power series expansion on `B (y, r/2)` as it is
contained in `B (x, r)`. All the coefficients in this series expansion vanish, as `f` is zero
on a neighborhood of `y`. Therefore, `f` is zero on `B (y, r/2)`. As this ball contains `x`,
it follows that `f` vanishes on a neighborhood of `x`, proving the claim. -/
rintro x ⟨xu, xU⟩
rcases hf x xU with ⟨p, r, hp⟩
obtain ⟨y, yu, hxy⟩ : ∃ y ∈ u, edist x y < r / 2 :=
EMetric.mem_closure_iff.1 xu (r / 2) (ENNReal.half_pos hp.r_pos.ne')
let q := p.changeOrigin (y - x)
have has_series : HasFPowerSeriesOnBall f q y (r / 2) :=
by
have A : (‖y - x‖₊ : ℝ≥0∞) < r / 2 := by rwa [edist_comm, edist_eq_enorm_sub] at hxy
have := hp.changeOrigin (A.trans_le ENNReal.half_le_self)
simp only [add_sub_cancel] at this
apply this.mono (ENNReal.half_pos hp.r_pos.ne')
apply ENNReal.le_sub_of_add_le_left ENNReal.coe_ne_top
apply (add_le_add A.le (le_refl (r / 2))).trans (le_of_eq _)
exact ENNReal.add_halves _
have M : EMetric.ball y (r / 2) ∈ 𝓝 x := EMetric.isOpen_ball.mem_nhds hxy
filter_upwards [M] with z hz
have A : HasSum (fun n : ℕ => q n fun _ : Fin n => z - y) (f z) := has_series.hasSum_sub hz
have B : HasSum (fun n : ℕ => q n fun _ : Fin n => z - y) 0 :=
by
have : HasFPowerSeriesAt 0 q y := has_series.hasFPowerSeriesAt.congr yu
convert hasSum_zero (α := F) using 1
ext n
exact this.apply_eq_zero n _
exact HasSum.unique A B
