Skip to content

Commit bbd46d7

Browse files
AlexKontorovichocfnash
AlexKontorovich
and
ocfnash
committed
feat: a complex differentiable function on a disk has a primitive (leanprover-community#9598)
We prove that holomorphic functions on discs have primitives. TODO: Extend to holomorphic functions on simply connected domains, and use this to define general complex logarithms. Co-authored by: Ian Jauslin ian.jauslin@rutgers.edu Co-authored-by: Oliver Nash <github@olivernash.org>
1 parent 07c7363 commit bbd46d7

4 files changed

Lines changed: 299 additions & 2 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1554,6 +1554,7 @@ import Mathlib.Analysis.Complex.Exponential
15541554
import Mathlib.Analysis.Complex.ExponentialBounds
15551555
import Mathlib.Analysis.Complex.Hadamard
15561556
import Mathlib.Analysis.Complex.HalfPlane
1557+
import Mathlib.Analysis.Complex.HasPrimitives
15571558
import Mathlib.Analysis.Complex.IntegerCompl
15581559
import Mathlib.Analysis.Complex.IsIntegral
15591560
import Mathlib.Analysis.Complex.Isometry

‎Mathlib/Analysis/Complex/Asymptotics.lean‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,12 @@ lemma isBigO_comp_ofReal_nhds_ne {f g : ℂ → ℂ} {x : ℝ} (h : f =O[𝓝[
5353
(fun y : ℝ ↦ f y) =O[𝓝[≠] x] (fun y : ℝ ↦ g y) :=
5454
h.comp_tendsto <| continuous_ofReal.continuousWithinAt.tendsto_nhdsWithin fun _ _ ↦ by simp_all
5555

56+
lemma isBigO_re_sub_re {z : ℂ} : (fun (w : ℂ) ↦ w.re - z.re) =O[𝓝 z] fun w ↦ w - z :=
57+
Asymptotics.isBigO_of_le _ fun w ↦ abs_re_le_norm (w - z)
58+
59+
lemma isBigO_im_sub_im {z : ℂ} : (fun (w : ℂ) ↦ w.im - z.im) =O[𝓝 z] fun w ↦ w - z :=
60+
Asymptotics.isBigO_of_le _ fun w ↦ abs_im_le_norm (w - z)
61+
5662
end Complex
5763

5864
section Int

‎Mathlib/Analysis/Complex/Convex.lean‎

Lines changed: 20 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -62,12 +62,30 @@ theorem convex_halfSpace_im_gt : Convex ℝ { c : ℂ | r < c.im } :=
6262
convex_halfSpace_gt (.mk add_im smul_im) _
6363
theorem convex_halfSpace_im_ge : Convex ℝ { c : ℂ | r ≤ c.im } :=
6464
convex_halfSpace_ge (.mk add_im smul_im) _
65-
lemma Complex.isConnected_of_upperHalfPlane {r} {s : Set ℂ} (hs₁ : {z | r < z.im} ⊆ s)
65+
66+
namespace Complex
67+
68+
lemma isConnected_of_upperHalfPlane {r} {s : Set ℂ} (hs₁ : {z | r < z.im} ⊆ s)
6669
(hs₂ : s ⊆ {z | r ≤ z.im}) : IsConnected s := by
6770
refine .subset_closure ?_ hs₁ (by simpa only [closure_setOf_lt_im] using hs₂)
6871
exact (convex_halfSpace_im_gt r).isConnected ⟨(r + 1) * I, by simp⟩
6972

70-
lemma Complex.isConnected_of_lowerHalfPlane {r} {s : Set ℂ} (hs₁ : {z | z.im < r} ⊆ s)
73+
lemma isConnected_of_lowerHalfPlane {r} {s : Set ℂ} (hs₁ : {z | z.im < r} ⊆ s)
7174
(hs₂ : s ⊆ {z | z.im ≤ r}) : IsConnected s := by
7275
refine .subset_closure ?_ hs₁ (by simpa only [closure_setOf_im_lt] using hs₂)
7376
exact (convex_halfSpace_im_lt r).isConnected ⟨(r - 1) * I, by simp⟩
77+
78+
lemma rectangle_eq_convexHull (z w : ℂ) :
79+
Rectangle z w = convexHull ℝ {z, z.re + w.im * I, w.re + z.im * I, w} := by
80+
simp_rw [Rectangle, ← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm,
81+
← preimage_equivRealProd_prod, insert_prod, singleton_prod, image_pair, insert_union,
82+
← insert_eq, preimage_equiv_eq_image_symm, image_insert_eq, image_singleton,
83+
equivRealProd_symm_apply, re_add_im]
84+
85+
/-- If opposite corners of a rectangle are contained in a convex set, the whole rectangle is. -/
86+
lemma Convex.rectangle_subset {U : Set ℂ} (U_convex : Convex ℝ U) {z w : ℂ} (hz : z ∈ U)
87+
(hw : w ∈ U) (hzw : (z.re + w.im * I) ∈ U) (hwz : (w.re + z.im * I) ∈ U) :
88+
Rectangle z w ⊆ U := by
89+
simpa only [rectangle_eq_convexHull] using convexHull_min (by grind) U_convex
90+
91+
end Complex

‎Mathlib/Analysis/Complex/HasPrimitives.lean‎

Lines changed: 272 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,272 @@
1+
/-
2+
Copyright (c) 2024 Ian Jauslin and Alex Kontorovich. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Ian Jauslin, Alex Kontorovich, Oliver Nash
5+
-/
6+
import Mathlib.Analysis.Complex.CauchyIntegral
7+
import Mathlib.Analysis.Complex.Convex
8+
9+
/-!
10+
# Primitives of Holomorphic Functions
11+
12+
In this file, we give conditions under which holomorphic functions have primitives. The main goal
13+
is to prove that holomorphic functions on simply connected domains have primitives. As a first step,
14+
we prove that holomorphic functions on disks have primitives. The approach is based on Morera's
15+
theorem, that a continuous function (on a disk) whose integral round a rectangle vanishes on all
16+
rectangles contained in the disk has a primitive. (Coupled with the fact that holomorphic functions
17+
satisfy this property.) To prove Morera's theorem, we first define the `Complex.wedgeIntegral`,
18+
which is the integral of a function over a "wedge" (a horizontal segment followed by a vertical
19+
segment in the disk), and compute its derivative.
20+
21+
## Main results
22+
23+
* `Complex.IsConservativeOn.isExactOn_ball`: **Morera's Theorem**: On a disk, a continuous function
24+
whose integrals on rectangles vanish, has primitives.
25+
* `DifferentiableOn.isExactOn_ball`: On a disk, a holomorphic function has primitives.
26+
27+
TODO: Extend to holomorphic functions on simply connected domains.
28+
-/
29+
30+
noncomputable section
31+
32+
open Complex MeasureTheory Metric Set Topology
33+
open scoped Interval
34+
35+
namespace Complex
36+
37+
section AuxiliaryLemmata
38+
39+
variable {c z : ℂ} {r x y : ℝ}
40+
41+
private lemma re_add_im_mul_mem_ball (hz : z ∈ ball c r) :
42+
z.re + c.im * I ∈ ball c r := by
43+
suffices dist (z.re + c.im * I) c ≤ dist z c from lt_of_le_of_lt this hz
44+
rw [dist_eq_re_im, dist_eq_re_im, Real.le_sqrt (by positivity) (by positivity),
45+
Real.sq_sqrt (by positivity)]
46+
simp [sq_nonneg _]
47+
48+
private lemma mem_ball_re_aux (hx : x ∈ Ioo (z.re - (r - dist z c)) (z.re + (r - dist z c))) :
49+
x + z.im * I ∈ ball c r := by
50+
set r₁ := r - dist z c
51+
set s := Ioo (z.re - r₁) (z.re + r₁)
52+
have s_ball₁ : s ×ℂ {z.im} ⊆ ball z r₁ := by
53+
rintro y ⟨yRe : y.re ∈ s, yIm : y.im = z.im⟩
54+
rw [mem_ball, dist_eq_re_im, yIm, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs]
55+
grind [abs_lt]
56+
suffices s ×ℂ {z.im} ⊆ ball c r from this <| by simp [mem_reProdIm, hx]
57+
exact s_ball₁.trans <| ball_subset_ball' <| by simp [r₁]
58+
59+
private lemma mem_closedBall_aux (z_in_ball : z ∈ closedBall c r) (y_in_I : y ∈ Ι c.im z.im) :
60+
z.re + y * I ∈ closedBall c r := by
61+
refine le_trans ?_ (mem_closedBall.mp z_in_ball)
62+
rw [dist_eq_re_im, dist_eq_re_im, Real.le_sqrt (by positivity) (by positivity),
63+
Real.sq_sqrt (by positivity)]
64+
suffices (y - c.im) ^ 2 ≤ (z.im - c.im) ^ 2 by simpa
65+
cases mem_uIoc.mp y_in_I <;> nlinarith
66+
67+
private lemma mem_ball_of_map_re_aux {a₁ a₂ b : ℝ} (ha₁ : a₁ + b * I ∈ ball c r)
68+
(ha₂ : a₂ + b * I ∈ ball c r) : (fun (x : ℝ) ↦ x + b * I) '' [[a₁, a₂]] ⊆ ball c r := by
69+
convert Convex.rectangle_subset (convex_ball c r) ha₁ ha₂ ?_ ?_ using 1 <;>
70+
simp [horizontalSegment_eq a₁ a₂ b, ha₁, ha₂, Rectangle]
71+
72+
private lemma mem_ball_of_map_im_aux₁ {a b₁ b₂ : ℝ} (hb₁ : a + b₁ * I ∈ ball c r)
73+
(hb₂ : a + b₂ * I ∈ ball c r) : (fun (y : ℝ) ↦ a + y * I) '' [[b₁, b₂]] ⊆ ball c r := by
74+
convert Convex.rectangle_subset (convex_ball c r) hb₁ hb₂ ?_ ?_ using 1 <;>
75+
simp [verticalSegment_eq a b₁ b₂, hb₁, hb₂, Rectangle]
76+
77+
private lemma mem_ball_of_map_im_aux₂ {w : ℂ} (hw : w ∈ ball z (r - dist z c)) :
78+
(fun (y : ℝ) ↦ w.re + y * I) '' [[z.im, w.im]] ⊆ ball c r := by
79+
apply mem_ball_of_map_im_aux₁ <;>
80+
apply mem_of_subset_of_mem (ball_subset_ball' (by simp) : ball z (r - dist z c) ⊆ ball c r)
81+
· exact re_add_im_mul_mem_ball hw
82+
· simpa using hw
83+
84+
end AuxiliaryLemmata
85+
86+
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
87+
88+
/-- The `(z, w)`-wedge-integral of `f`, is the integral of `f` over two sides of the rectangle
89+
determined by `z` and `w`. -/
90+
def wedgeIntegral (z w : ℂ) (f : ℂ → E) : E :=
91+
(∫ x : ℝ in z.re..w.re, f (x + z.im * I)) + I • (∫ y : ℝ in z.im..w.im, f (w.re + y * I))
92+
93+
lemma wedgeIntegral_add_wedgeIntegral_eq (z w : ℂ) (f : ℂ → E) :
94+
wedgeIntegral z w f + wedgeIntegral w z f =
95+
(∫ x : ℝ in z.re..w.re, f (x + z.im * I)) -
96+
(∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
97+
I • (∫ y : ℝ in z.im..w.im, f (w.re + y * I)) -
98+
I • (∫ y : ℝ in z.im..w.im, f (z.re + y * I)) := by
99+
simp only [wedgeIntegral, intervalIntegral.integral_symm z.re w.re,
100+
intervalIntegral.integral_symm z.im w.im, smul_neg]
101+
abel
102+
103+
/-- A function `f` `IsConservativeOn` in `U` if, for any rectangle contained in `U`
104+
the integral of `f` over the rectangle is zero. -/
105+
def IsConservativeOn (f : ℂ → E) (U : Set ℂ) : Prop :=
106+
∀ z w, Rectangle z w ⊆ U → wedgeIntegral z w f = - wedgeIntegral w z f
107+
108+
/-- A function `f` `IsExactOn` in `U` if it is the complex derivative of a function on `U`.
109+
110+
In complex variable theory, this is also referred to as "having a primitive". -/
111+
def IsExactOn (f : ℂ → E) (U : Set ℂ) : Prop :=
112+
∃ g, ∀ z ∈ U, HasDerivAt g (f z) z
113+
114+
variable {c : ℂ} {r : ℝ} {f : ℂ → E}
115+
116+
theorem _root_.DifferentiableOn.isConservativeOn {U : Set ℂ} (hf : DifferentiableOn ℂ f U) :
117+
IsConservativeOn f U := by
118+
rintro z w hzw
119+
rw [← add_eq_zero_iff_eq_neg, wedgeIntegral_add_wedgeIntegral_eq]
120+
exact integral_boundary_rect_eq_zero_of_differentiableOn f z w <| hf.mono hzw
121+
122+
variable [CompleteSpace E]
123+
124+
lemma IsExactOn.isConservativeOn_of_isOpen {U : Set ℂ} (hU : IsOpen U) (hf : IsExactOn f U) :
125+
IsConservativeOn f U := by
126+
obtain ⟨g, hg⟩ := hf
127+
have hg' : DifferentiableOn ℂ g U := fun z hz ↦ (hg z hz).differentiableAt.differentiableWithinAt
128+
apply DifferentiableOn.isConservativeOn
129+
exact (differentiableOn_congr <| fun z hz ↦ (hg z hz).deriv).mp <| hg'.deriv hU
130+
131+
section ContinuousOnBall
132+
133+
variable (f_cont : ContinuousOn f (ball c r)) {z : ℂ} (hz : z ∈ ball c r)
134+
include f_cont hz
135+
136+
omit [CompleteSpace E] in
137+
/-- If a function `f` `IsConservativeOn` on a disk of center `c`, then for points `z` in this disk,
138+
the wedge integral from `c` to `z` is additive under a detour through a nearby point `w`. -/
139+
lemma IsConservativeOn.eventually_nhds_wedgeIntegral_sub_wedgeIntegral
140+
(hf : IsConservativeOn f (ball c r)) :
141+
∀ᶠ w in 𝓝 z, wedgeIntegral c w f - wedgeIntegral c z f = wedgeIntegral z w f := by
142+
refine eventually_nhds_iff_ball.mpr ⟨r - dist z c, by simpa using hz, fun w w_in_z_ball ↦ ?_⟩
143+
set I₁ := ∫ x in c.re..w.re, f (x + c.im * I)
144+
set I₂ := I • ∫ y in c.im..w.im, f (w.re + y * I)
145+
set I₃ := ∫ x in c.re..z.re, f (x + c.im * I)
146+
set I₄ := I • ∫ y in c.im..z.im, f (z.re + y * I)
147+
set I₅ := ∫ x in z.re..w.re, f (x + z.im * I)
148+
set I₆ := I • ∫ y in z.im..w.im, f (w.re + y * I)
149+
set I₇ := ∫ x in z.re..w.re, f (x + c.im * I)
150+
set I₈ := I • ∫ y in c.im..z.im, f (w.re + y * I)
151+
have z_ball : ball z (r - dist z c) ⊆ ball c r := ball_subset_ball' (by simp)
152+
have w_mem : w ∈ ball c r := mem_of_subset_of_mem z_ball w_in_z_ball
153+
have integrableHoriz (a₁ a₂ b : ℝ) (ha₁ : a₁ + b * I ∈ ball c r) (ha₂ : a₂ + b * I ∈ ball c r) :
154+
IntervalIntegrable (fun x ↦ f (x + b * I)) volume a₁ a₂ :=
155+
((f_cont.mono (mem_ball_of_map_re_aux ha₁ ha₂)).comp (by fun_prop)
156+
(mapsTo_image _ _)).intervalIntegrable
157+
have integrableVert (a b₁ b₂ : ℝ) (hb₁ : a + b₁ * I ∈ ball c r) (hb₂ : a + b₂ * I ∈ ball c r) :
158+
IntervalIntegrable (fun y ↦ f (a + y * I)) volume b₁ b₂ :=
159+
((f_cont.mono (mem_ball_of_map_im_aux₁ hb₁ hb₂)).comp (by fun_prop)
160+
(mapsTo_image _ _)).intervalIntegrable
161+
have hI₁ : I₁ = I₃ + I₇ := by
162+
rw [intervalIntegral.integral_add_adjacent_intervals] <;> apply integrableHoriz
163+
· exact re_add_im_mul_mem_ball <| mem_ball_self (pos_of_mem_ball hz)
164+
· exact re_add_im_mul_mem_ball hz
165+
· exact re_add_im_mul_mem_ball hz
166+
· exact re_add_im_mul_mem_ball w_mem
167+
have hI₂ : I₂ = I₈ + I₆ := by
168+
rw [← smul_add, intervalIntegral.integral_add_adjacent_intervals] <;> apply integrableVert
169+
· exact re_add_im_mul_mem_ball w_mem
170+
· exact mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)
171+
· exact mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)
172+
· simpa using w_mem
173+
have hI₀ : I₇ - I₅ + I₈ - I₄ = 0 := by
174+
have wzInBall : w.re + z.im * I ∈ ball c r :=
175+
mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)
176+
have wcInBall : w.re + c.im * I ∈ ball c r := re_add_im_mul_mem_ball w_mem
177+
have hU : Rectangle (z.re + c.im * I) (w.re + z.im * I) ⊆ ball c r :=
178+
(convex_ball c r).rectangle_subset (re_add_im_mul_mem_ball hz) wzInBall
179+
(by simpa using hz) (by simpa using wcInBall)
180+
simpa [← add_eq_zero_iff_eq_neg, wedgeIntegral_add_wedgeIntegral_eq] using
181+
hf (z.re + c.im * I) (w.re + z.im * I) hU
182+
grind [wedgeIntegral]
183+
184+
/- The horizontal integral of `f` from `z` to `z.re + w.im * I` is equal to `(w - z).re * f z`
185+
up to `o(w - z)`, as `w` tends to `z`. -/
186+
private lemma hasDerivAt_wedgeIntegral_re_aux :
187+
(fun w ↦ (∫ x in z.re..w.re, f (x + z.im * I)) - (w - z).re • f z) =o[𝓝 z] fun w ↦ w - z := by
188+
suffices (fun x ↦ (∫ t in z.re..x, f (t + z.im * I)) - (x - z.re) • f z) =o[𝓝 z.re]
189+
fun x ↦ x - z.re from
190+
this.comp_tendsto (continuous_re.tendsto z) |>.trans_isBigO isBigO_re_sub_re
191+
let r₁ := r - dist z c
192+
have r₁_pos : 0 < r₁ := by simpa only [mem_ball, sub_pos, r₁] using hz
193+
let s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
194+
have zRe_mem_s : z.re ∈ s := by simp [s, r₁_pos]
195+
have f_contOn : ContinuousOn (fun (x : ℝ) ↦ f (x + z.im * I)) s :=
196+
f_cont.comp ((continuous_add_right _).comp continuous_ofReal).continuousOn <|
197+
fun _ ↦ mem_ball_re_aux
198+
have int1 : IntervalIntegrable (fun (x : ℝ) ↦ f (x + z.im * I)) volume z.re z.re :=
199+
ContinuousOn.intervalIntegrable <| f_contOn.mono <| by simpa
200+
have int2 : StronglyMeasurableAtFilter (fun (x : ℝ) ↦ f (x + z.im * I)) (𝓝 z.re) :=
201+
f_contOn.stronglyMeasurableAtFilter isOpen_Ioo _ zRe_mem_s
202+
have int3 : ContinuousAt (fun (x : ℝ) ↦ f (x + z.im * I)) z.re :=
203+
isOpen_Ioo.continuousOn_iff.mp f_contOn zRe_mem_s
204+
simpa [HasDerivAt, HasDerivAtFilter, hasFDerivAtFilter_iff_isLittleO] using
205+
intervalIntegral.integral_hasDerivAt_right int1 int2 int3
206+
207+
/-- The vertical integral of `f` from `w.re + z.im * I` to `w` is equal to `(w - z).im * f z`
208+
up to `o(w - z)`, as `w` tends to `z`. -/
209+
private lemma hasDerivAt_wedgeIntegral_im_aux :
210+
(fun w ↦ (∫ y in z.im..w.im, f (w.re + y * I)) - (w - z).im • f z) =o[𝓝 z] fun w ↦ w - z := by
211+
suffices (fun w ↦ ∫ y in z.im..w.im, f (w.re + y * I) - f z) =o[𝓝 z] fun w ↦ w - z by
212+
calc
213+
_ = fun w ↦ (∫ y in z.im..w.im, f (w.re + y * I)) - (∫ _ in z.im..w.im, f z) := by simp
214+
_ =ᶠ[𝓝 z] fun w ↦ ∫ y in z.im..w.im, f (w.re + y * I) - f z := ?_
215+
_ =o[𝓝 z] fun w ↦ w - z := this
216+
refine eventually_nhds_iff_ball.mpr ⟨r - dist z c, by simpa using hz, fun w hw ↦ ?_⟩
217+
exact (intervalIntegral.integral_sub
218+
((f_cont.mono (mem_ball_of_map_im_aux₂ hw)).comp (by fun_prop)
219+
(mapsTo_image _ _)).intervalIntegrable intervalIntegrable_const).symm
220+
have : (fun w ↦ f w - f z) =o[𝓝 z] fun _ ↦ (1 : ℝ) := by
221+
rw [Asymptotics.isLittleO_one_iff, tendsto_sub_nhds_zero_iff]
222+
exact f_cont.continuousAt <| _root_.mem_nhds_iff.mpr ⟨ball c r, le_refl _, isOpen_ball, hz⟩
223+
rw [Asymptotics.IsLittleO] at this ⊢
224+
intro ε ε_pos
225+
replace := this ε_pos
226+
simp only [Asymptotics.isBigOWith_iff, norm_one, mul_one] at this ⊢
227+
replace this : ∀ᶠ w in 𝓝 z, ∀ y ∈ Ι z.im w.im, ‖f (w.re + y * I) - f z‖ ≤ ε := by
228+
rw [Metric.nhds_basis_closedBall.eventually_iff] at this ⊢
229+
obtain ⟨i, i_pos, hi⟩ := this
230+
exact ⟨i, i_pos, fun w w_in_ball y y_in_I ↦ hi (mem_closedBall_aux w_in_ball y_in_I)⟩
231+
filter_upwards [this] with w hw
232+
calc
233+
_ ≤ ε * ‖w.im - z.im‖ := intervalIntegral.norm_integral_le_of_norm_le_const hw
234+
_ = ε * ‖(w - z).im‖ := by simp
235+
_ ≤ ε * ‖w - z‖ := (mul_le_mul_iff_of_pos_left ε_pos).mpr (abs_im_le_norm _)
236+
237+
/-- The `wedgeIntegral` has derivative at `z` equal to `f z`. -/
238+
theorem IsConservativeOn.hasDerivAt_wedgeIntegral (h : IsConservativeOn f (ball c r)) :
239+
HasDerivAt (fun w ↦ wedgeIntegral c w f) (f z) z := by
240+
rw [hasDerivAt_iff_isLittleO]
241+
calc
242+
_ =ᶠ[𝓝 z] (fun w ↦ wedgeIntegral z w f - (w - z) • f z) := ?_
243+
_ = (fun w ↦ (∫ x in z.re..w.re, f (x + z.im * I)) - (w - z).re • f z)
244+
+ I • (fun w ↦ (∫ y in z.im..w.im, f (w.re + y * I)) - (w - z).im • f z) := ?_
245+
_ =o[𝓝 z] fun w ↦ w - z := (hasDerivAt_wedgeIntegral_re_aux f_cont hz).add
246+
((hasDerivAt_wedgeIntegral_im_aux f_cont hz).const_smul_left I)
247+
· exact (h.eventually_nhds_wedgeIntegral_sub_wedgeIntegral f_cont hz).mono <| by simp
248+
ext w
249+
set I₁ := ∫ x in z.re..w.re, f (x + z.im * I)
250+
set I₂ := ∫ y in z.im..w.im, f (w.re + y * I)
251+
calc
252+
_ = I₁ + I • I₂ - ((w - z).re + (w - z).im * I) • f z := by congr; rw [re_add_im]
253+
_ = I₁ + I • I₂ - ((w.re - z.re : ℂ) + (w.im - z.im) * I) • f z := by simp
254+
_ = I₁ - (w.re - z.re : ℂ) • f z + I • (I₂ - (w.im - z.im : ℂ) • f z) := ?_
255+
· rw [add_smul, smul_sub, smul_smul, mul_comm I]; abel
256+
· congr <;> simp
257+
258+
end ContinuousOnBall
259+
260+
/-- **Morera's theorem for a disk** On a disk, a continuous function whose integrals on rectangles
261+
vanish, has primitives. -/
262+
theorem IsConservativeOn.isExactOn_ball (hf' : ContinuousOn f (ball c r))
263+
(hf : IsConservativeOn f (ball c r)) :
264+
IsExactOn f (ball c r) :=
265+
⟨fun z ↦ wedgeIntegral c z f, fun _ ↦ hf.hasDerivAt_wedgeIntegral hf'⟩
266+
267+
/-- **Morera's theorem for a disk** On a disk, a holomorphic function has primitives. -/
268+
theorem _root_.DifferentiableOn.isExactOn_ball (hf : DifferentiableOn ℂ f (ball c r)) :
269+
IsExactOn f (ball c r) :=
270+
hf.isConservativeOn.isExactOn_ball hf.continuousOn
271+
272+
end Complex

0 commit comments

Comments
 (0)