Holomorphic functions are analytic

Stream: new members

[Vincent Beffara]

There are removable singularities, but I did not find this basic result in mathlib:

import analysis.analytic.basic
import analysis.calculus.fderiv
import analysis.complex.removable_singularity

variables {U : set ℂ} {f : ℂ → ℂ}

open filter

lemma analytic_at_of_differentiable_on (U_open : is_open U) (f_diff : differentiable_on ℂ f U)
  ⦃z : ℂ⦄ (hz : z ∈ U) : analytic_at ℂ f z :=
begin
  apply complex.analytic_at_of_differentiable_on_punctured_nhds_of_continuous_at,
  { refine ⟨{z : ℂ | differentiable_at ℂ f z}, _, set.univ, univ_mem, (set.inter_univ _).symm⟩,
    refine mem_of_superset (U_open.mem_nhds_iff.mpr hz) _,
    exact λ w hw, f_diff.differentiable_at (U_open.mem_nhds_iff.mpr hw) },
  { exact f_diff.continuous_on.continuous_at (U_open.mem_nhds_iff.mpr hz) }
end

I'm kind of happy with the statement, but the style of the proof (especially the middle 3 lines) feels like the atrocious attempt at hammering through filters. What is the right way to write this proof? I.e., if a property holds in an open set, it holds on a punctured neighborhood of any point in the set.

[Vincent Beffara]

Ah, I knew I should have asked earlier ...

import analysis.analytic.basic
import analysis.calculus.fderiv
import analysis.complex.removable_singularity

variables {U : set ℂ} {f : ℂ → ℂ}

open filter

lemma analytic_at_of_differentiable_on (U_open : is_open U) (f_diff : differentiable_on ℂ f U)
  ⦃z : ℂ⦄ (hz : z ∈ U) : analytic_at ℂ f z :=
begin
  apply complex.analytic_at_of_differentiable_on_punctured_nhds_of_continuous_at,
  { apply eventually.filter_mono nhds_within_le_nhds,
    apply eventually_of_mem (U_open.mem_nhds_iff.mpr hz),
    exact λ w hw, f_diff.differentiable_at (U_open.mem_nhds_iff.mpr hw) },
  { exact f_diff.continuous_on.continuous_at (U_open.mem_nhds_iff.mpr hz) }
end

This feels a little bit better. Am I on the right track?

[Anatole Dedecker]

I think you're trying to use too strong theorems, did you see docs#differentiable_on.analytic_at ?

[Vincent Beffara]

Ah indeed I had missed it, not sure how :face_palm:

[Anatole Dedecker]

Then you can do

import analysis.complex.cauchy_integral

variables {U : set ℂ} {f : ℂ → ℂ}

open filter

lemma analytic_at_of_differentiable_on (U_open : is_open U) (f_diff : differentiable_on ℂ f U)
  ⦃z : ℂ⦄ (hz : z ∈ U) : analytic_at ℂ f z :=
f_diff.analytic_at (U_open.mem_nhds hz)

[Patrick Massot]

Anatole's answer is of course the right one, but the question of how to avoid fighting against filters is still valid, so let me write:

import analysis.analytic.basic
import analysis.calculus.fderiv
import analysis.complex.removable_singularity

variables {U : set ℂ} {f : ℂ → ℂ}

open filter

lemma analytic_at_of_differentiable_on (U_open : is_open U) (f_diff : differentiable_on ℂ f U)
  ⦃z : ℂ⦄ (hz : z ∈ U) : analytic_at ℂ f z :=
begin
  apply complex.analytic_at_of_differentiable_on_punctured_nhds_of_continuous_at,
  { apply eventually_nhds_within_of_eventually_nhds,
    exact f_diff.eventually_differentiable_at (U_open.mem_nhds hz) },
  { exact f_diff.continuous_on.continuous_at (U_open.mem_nhds_iff.mpr hz) }
end