removable singularity

Stream: maths

[Yury G. Kudryashov]

Hi, do we need the [complete_space E] assumption in docs#complex.differentiable_on_update_lim_of_is_o and related results? In other words, is it possible that the values of an analytic function $f\colon \mathbb C\to E$ belong to a non-closed complex subspace $F\subset E$ for all points but one.
I can neither prove nor disprove the version without [complete_space E] assumption.

[Yury G. Kudryashov]

@Sebastien Gouezel Any ideas?

[Sebastien Gouezel]

No idea (I mean, no counterexample, but my guess is that the assumption [complete_space E] is necessary). By the way, this theorem is expressed in a slightly strange way, since the assumption is that f z - f c = o(1/(z-c)), but then the value of f c is ditched as it might not be the right one, and replaced by the limit of f at c. Given this, wouldn't it be more natural to have an assumption f z = o(1/(z-c)) (which is equivalent to the previous one)?

[Yury G. Kudryashov]

Indeed, it is equivalent. I'll update this theorem.

[Junyan Xu]

I think it's better to replace f c by any w : ℂ. But yes it doesn't matter as you can just update the value at c to be w. replace f by f - f c.

[Junyan Xu]

I also think it would be nice to specialize docs#sum_cauchy_power_series_eq_integral etc. to w=0, which can then be used to golf docs#circle_integral.integral_sub_inv_of_mem_ball.

[Junyan Xu]

It turns out the [complete_space] assumption is indeed necessary. Let the complex analytic function f : ℂ → ℓ^2(ℂ) defined by f(z) = (1, z, z^2, z^3, ...). Then any set of values is linear independent, because any finite subset is, by non-vanishing of the Vandermonde determinant. So if you take F to be the span of f(0 < |z| < 1), then f(0) is not in the span.