Skip to content

Commit

Permalink
bump to nightly-2023-03-10-14
Browse files Browse the repository at this point in the history 
mathlib commit leanprover-community/mathlib@ddec54a
  • Loading branch information
@leanprover-community-bot
leanprover-community-bot committed Mar 10, 2023
1 parent 252357f commit 24f1489
Show file tree
Hide file tree
Showing 61 changed files with 2,070 additions and 790 deletions.
58 changes: 31 additions & 27 deletions Mathbin/Analysis/Complex/Basic.lean
View file
Expand Up @@ -47,30 +47,31 @@ namespace Complex
open ComplexConjugate Topology

instance : Norm ℂ :=
⟨abs⟩
⟨Complex.AbsTheory.Complex.abs⟩

@[simp]
theorem norm_eq_abs (z : ℂ) : ‖z‖ = abs z :=
theorem norm_eq_abs (z : ℂ) : ‖z‖ = Complex.AbsTheory.Complex.abs z :=
rfl
#align complex.norm_eq_abs Complex.norm_eq_abs

theorem norm_exp_of_real_mul_i (t : ℝ) : ‖exp (t * i)‖ = 1 := by
theorem norm_exp_of_real_mul_i (t : ℝ) : ‖exp (t * I)‖ = 1 := by
simp only [norm_eq_abs, abs_exp_of_real_mul_I]
#align complex.norm_exp_of_real_mul_I Complex.norm_exp_of_real_mul_i

