Passage to the limit in the two Green integrals

Uniform convergence of absolutely continuous curves and L¹ convergence of derivatives preserve circulation of compactly supported continuous fields. L¹ convergence of the winding weights preserves the curl area integral for globally C¹, compactly supported fields. Both integrals are integrable; index vanishing identifies the whole-plane area integral with its restriction to the field domain.

theorem AbsolutelyContinuousOnInterval.tendsto_integral_circulationFun {γn : ℕ → ℝ → ℂ} {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hγn : ∀ (n : ℕ), AbsolutelyContinuousOnInterval (γn n) a b) (hab : a ≤ b) {P Q : ℂ → ℝ} (hP : Continuous P) (hQ : Continuous Q) (hcP : HasCompactSupport P) (hcQ : HasCompactSupport Q) (hconv : TendstoUniformlyOn γn γ Filter.atTop (Set.Icc a b)) (hdconv : Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ) in a..b, ‖deriv (γn n) t - deriv γ t‖) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ) in a..b, TauCeti.Green.circulationFun P Q (γn n) t) Filter.atTop (nhds (∫ (t : ℝ) in a..b, TauCeti.Green.circulationFun P Q γ t))

Uniform convergence of AC curves and derivative L¹ convergence preserve the actual circulation integral of compactly supported continuous planar fields.

theorem AbsolutelyContinuousOnInterval.integrable_windingWeight_mul_curl {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b) {P Q : ℂ → ℝ} (hP : ContDiff ℝ 1 P) (hQ : ContDiff ℝ 1 Q) : MeasureTheory.Integrable (fun (z : ℂ) => TauCeti.Green.windingWeight γ a b z * TauCeti.Green.curl P Q z) MeasureTheory.volume

The winding-weighted curl of globally C¹ fields is integrable for every closed AC curve.

theorem AbsolutelyContinuousOnInterval.tendsto_integral_windingWeight_mul_curl {γn : ℕ → ℝ → ℂ} {γ : ℝ → ℂ} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hγn : ∀ (n : ℕ), AbsolutelyContinuousOnInterval (γn n) a b) (hclosed : γ a = γ b) (hclosedn : ∀ (n : ℕ), γn n a = γn n b) {P Q : ℂ → ℝ} (hP : ContDiff ℝ 1 P) (hQ : ContDiff ℝ 1 Q) (hcP : HasCompactSupport P) (hcQ : HasCompactSupport Q) (hwconv : Filter.Tendsto (fun (n : ℕ) => ∫ (z : ℂ), |TauCeti.Green.windingWeight (γn n) a b z - TauCeti.Green.windingWeight γ a b z|) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : ℂ), TauCeti.Green.windingWeight (γn n) a b z * TauCeti.Green.curl P Q z) Filter.atTop (nhds (∫ (z : ℂ), TauCeti.Green.windingWeight γ a b z * TauCeti.Green.curl P Q z))

Actual winding-weighted curl integrals converge under L¹ convergence of the weights. There is no uniform bound on the winding numbers.

theorem AbsolutelyContinuousOnInterval.tendsto_setIntegral_windingWeight_mul_curl {γn : ℕ → ℝ → ℂ} {γ : ℝ → ℂ} {a b : ℝ} {U : Set ℂ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hγn : ∀ (n : ℕ), AbsolutelyContinuousOnInterval (γn n) a b) (hclosed : γ a = γ b) (hclosedn : ∀ (n : ℕ), γn n a = γn n b) {P Q : ℂ → ℝ} (hP : ContDiff ℝ 1 P) (hQ : ContDiff ℝ 1 Q) (hcP : HasCompactSupport P) (hcQ : HasCompactSupport Q) (hwconv : Filter.Tendsto (fun (n : ℕ) => ∫ (z : ℂ), |TauCeti.Green.windingWeight (γn n) a b z - TauCeti.Green.windingWeight γ a b z|) Filter.atTop (nhds 0)) (hindex : ∀ z ∉ U, TauCeti.Contour.windingNumber γ a b z = 0) (hindexn : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ z ∉ U, TauCeti.Contour.windingNumber (γn n) a b z = 0) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : ℂ) in U, TauCeti.Green.windingWeight (γn n) a b z * TauCeti.Green.curl P Q z) Filter.atTop (nhds (∫ (z : ℂ) in U, TauCeti.Green.windingWeight γ a b z * TauCeti.Green.curl P Q z))

The weighted curl integrals over an index-vanishing domain converge when the winding weights converge in L¹. The approximating indices need vanish outside the domain only eventually.

theorem AbsolutelyContinuousOnInterval.integral_circulationFun_eq_setIntegral {γn : ℕ → ℝ → ℂ} {γ : ℝ → ℂ} {a b : ℝ} {U : Set ℂ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hγn : ∀ (n : ℕ), AbsolutelyContinuousOnInterval (γn n) a b) (hab : a ≤ b) (hclosed : γ a = γ b) (hclosedn : ∀ (n : ℕ), γn n a = γn n b) {P Q : ℂ → ℝ} (hP : ContDiff ℝ 1 P) (hQ : ContDiff ℝ 1 Q) (hcP : HasCompactSupport P) (hcQ : HasCompactSupport Q) (hconv : TendstoUniformlyOn γn γ Filter.atTop (Set.Icc a b)) (hdconv : Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ) in a..b, ‖deriv (γn n) t - deriv γ t‖) Filter.atTop (nhds 0)) (hwconv : Filter.Tendsto (fun (n : ℕ) => ∫ (z : ℂ), |TauCeti.Green.windingWeight (γn n) a b z - TauCeti.Green.windingWeight γ a b z|) Filter.atTop (nhds 0)) (hindex : ∀ z ∉ U, TauCeti.Contour.windingNumber γ a b z = 0) (hindexn : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ z ∉ U, TauCeti.Contour.windingNumber (γn n) a b z = 0) (hgreen : ∀ᶠ (n : ℕ) in Filter.atTop, ∫ (t : ℝ) in a..b, TauCeti.Green.circulationFun P Q (γn n) t = ∫ (z : ℂ) in U, TauCeti.Green.windingWeight (γn n) a b z * TauCeti.Green.curl P Q z) : ∫ (t : ℝ) in a..b, TauCeti.Green.circulationFun P Q γ t = ∫ (z : ℂ) in U, TauCeti.Green.windingWeight γ a b z * TauCeti.Green.curl P Q z

Passage to the limit in both actual Green integrals. Any approximating Green identities valid eventually pass to the closed AC limit, using uniform, derivative L¹, and weight L¹ convergence. In particular this applies to the endpoint-preserving polygonal approximations.