feat(analysis/complex/cauchy_integral): review docs, add versions wit…

…hout `off_countable` (#11417)

src/analysis/complex/cauchy_integral.lean

@@ -7,6 +7,7 @@ import measure_theory.measure.complex_lebesgue
 import measure_theory.integral.divergence_theorem
 import measure_theory.integral.circle_integral
 import analysis.analytic.basic
+import analysis.complex.re_im_topology
 import data.real.cardinality
 
 /-!
@@ -140,22 +141,20 @@ open_locale interval real nnreal ennreal topological_space big_operators
 
 noncomputable theory
 
-universes u v
+universes u
 
 variables {E : Type u} [normed_group E] [normed_space ℂ E] [measurable_space E] [borel_space E]
   [second_countable_topology E] [complete_space E]
 
 namespace complex
 
-/-- Suppose that a function `f : ℂ → E` is real differentiable on a rectangle with vertices
-`z w : ℂ` and $\frac{\partial f}{\partial \bar z}$ is integrable on this rectangle. Then
-the integral of `f` over the boundary of the rectangle is equal to the integral of
+/-- Suppose that a function `f : ℂ → E` is continuous on a closed rectangle with opposite corners at
+`z w : ℂ`, is *real* differentiable at all but countably many points of the corresponding open
+rectangle, and $\frac{\partial f}{\partial \bar z}$ is integrable on this rectangle. Then the
+integral of `f` over the boundary of the rectangle is equal to the integral of
 $2i\frac{\partial f}{\partial \bar z}=i\frac{\partial f}{\partial x}-\frac{\partial f}{\partial y}$
-over the rectangle.
-
-Moreover, the same is true if `f` is only differentiable at points outside of a countable set `s`
-and is continuous at the points of this set. -/
-lemma integral_boundary_rect_of_has_fderiv_within_at_real_off_countable (f : ℂ → E)
+over the rectangle. -/
+lemma integral_boundary_rect_of_has_fderiv_at_real_off_countable (f : ℂ → E)
   (f' : ℂ → ℂ →L[ℝ] E) (z w : ℂ) (s : set ℂ) (hs : countable s)
   (Hc : continuous_on f (re ⁻¹' [z.re, w.re] ∩ im ⁻¹' [z.im, w.im]))
   (Hd : ∀ x ∈ (re ⁻¹' (Ioo (min z.re w.re) (max z.re w.re)) ∩
@@ -190,11 +189,46 @@ begin
   simpa only [hF'] using Hi.neg
 end
 
-/-- **Cauchy theorem**: the integral of a complex differentiable function over the boundary of a
-rectangle equals zero.
+/-- Suppose that a function `f : ℂ → E` is continuous on a closed rectangle with opposite corners at
+`z w : ℂ`, is *real* differentiable on the corresponding open rectangle, and
+$\frac{\partial f}{\partial \bar z}$ is integrable on this rectangle. Then the integral of `f` over
+the boundary of the rectangle is equal to the integral of
+$2i\frac{\partial f}{\partial \bar z}=i\frac{\partial f}{\partial x}-\frac{\partial f}{\partial y}$
+over the rectangle. -/
+lemma integral_boundary_rect_of_continuous_on_of_has_fderiv_at_real (f : ℂ → E)
+  (f' : ℂ → ℂ →L[ℝ] E) (z w : ℂ)
+  (Hc : continuous_on f (re ⁻¹' [z.re, w.re] ∩ im ⁻¹' [z.im, w.im]))
+  (Hd : ∀ x ∈ (re ⁻¹' (Ioo (min z.re w.re) (max z.re w.re)) ∩
+    im ⁻¹' (Ioo (min z.im w.im) (max z.im w.im))), has_fderiv_at f (f' x) x)
+  (Hi : integrable_on (λ z, I • f' z 1 - f' z I) (re ⁻¹' [z.re, w.re] ∩ im ⁻¹' [z.im, w.im])) :
+  (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
+    (I • ∫ y : ℝ in z.im..w.im, f (re w + y * I)) - I • ∫ y : ℝ in z.im..w.im, f (re z + y * I) =
+    ∫ x : ℝ in z.re..w.re, ∫ y : ℝ in z.im..w.im, I • f' (x + y * I) 1 - f' (x + y * I) I :=
+integral_boundary_rect_of_has_fderiv_at_real_off_countable f f' z w ∅ countable_empty Hc
+  (λ x hx, Hd x hx.1) Hi
 
-Moreover, the same is true if `f` is only differentiable at points outside of a countable set `s`
-and is continuous at the points of this set. -/
+/-- Suppose that a function `f : ℂ → E` is *real* differentiable on a closed rectangle with opposite
+corners at `z w : ℂ` and $\frac{\partial f}{\partial \bar z}$ is integrable on this rectangle. Then
+the integral of `f` over the boundary of the rectangle is equal to the integral of
+$2i\frac{\partial f}{\partial \bar z}=i\frac{\partial f}{\partial x}-\frac{\partial f}{\partial y}$
+over the rectangle. -/
+lemma integral_boundary_rect_of_differentiable_on_real (f : ℂ → E) (z w : ℂ)
+  (Hd : differentiable_on ℝ f (re ⁻¹' [z.re, w.re] ∩ im ⁻¹' [z.im, w.im]))
+  (Hi : integrable_on (λ z, I • fderiv ℝ f z 1 - fderiv ℝ f z I)
+    (re ⁻¹' [z.re, w.re] ∩ im ⁻¹' [z.im, w.im])) :
+  (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
+    (I • ∫ y : ℝ in z.im..w.im, f (re w + y * I)) - I • ∫ y : ℝ in z.im..w.im, f (re z + y * I) =
+    ∫ x : ℝ in z.re..w.re, ∫ y : ℝ in z.im..w.im,
+      I • fderiv ℝ f (x + y * I) 1 - fderiv ℝ f (x + y * I) I :=
+integral_boundary_rect_of_has_fderiv_at_real_off_countable f (fderiv ℝ f) z w ∅ countable_empty
+  Hd.continuous_on
+  (λ x hx, Hd.has_fderiv_at $ by simpa only [← mem_interior_iff_mem_nhds,
+    interior_preimage_re_inter_preimage_im, interval, interior_Icc] using hx.1) Hi
+
+/-- **Cauchy theorem**: the integral of a complex differentiable function over the boundary of a
+rectangle equals zero. More precisely, if `f` is continuous on a closed rectangle and is complex
+differentiable at all but countably many points of the corresponding open rectangle, then its
+integral over the boundary of the rectangle equals zero. -/
 lemma integral_boundary_rect_eq_zero_of_differentiable_on_off_countable (f : ℂ → E)
   (z w : ℂ) (s : set ℂ) (hs : countable s)
   (Hc : continuous_on f (re ⁻¹' [z.re, w.re] ∩ im ⁻¹' [z.im, w.im]))
@@ -203,17 +237,41 @@ lemma integral_boundary_rect_eq_zero_of_differentiable_on_off_countable (f : ℂ
   (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
     (I • ∫ y : ℝ in z.im..w.im, f (re w + y * I)) -
       I • ∫ y : ℝ in z.im..w.im, f (re z + y * I) = 0 :=
-by refine (integral_boundary_rect_of_has_fderiv_within_at_real_off_countable f
+by refine (integral_boundary_rect_of_has_fderiv_at_real_off_countable f
   (λ z, (fderiv ℂ f z).restrict_scalars ℝ) z w s hs Hc
   (λ x hx, (Hd x hx).has_fderiv_at.restrict_scalars ℝ) _).trans _;
     simp [← continuous_linear_map.map_smul]
 
-/-- If `f : ℂ → E` is complex differentiable on the closed annulus `r ≤ ∥z - c∥ ≤ R`, `0 < r ≤ R`,
-then the integrals of `f z / (z - c)` (formally, `(z - c)⁻¹ • f z`) over the circles
-`∥z - c∥ = r` and `∥z - c∥ = R` are equal to each other.
+/-- **Cauchy theorem**: the integral of a complex differentiable function over the boundary of a
+rectangle equals zero. More precisely, if `f` is continuous on a closed rectangle and is complex
+differentiable on the corresponding open rectangle, then its integral over the boundary of the
+rectangle equals zero. -/
+lemma integral_boundary_rect_eq_zero_of_continuous_on_of_differentiable_on (f : ℂ → E) (z w : ℂ)
+  (Hc : continuous_on f (re ⁻¹' [z.re, w.re] ∩ im ⁻¹' [z.im, w.im]))
+  (Hd : differentiable_on ℂ f (re ⁻¹' (Ioo (min z.re w.re) (max z.re w.re)) ∩
+    im ⁻¹' (Ioo (min z.im w.im) (max z.im w.im)))) :
+  (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
+    (I • ∫ y : ℝ in z.im..w.im, f (re w + y * I)) -
+      I • ∫ y : ℝ in z.im..w.im, f (re z + y * I) = 0 :=
+integral_boundary_rect_eq_zero_of_differentiable_on_off_countable f z w ∅ countable_empty
+  Hc $ λ x hx, Hd.differentiable_at $ (is_open_Ioo.re_prod_im is_open_Ioo).mem_nhds hx.1
 
-Moreover, the same is true if `f` is differentiable at points of the annulus outside of a countable
-set `s` and is continuous at points of this set.  -/
+/-- **Cauchy theorem**: the integral of a complex differentiable function over the boundary of a
+rectangle equals zero. More precisely, if `f` is complex differentiable on a closed rectangle, then
+its integral over the boundary of the rectangle equals zero. -/
+lemma integral_boundary_rect_eq_zero_of_differentiable_on (f : ℂ → E) (z w : ℂ)
+  (H : differentiable_on ℂ f (re ⁻¹' [z.re, w.re] ∩ im ⁻¹' [z.im, w.im])) :
+  (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
+    (I • ∫ y : ℝ in z.im..w.im, f (re w + y * I)) -
+      I • ∫ y : ℝ in z.im..w.im, f (re z + y * I) = 0 :=
+integral_boundary_rect_eq_zero_of_continuous_on_of_differentiable_on f z w H.continuous_on $
+  H.mono $
+    inter_subset_inter (preimage_mono Ioo_subset_Icc_self) (preimage_mono Ioo_subset_Icc_self)
+
+/-- If `f : ℂ → E` is continuous the closed annulus `r ≤ ∥z - c∥ ≤ R`, `0 < r ≤ R`, and is complex
+differentiable at all but countably many points of its interior, then the integrals of
+`f z / (z - c)` (formally, `(z - c)⁻¹ • f z`) over the circles `∥z - c∥ = r` and `∥z - c∥ = R` are
+equal to each other. -/
 lemma circle_integral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable
   {c : ℂ} {r R : ℝ} (h0 : 0 < r) (hle : r ≤ R) {f : ℂ → E} {s : set ℂ} (hs : countable s)
   (hc : continuous_on f (closed_ball c R \ ball c r))
@@ -248,10 +306,10 @@ begin
       _ hs hc hd
 end
 
-/-- **Cauchy integral formula** for the value at the center of a disc. If `f` is differentiable on a
-punctured closed disc of radius `R` and has a limit `y` at the center of the disc, then the integral
-$\int_{|z|=R} f(z)\,d(\arg z)=-i\int_{|z|=R}\frac{f(z)\,dz}{z}$ is equal to $2πy`. Moreover, the
-same is true if at the points of some countable set, `f` is only continuous, not differentiable. -/
+/-- **Cauchy integral formula** for the value at the center of a disc. If `f` is continuous on a
+punctured closed disc of radius `R`, is differentiable at all but countably many points of the
+interior of this disc, and has a limit `y` at the center of the disc, then the integral
+$\oint_{∥z-c∥=R} \frac{f(z)}{z-c}\,dz$ is equal to $2πiy`. -/
 lemma circle_integral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto
   {c : ℂ} {R : ℝ} (h0 : 0 < R) {f : ℂ → E} {y : E} {s : set ℂ} (hs : countable s)
   (hc : continuous_on f (closed_ball c R \ {c}))
@@ -305,10 +363,9 @@ begin
   ... = ε : by { field_simp [hr0.ne', real.two_pi_pos.ne'], ac_refl }
 end
 
-/-- **Cauchy integral formula** for the value at the center of a disc. If `f` is differentiable on a
-closed disc of radius `R`, then the integral
-$\int_{|z|=R} f(z)\,d(\arg z)=-i\int_{|z|=R}\frac{f(z)\,dz}{z}$ is equal to $2πy`. Moreover, the
-same is true if at the points of some countable set, `f` is only continuous, not differentiable. -/
+/-- **Cauchy integral formula** for the value at the center of a disc. If `f : ℂ → E` is continuous
+on a closed disc of radius `R` and is complex differentiable at all but countably many points of its
+interior, then the integral $\oint_{|z-c|=R} \frac{f(z)}{z-c}\,dz$ is equal to $2πiy`. -/
 lemma circle_integral_sub_center_inv_smul_of_differentiable_on_off_countable {R : ℝ} (h0 : 0 < R)
   {f : ℂ → E} {c : ℂ} {s : set ℂ} (hs : countable s)
   (hc : continuous_on f (closed_ball c R)) (hd : ∀ z ∈ ball c R \ s, differentiable_at ℂ f z) :
@@ -317,9 +374,9 @@ circle_integral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendst
   (hc.mono $ diff_subset _ _) (λ z hz, hd z ⟨hz.1.1, hz.2⟩)
   (hc.continuous_at $ closed_ball_mem_nhds _ h0).continuous_within_at
 
-/-- **Cauchy theorem**: the integral of a complex differentiable function over the boundary of a
-disc equals zero. Moreover, the same is true if at the points of some countable set, `f` is only
-continuous. -/
+/-- **Cauchy theorem**: if `f : ℂ → E` is continuous on a closed ball `{z | ∥z - c∥ ≤ R}` and is
+complex differentiable at all but countably many points of its interior, then the integral
+$\oint_{|z-c|=R}f(z)\,dz$ equals zero. -/
 lemma circle_integral_eq_zero_of_differentiable_on_off_countable {R : ℝ} (h0 : 0 ≤ R) {f : ℂ → E}
   {c : ℂ} {s : set ℂ} (hs : countable s) (hc : continuous_on f (closed_ball c R))
   (hd : ∀ z ∈ ball c R \ s, differentiable_at ℂ f z) :
@@ -378,9 +435,9 @@ begin
     (hc'.smul continuous_on_const).circle_integrable hR.le]
 end
 
-/-- **Cauchy integral formula**: if `f : ℂ → E` is complex differentiable on a closed disc of radius
-`R`, then for any `w` in the corresponding open disc we have
-$\frac{1}{2πi}\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=f(w)$.
+/-- **Cauchy integral formula**: if `f : ℂ → E` is continuous on a closed disc of radius `R` and is
+complex differentiable at all but countably many points of its interior, then for any `w` in this
+interior we have $\frac{1}{2πi}\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=f(w)$.
 -/
 lemma two_pi_I_inv_smul_circle_integral_sub_inv_smul_of_differentiable_on_off_countable
   {R : ℝ} {c w : ℂ} {f : ℂ → E} {s : set ℂ} (hs : countable s) (hw : w ∈ ball c R)
@@ -417,9 +474,9 @@ begin
   exact ⟨g x, (hlu_sub hx.1).1, (hlu_sub hx.1).2, hx.2⟩
 end
 
-/-- **Cauchy integral formula**: if `f : ℂ → E` is complex differentiable on a closed disc of radius
-`R`, then for any `w` in the corresponding open disc we have
-$\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2\pi i\,f(w)$.
+/-- **Cauchy integral formula**: if `f : ℂ → E` is continuous on a closed disc of radius `R` and is
+complex differentiable at all but countably many points of its interior, then for any `w` in this
+interior we have $\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)$.
 -/
 lemma circle_integral_sub_inv_smul_of_differentiable_on_off_countable
   {R : ℝ} {c w : ℂ} {f : ℂ → E} {s : set ℂ} (hs : countable s) (hw : w ∈ ball c R)
@@ -428,9 +485,29 @@ lemma circle_integral_sub_inv_smul_of_differentiable_on_off_countable
 by { rw [← two_pi_I_inv_smul_circle_integral_sub_inv_smul_of_differentiable_on_off_countable
   hs hw hc hd, smul_inv_smul₀], simp [real.pi_ne_zero, I_ne_zero] }
 
-/-- **Cauchy integral formula**: if `f : ℂ → ℂ` is complex differentiable on a closed disc of radius
-`R`, then for any `w` in the corresponding open disc we have
-$\oint_{|z-c|=R}\frac{f(z)}{z-w}dz=2\pi i\,f(w)$. -/
+/-- **Cauchy integral formula**: if `f : ℂ → E` is continuous on a closed disc of radius `R` and is
+complex differentiable on its interior, then for any `w` in this interior we have
+$\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)$.
+-/
+lemma circle_integral_sub_inv_smul_of_continuous_on_of_differentiable_on
+  {R : ℝ} {c w : ℂ} {f : ℂ → E} (hw : w ∈ ball c R)
+  (hc : continuous_on f (closed_ball c R)) (hd : differentiable_on ℂ f (ball c R)) :
+  ∮ z in C(c, R), (z - w)⁻¹ • f z = (2 * π * I : ℂ) • f w :=
+circle_integral_sub_inv_smul_of_differentiable_on_off_countable countable_empty hw hc $ λ z hz,
+  hd.differentiable_at (is_open_ball.mem_nhds hz.1)
+
+/-- **Cauchy integral formula**: if `f : ℂ → E` is complex differentiable on a closed disc of radius
+`R`, then for any `w` in its interior we have $\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)$. -/
+lemma circle_integral_sub_inv_smul_of_differentiable_on
+  {R : ℝ} {c w : ℂ} {f : ℂ → E} (hw : w ∈ ball c R) (hd : differentiable_on ℂ f (closed_ball c R)) :
+  ∮ z in C(c, R), (z - w)⁻¹ • f z = (2 * π * I : ℂ) • f w :=
+circle_integral_sub_inv_smul_of_continuous_on_of_differentiable_on hw hd.continuous_on $
+  hd.mono $ ball_subset_closed_ball
+
+/-- **Cauchy integral formula**: if `f : ℂ → ℂ` is continuous on a closed disc of radius `R` and is
+complex differentiable at all but countably many points of its interior, then for any `w` in this
+interior we have $\oint_{|z-c|=R}\frac{f(z)}{z-w}dz=2\pi i\,f(w)$.
+-/
 lemma circle_integral_div_sub_of_differentiable_on_off_countable {R : ℝ} {c w : ℂ} {s : set ℂ}
   (hs : countable s) (hw : w ∈ ball c R) {f : ℂ → ℂ} (hc : continuous_on f (closed_ball c R))
   (hd : ∀ z ∈ ball c R \ s, differentiable_at ℂ f z) :
@@ -458,6 +535,15 @@ lemma has_fpower_series_on_ball_of_differentiable_off_countable {R : ℝ≥0} {c
         ((hc.mono sphere_subset_closed_ball).circle_integrable R.2) hR).has_sum hw
     end }
 
+/-- If `f : ℂ → E` is continuous on a closed ball of positive radius and is complex differentiable
+on its interior, then it is analytic on the open ball with coefficients of the power series given by
+Cauchy integral formulas. -/
+lemma has_fpower_series_on_ball_of_continuous_on_of_differentiable_on {R : ℝ≥0} {c : ℂ} {f : ℂ → E}
+  (hc : continuous_on f (closed_ball c R)) (hd : differentiable_on ℂ f (ball c R)) (hR : 0 < R) :
+  has_fpower_series_on_ball f (cauchy_power_series f c R) c R :=
+has_fpower_series_on_ball_of_differentiable_off_countable countable_empty hc
+  (λ z hz, hd.differentiable_at $ is_open_ball.mem_nhds hz.1) hR
+
 /-- If `f : ℂ → E` is complex differentiable on a closed disc of positive radius, then it is
 analytic on the corresponding open disc, and the coefficients of the power series are given by
 Cauchy integral formulas. See also
@@ -466,8 +552,8 @@ weaker assumptions. -/
 protected lemma _root_.differentiable_on.has_fpower_series_on_ball {R : ℝ≥0} {c : ℂ} {f : ℂ → E}
   (hd : differentiable_on ℂ f (closed_ball c R)) (hR : 0 < R) :
   has_fpower_series_on_ball f (cauchy_power_series f c R) c R :=
-has_fpower_series_on_ball_of_differentiable_off_countable countable_empty hd.continuous_on
-  (λ z hz, hd.differentiable_at $ closed_ball_mem_nhds_of_mem hz.1) hR
+has_fpower_series_on_ball_of_continuous_on_of_differentiable_on hd.continuous_on
+  (hd.mono ball_subset_closed_ball) hR
 
 /-- If `f : ℂ → E` is complex differentiable on some set `s`, then it is analytic at any point `z`
 such that `s ∈ 𝓝 z` (equivalently, `z ∈ interior s`). -/
@@ -480,7 +566,7 @@ begin
 end
 
 /-- A complex differentiable function `f : ℂ → E` is analytic at every point. -/
-protected lemma differentiable.analytic_at {f : ℂ → E} (hf : differentiable ℂ f) (z : ℂ) :
+protected lemma _root_.differentiable.analytic_at {f : ℂ → E} (hf : differentiable ℂ f) (z : ℂ) :
   analytic_at ℂ f z :=
 hf.differentiable_on.analytic_at univ_mem
 

src/analysis/complex/re_im_topology.lean

@@ -150,3 +150,13 @@ by simpa only [closure_Ici, closure_Iic, frontier_Ici, frontier_Iic]
   using frontier_preimage_re_inter_preimage_im (Ici a) (Iic b)
 
 end complex
+
+open complex
+
+lemma is_open.re_prod_im {s t : set ℝ} (hs : is_open s) (ht : is_open t) :
+  is_open (re ⁻¹' s ∩ im ⁻¹' t) :=
+(hs.preimage continuous_re).inter (ht.preimage continuous_im)
+
+lemma is_closed.re_prod_im {s t : set ℝ} (hs : is_closed s) (ht : is_closed t) :
+  is_closed (re ⁻¹' s ∩ im ⁻¹' t) :=
+(hs.preimage continuous_re).inter (ht.preimage continuous_im)