instance : NormedAddCommGroup ℂ :=
AddGroupNorm.toNormedAddCommGroup
{ abs with
map_zero' := map_zero abs
neg' := abs.map_neg
eq_zero_of_map_eq_zero' := fun _ => abs.eq_zero.1 }
{
Complex.AbsTheory.Complex.abs with
map_zero' := map_zero Complex.AbsTheory.Complex.abs
neg' := Complex.AbsTheory.Complex.abs.map_neg
eq_zero_of_map_eq_zero' := fun _ => Complex.AbsTheory.Complex.abs.eq_zero.1 }

instance : NormedField ℂ :=
{ Complex.field,
Complex.normedAddCommGroup with
norm := abs
norm := Complex.AbsTheory.Complex.abs
dist_eq := fun _ _ => rfl
norm_mul' := map_mul abs }
norm_mul' := map_mul Complex.AbsTheory.Complex.abs }

instance : DenselyNormedField ℂ
where lt_norm_lt r₁ r₂ h₀ hr :=
Expand All @@ -95,7 +96,7 @@ instance (priority := 900) NormedSpace.complexToReal : NormedSpace ℝ E :=
NormedSpace.restrictScalars ℝ ℂ E
#align normed_space.complex_to_real NormedSpace.complexToReal

theorem dist_eq (z w : ℂ) : dist z w = abs (z - w) :=
theorem dist_eq (z w : ℂ) : dist z w = Complex.AbsTheory.Complex.abs (z - w) :=
rfl
#align complex.dist_eq Complex.dist_eq

Expand Down Expand Up @@ -152,12 +153,12 @@ theorem nndist_self_conj (z : ℂ) : nndist z (conj z) = 2 * Real.nnabs z.im :=
#align complex.nndist_self_conj Complex.nndist_self_conj

@[simp]
theorem comap_abs_nhds_zero : Filter.comap abs (𝓝 0) = 𝓝 0 :=
theorem comap_abs_nhds_zero : Filter.comap Complex.AbsTheory.Complex.abs (𝓝 0) = 𝓝 0 :=
comap_norm_nhds_zero
#align complex.comap_abs_nhds_zero Complex.comap_abs_nhds_zero

theorem norm_real (r : ℝ) : ‖(r : ℂ)‖ = ‖r‖ :=
abs_of_real _
abs_ofReal _
#align complex.norm_real Complex.norm_real

@[simp]
Expand All @@ -181,7 +182,7 @@ theorem norm_int_of_nonneg {n : ℤ} (hn : 0 ≤ n) : ‖(n : ℂ)‖ = n := by
#align complex.norm_int_of_nonneg Complex.norm_int_of_nonneg

@[continuity]
theorem continuous_abs : Continuous abs :=
theorem continuous_abs : Continuous Complex.AbsTheory.Complex.abs :=
continuous_norm
#align complex.continuous_abs Complex.continuous_abs

Expand Down Expand Up @@ -215,12 +216,12 @@ theorem norm_eq_one_of_pow_eq_one {ζ : ℂ} {n : ℕ} (h : ζ ^ n = 1) (hn : n
congr_arg coe (nnnorm_eq_one_of_pow_eq_one h hn)
#align complex.norm_eq_one_of_pow_eq_one Complex.norm_eq_one_of_pow_eq_one

theorem equivRealProd_apply_le (z : ℂ) : ‖equivRealProd z‖ ≤ abs z := by
theorem equivRealProd_apply_le (z : ℂ) : ‖equivRealProd z‖ ≤ Complex.AbsTheory.Complex.abs z := by
simp [Prod.norm_def, abs_re_le_abs, abs_im_le_abs]
#align complex.equiv_real_prod_apply_le Complex.equivRealProd_apply_le

theorem equivRealProd_apply_le' (z : ℂ) : ‖equivRealProd z‖ ≤ 1 * abs z := by
simpa using equiv_real_prod_apply_le z
theorem equivRealProd_apply_le' (z : ℂ) : ‖equivRealProd z‖ ≤ 1 * Complex.AbsTheory.Complex.abs z :=
by simpa using equiv_real_prod_apply_le z
#align complex.equiv_real_prod_apply_le' Complex.equivRealProd_apply_le'

theorem lipschitz_equivRealProd : LipschitzWith 1 equivRealProd := by
Expand Down Expand Up @@ -249,7 +250,8 @@ instance : ProperSpace ℂ :=
(id lipschitz_equivRealProd : LipschitzWith 1 equivRealProdClm.toHomeomorph).ProperSpace

/-- The `abs` function on `ℂ` is proper. -/
theorem tendsto_abs_cocompact_atTop : Filter.Tendsto abs (Filter.cocompact ℂ) Filter.atTop :=
theorem tendsto_abs_cocompact_atTop :
Filter.Tendsto Complex.AbsTheory.Complex.abs (Filter.cocompact ℂ) Filter.atTop :=
tendsto_norm_cocompact_atTop
#align complex.tendsto_abs_cocompact_at_top Complex.tendsto_abs_cocompact_atTop

Expand Down Expand Up @@ -304,7 +306,7 @@ theorem imClm_apply (z : ℂ) : (imClm : ℂ → ℝ) z = z.im :=

theorem restrictScalars_one_smul_right' (x : E) :
ContinuousLinearMap.restrictScalars ℝ ((1 : ℂ →L[ℂ] ℂ).smul_right x : ℂ →L[ℂ] E) =
reClm.smul_right x + i • imClm.smul_right x :=
reClm.smul_right x + I • imClm.smul_right x :=
by
ext ⟨a, b⟩
simp [mk_eq_add_mul_I, add_smul, mul_smul, smul_comm I]
Expand Down Expand Up @@ -430,31 +432,31 @@ noncomputable instance : IsROrC ℂ
where
re := ⟨Complex.re, Complex.zero_re, Complex.add_re⟩
im := ⟨Complex.im, Complex.zero_im, Complex.add_im⟩
i := Complex.i
I := Complex.I
i_re_ax := by simp only [AddMonoidHom.coe_mk, Complex.i_re]
i_mul_i_ax := by simp only [Complex.i_mul_i, eq_self_iff_true, or_true_iff]
i_mul_i_ax := by simp only [Complex.i_mul_I, eq_self_iff_true, or_true_iff]
re_add_im_ax z := by
simp only [AddMonoidHom.coe_mk, Complex.re_add_im, Complex.coe_algebraMap,
Complex.ofReal_eq_coe]
of_real_re_ax r := by
simp only [AddMonoidHom.coe_mk, Complex.of_real_re, Complex.coe_algebraMap,
simp only [AddMonoidHom.coe_mk, Complex.ofReal_re, Complex.coe_algebraMap,
Complex.ofReal_eq_coe]
of_real_im_ax r := by
simp only [AddMonoidHom.coe_mk, Complex.of_real_im, Complex.coe_algebraMap,
simp only [AddMonoidHom.coe_mk, Complex.ofReal_im, Complex.coe_algebraMap,
Complex.ofReal_eq_coe]
mul_re_ax z w := by simp only [Complex.mul_re, AddMonoidHom.coe_mk]
mul_im_ax z w := by simp only [AddMonoidHom.coe_mk, Complex.mul_im]
conj_re_ax z := rfl
conj_im_ax z := rfl
conj_i_ax := by simp only [Complex.conj_i, RingHom.coe_mk]
conj_i_ax := by simp only [Complex.conj_I, RingHom.coe_mk]
norm_sq_eq_def_ax z := by
simp only [← Complex.normSq_eq_abs, ← Complex.normSq_apply, AddMonoidHom.coe_mk,
Complex.norm_eq_abs]
mul_im_i_ax z := by simp only [mul_one, AddMonoidHom.coe_mk, Complex.i_im]
inv_def_ax z := by
simp only [Complex.inv_def, Complex.normSq_eq_abs, Complex.coe_algebraMap,
Complex.ofReal_eq_coe, Complex.norm_eq_abs]
div_i_ax := Complex.div_i
div_i_ax := Complex.div_I

theorem IsROrC.re_eq_complex_re : ⇑(IsROrC.re : ℂ →+ ℝ) = Complex.re :=
rfl
Expand All @@ -469,7 +471,8 @@ section ComplexOrder
open ComplexOrder

theorem eq_coe_norm_of_nonneg {z : ℂ} (hz : 0 ≤ z) : z = ↑‖z‖ := by
rw [eq_re_of_real_le hz, IsROrC.norm_of_real, Real.norm_of_nonneg (Complex.le_def.2 hz).1]
rw [eq_re_of_real_le hz, IsROrC.norm_of_real,
Real.norm_of_nonneg (Complex.ComplexOrder.le_def.2 hz).1]
#align complex.eq_coe_norm_of_nonneg Complex.eq_coe_norm_of_nonneg

end ComplexOrder
Expand Down Expand Up @@ -506,7 +509,7 @@ theorem im_to_complex {x : ℂ} : imC x = x.im :=
#align is_R_or_C.im_to_complex IsROrC.im_to_complex

@[simp]
theorem i_to_complex : IC = Complex.i :=
theorem i_to_complex : IC = Complex.I :=
rfl
#align is_R_or_C.I_to_complex IsROrC.i_to_complex

Expand All @@ -516,7 +519,8 @@ theorem normSq_to_complex {x : ℂ} : norm_sqC x = Complex.normSq x := by
#align is_R_or_C.norm_sq_to_complex IsROrC.normSq_to_complex

@[simp]
theorem abs_to_complex {x : ℂ} : absC x = Complex.abs x := by simp [IsROrC.abs, Complex.abs]
theorem abs_to_complex {x : ℂ} : absC x = Complex.AbsTheory.Complex.abs x := by
simp [IsROrC.abs, Complex.AbsTheory.Complex.abs]
#align is_R_or_C.abs_to_complex IsROrC.abs_to_complex

section tsum
Expand Down
66 changes: 33 additions & 33 deletions Mathbin/Analysis/Complex/CauchyIntegral.lean
View file
Expand Up @@ -173,11 +173,11 @@ theorem integral_boundary_rect_of_hasFderivAt_real_off_countable (f : ℂ → E)
(Hd :
∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s,
HasFderivAt f (f' x) x)
(Hi : IntegrableOn (fun z => i • f' z 1 - f' z i) ([z.re, w.re] ×ℂ [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 :=
(Hi : IntegrableOn (fun z => I • f' z 1 - f' z I) ([z.re, w.re] ×ℂ [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 :=
by
set e : (ℝ × ℝ) ≃L[ℝ] ℂ := equiv_real_prod_clm.symm
have he : ∀ x y : ℝ, ↑x + ↑y * I = e (x, y) := fun x y => (mk_eq_add_mul_I x y).symm
Expand Down Expand Up @@ -226,11 +226,11 @@ theorem integral_boundary_rect_of_continuousOn_of_hasFderivAt_real (f : ℂ →
(Hd :
∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im),
HasFderivAt f (f' x) x)
(Hi : IntegrableOn (fun z => i • f' z 1 - f' z i) ([z.re, w.re] ×ℂ [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 :=
(Hi : IntegrableOn (fun z => I • f' z 1 - f' z I) ([z.re, w.re] ×ℂ [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_hasFderivAt_real_off_countable f f' z w ∅ countable_empty Hc
(fun x hx => Hd x hx.1) Hi
#align complex.integral_boundary_rect_of_continuous_on_of_has_fderiv_at_real Complex.integral_boundary_rect_of_continuousOn_of_hasFderivAt_real
Expand All @@ -243,12 +243,12 @@ over the rectangle. -/
theorem integral_boundary_rect_of_differentiableOn_real (f : ℂ → E) (z w : ℂ)
(Hd : DifferentiableOn ℝ f ([z.re, w.re] ×ℂ [z.im, w.im]))
(Hi :
IntegrableOn (fun z => i • fderiv ℝ f z 1 - fderiv ℝ f z i) ([z.re, w.re] ×ℂ [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)) =
IntegrableOn (fun z => I • fderiv ℝ f z 1 - fderiv ℝ f z I) ([z.re, w.re] ×ℂ [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 :=
∫ y : ℝ in z.im..w.im, I • fderiv ℝ f (x + y * I) 1 - fderiv ℝ f (x + y * I) I :=
integral_boundary_rect_of_hasFderivAt_real_off_countable f (fderiv ℝ f) z w ∅ countable_empty
Hd.ContinuousOn
(fun x hx =>
Expand All @@ -267,9 +267,9 @@ theorem integral_boundary_rect_eq_zero_of_differentiable_on_off_countable (f :
(Hd :
∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s,
DifferentiableAt ℂ f x) :
((((∫ 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, 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'
Expand All @@ -289,9 +289,9 @@ theorem integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn (f :
(Hd :
DifferentiableOn ℂ f
(Ioo (min z.re w.re) (max z.re w.re) ×ℂ 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)) =
((((∫ 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
fun x hx => Hd.DifferentiableAt <| (isOpen_Ioo.reProdIm isOpen_Ioo).mem_nhds hx.1
Expand All @@ -302,9 +302,9 @@ over the boundary of a rectangle equals zero. More precisely, if `f` is complex
closed rectangle, then its integral over the boundary of the rectangle equals zero. -/
theorem integral_boundary_rect_eq_zero_of_differentiableOn (f : ℂ → E) (z w : ℂ)
(H : DifferentiableOn ℂ f ([z.re, w.re] ×ℂ [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, 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_continuousOn_of_differentiableOn f z w H.ContinuousOn <|
H.mono <|
Expand Down Expand Up @@ -383,7 +383,7 @@ theorem circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of
{R : ℝ} (h0 : 0 < R) {f : ℂ → E} {y : E} {s : Set ℂ} (hs : s.Countable)
(hc : ContinuousOn f (closedBall c R \ {c}))
(hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z) (hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)) :
(∮ z in C(c, R), (z - c)⁻¹ • f z) = (2 * π * i : ℂ) • y :=
(∮ z in C(c, R), (z - c)⁻¹ • f z) = (2 * π * I : ℂ) • y :=
by
rw [← sub_eq_zero, ← norm_le_zero_iff]
refine' le_of_forall_le_of_dense fun ε ε0 => _
Expand Down Expand Up @@ -443,7 +443,7 @@ interior, then the integral $\oint_{|z-c|=R} \frac{f(z)}{z-c}\,dz$ is equal to $
theorem circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable {R : ℝ} (h0 : 0 < R)
{f : ℂ → E} {c : ℂ} {s : Set ℂ} (hs : s.Countable) (hc : ContinuousOn f (closedBall c R))
(hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z) :
(∮ z in C(c, R), (z - c)⁻¹ • f z) = (2 * π * i : ℂ) • f c :=
(∮ z in C(c, R), (z - c)⁻¹ • f z) = (2 * π * I : ℂ) • f c :=
circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto h0 hs
(hc.mono <| diff_subset _ _) (fun z hz => hd z ⟨hz.1.1, hz.2⟩)
(hc.ContinuousAt <| closedBall_mem_nhds _ h0).ContinuousWithinAt
Expand Down Expand Up @@ -474,7 +474,7 @@ theorem circleIntegral_eq_zero_of_differentiable_on_off_countable {R : ℝ} (h0
theorem circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux {R : ℝ} {c w : ℂ}
{f : ℂ → E} {s : Set ℂ} (hs : s.Countable) (hw : w ∈ ball c R \ s)
(hc : ContinuousOn f (closedBall c R)) (hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x) :
(∮ z in C(c, R), (z - w)⁻¹ • f z) = (2 * π * i : ℂ) • f w :=
(∮ z in C(c, R), (z - w)⁻¹ • f z) = (2 * π * I : ℂ) • f w :=
by
have hR : 0 < R := dist_nonneg.trans_lt hw.1
set F : ℂ → E := dslope f w
Expand Down Expand Up @@ -509,7 +509,7 @@ interior we have $\frac{1}{2πi}\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=f(w)$.
theorem two_pi_i_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable {R : ℝ}
{c w : ℂ} {f : ℂ → E} {s : Set ℂ} (hs : s.Countable) (hw : w ∈ ball c R)
(hc : ContinuousOn f (closedBall c R)) (hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x) :
((2 * π * i : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z) = f w :=
((2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z) = f w :=
by
have hR : 0 < R := dist_nonneg.trans_lt hw
suffices w ∈ closure (ball c R \ s) by
Expand Down Expand Up @@ -551,7 +551,7 @@ interior we have $\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)$.
theorem circleIntegral_sub_inv_smul_of_differentiable_on_off_countable {R : ℝ} {c w : ℂ} {f : ℂ → E}
{s : Set ℂ} (hs : s.Countable) (hw : w ∈ ball c R) (hc : ContinuousOn f (closedBall c R))
(hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x) :
(∮ z in C(c, R), (z - w)⁻¹ • f z) = (2 * π * i : ℂ) • f w :=
(∮ z in C(c, R), (z - w)⁻¹ • f z) = (2 * π * I : ℂ) • f w :=
by
rw [←
two_pi_I_inv_smul_circle_integral_sub_inv_smul_of_differentiable_on_off_countable hs hw hc hd,
Expand All @@ -564,7 +564,7 @@ continuous on its closure, then for any `w` in this open ball we have
$\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)$. -/
theorem DiffContOnCl.circleIntegral_sub_inv_smul {R : ℝ} {c w : ℂ} {f : ℂ → E}
(h : DiffContOnCl ℂ f (ball c R)) (hw : w ∈ ball c R) :
(∮ z in C(c, R), (z - w)⁻¹ • f z) = (2 * π * i : ℂ) • f w :=
(∮ z in C(c, R), (z - w)⁻¹ • f z) = (2 * π * I : ℂ) • f w :=
circleIntegral_sub_inv_smul_of_differentiable_on_off_countable countable_empty hw
h.continuousOn_ball fun x hx => h.DifferentiableAt isOpen_ball hx.1
#align diff_cont_on_cl.circle_integral_sub_inv_smul DiffContOnCl.circleIntegral_sub_inv_smul
Expand All @@ -574,7 +574,7 @@ continuous on its closure, then for any `w` in this open ball we have
$\frac{1}{2πi}\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=f(w)$. -/
theorem DiffContOnCl.two_pi_i_inv_smul_circleIntegral_sub_inv_smul {R : ℝ} {c w : ℂ} {f : ℂ → E}
(hf : DiffContOnCl ℂ f (ball c R)) (hw : w ∈ ball c R) :
((2 * π * i : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z) = f w :=
((2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z) = f w :=
by
have hR : 0 < R := not_le.mp (ball_eq_empty.not.mp (nonempty_of_mem hw).ne_empty)
refine'
Expand All @@ -588,7 +588,7 @@ theorem DiffContOnCl.two_pi_i_inv_smul_circleIntegral_sub_inv_smul {R : ℝ} {c
`R`, then for any `w` in its interior we have $\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)$. -/
theorem DifferentiableOn.circleIntegral_sub_inv_smul {R : ℝ} {c w : ℂ} {f : ℂ → E}
(hd : DifferentiableOn ℂ f (closedBall c R)) (hw : w ∈ ball c R) :
(∮ z in C(c, R), (z - w)⁻¹ • f z) = (2 * π * i : ℂ) • f w :=
(∮ z in C(c, R), (z - w)⁻¹ • f z) = (2 * π * I : ℂ) • f w :=
(hd.mono closure_ball_subset_closedBall).DiffContOnCl.circleIntegral_sub_inv_smul hw
#align differentiable_on.circle_integral_sub_inv_smul DifferentiableOn.circleIntegral_sub_inv_smul

Expand All @@ -599,7 +599,7 @@ interior we have $\oint_{|z-c|=R}\frac{f(z)}{z-w}dz=2\pi i\,f(w)$.
theorem circleIntegral_div_sub_of_differentiable_on_off_countable {R : ℝ} {c w : ℂ} {s : Set ℂ}
(hs : s.Countable) (hw : w ∈ ball c R) {f : ℂ → ℂ} (hc : ContinuousOn f (closedBall c R))
(hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z) :
(∮ z in C(c, R), f z / (z - w)) = 2 * π * i * f w := by
(∮ z in C(c, R), f z / (z - w)) = 2 * π * I * f w := by
simpa only [smul_eq_mul, div_eq_inv_mul] using
circle_integral_sub_inv_smul_of_differentiable_on_off_countable hs hw hc hd
#align complex.circle_integral_div_sub_of_differentiable_on_off_countable Complex.circleIntegral_div_sub_of_differentiable_on_off_countable
Expand Down

0 comments on commit 24f1489

Please sign in to comment.