English
If f: ℂ → E is continuous on a closed rectangle with corners z,w and satisfies differentiability assumptions, then the boundary integral equals the double integral of the partial derivatives of f along the rectangle.
Русский
Если f: ℂ → E непрерывна на замкнутом прямоугольнике с углами z,w и удовлетворяет предположениям дифференцируемости, то контурный интеграл по границе прямоугольника равен двойному интегралу по области внутри прямоугольника от частных производных f.
LaTeX
$$\\oint_{\\partial R} f(z) \\, dz = \\iint_R (i f_x(z) - f_y(z)) \\, dx dy$$
Lean4
/-- 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. -/
theorem integral_boundary_rect_of_hasFDerivAt_real_off_countable (f : ℂ → E) (f' : ℂ → ℂ →L[ℝ] E) (z w : ℂ) (s : Set ℂ)
(hs : s.Countable) (Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]]))
(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 :=
by
set e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
have he : ∀ x y : ℝ, ↑x + ↑y * I = e (x, y) := fun x y => (mk_eq_add_mul_I x y).symm
have he₁ : e (1, 0) = 1 := rfl; have he₂ : e (0, 1) = I := rfl
simp only [he] at *
set F : ℝ × ℝ → E := f ∘ e
set F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp (e : ℝ × ℝ →L[ℝ] ℂ)
have hF' : ∀ p : ℝ × ℝ, (-(I • F' p)) (1, 0) + F' p (0, 1) = -(I • f' (e p) 1 - f' (e p) I) :=
by
rintro ⟨x, y⟩
simp only [F', ContinuousLinearMap.neg_apply, ContinuousLinearMap.smul_apply, ContinuousLinearMap.comp_apply,
ContinuousLinearEquiv.coe_coe, he₁, he₂, neg_add_eq_sub, neg_sub]
set R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
set t : Set (ℝ × ℝ) := e ⁻¹' s
rw [uIcc_comm z.im] at Hc Hi; rw [min_comm z.im, max_comm z.im] at Hd
have hR : e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R := rfl
have htc : ContinuousOn F R := Hc.comp e.continuousOn hR.ge
have htd :
∀ p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max w.im z.im) \ t, HasFDerivAt F (F' p) p :=
fun p hp => (Hd (e p) hp).comp p e.hasFDerivAt
simp_rw [← intervalIntegral.integral_smul, intervalIntegral.integral_symm w.im z.im, ← intervalIntegral.integral_neg,
← hF']
refine
(integral2_divergence_prod_of_hasFDerivAt_off_countable (fun p => -(I • F p)) F (fun p => -(I • F' p)) F' z.re w.im
w.re z.im t (hs.preimage e.injective) (htc.const_smul _).neg htc (fun p hp => ((htd p hp).const_smul I).neg) htd
?_).symm
rw [←
(volume_preserving_equiv_real_prod.symm _).integrableOn_comp_preimage (MeasurableEquiv.measurableEmbedding _)] at Hi
simpa only [hF'] using Hi.neg
