Planar circulation and curl

The oriented real plane is ℂ, with positive basis (1, Complex.I). The circulation of a field with components P, Q uses the real 1-form P dx + Q dy; its curl is ∂x Q - ∂y P. The raw-curve integrand agrees with Mathlib's curveIntegral on a Path, including for paths whose derivative is defined only almost everywhere.

These conventions fix the signs for planar Green identities.

noncomputable def TauCeti.Green.oneForm (P Q : ℂ → ℝ) (z : ℂ) : ℂ →L[ℝ] ℝ

The real 1-form P dx + Q dy on the positively oriented complex plane.

Equations

• TauCeti.Green.oneForm P Q z = P z • Complex.reCLM + Q z • Complex.imCLM

@[simp]

theorem TauCeti.Green.oneForm_apply (P Q : ℂ → ℝ) (z v : ℂ) : (oneForm P Q z) v = P z * v.re + Q z * v.im

Evaluation of the planar 1-form in real coordinates.

theorem TauCeti.Green.oneForm_eq_clm (P Q : ℂ → ℝ) : oneForm P Q = fun (z : ℂ) => P z • Complex.reCLM + Q z • Complex.imCLM

The planar 1-form as a field of continuous linear maps in the coordinate projections.

theorem Continuous.oneForm {P Q : ℂ → ℝ} (hP : Continuous P) (hQ : Continuous Q) : Continuous (TauCeti.Green.oneForm P Q)

A continuous planar field gives a continuous field of real linear 1-forms.

theorem TauCeti.Green.exists_bound_oneForm {P Q : ℂ → ℝ} (hP : Continuous P) (hQ : Continuous Q) (hcP : HasCompactSupport P) (hcQ : HasCompactSupport Q) : ∃ (C : ℝ), ∀ (z : ℂ), ‖oneForm P Q z‖ ≤ C

A continuous compactly supported planar field has uniformly bounded 1-form operator norm.

noncomputable def TauCeti.Green.circulationFun (P Q : ℂ → ℝ) (γ : ℝ → ℂ) (t : ℝ) : ℝ

The integrand of circulation along a raw curve on an oriented real interval.

Equations

• TauCeti.Green.circulationFun P Q γ t = P (γ t) * (deriv γ t).re + Q (γ t) * (deriv γ t).im

theorem TauCeti.Green.circulationFun_eq_oneForm (P Q : ℂ → ℝ) (γ : ℝ → ℂ) (t : ℝ) : circulationFun P Q γ t = (oneForm P Q (γ t)) (deriv γ t)

The raw circulation integrand is the planar 1-form applied to the velocity.

noncomputable def TauCeti.Green.curl (P Q : ℂ → ℝ) (z : ℂ) : ℝ

Curl in the positive real basis (1, Complex.I). These are real Fréchet derivatives, so this definition is used for differentiable fields; directional Green identities state their slice derivatives separately.

Equations

• TauCeti.Green.curl P Q z = (fderiv ℝ Q z) 1 - (fderiv ℝ P z) Complex.I

theorem ContDiff.continuous_curl {P Q : ℂ → ℝ} (hP : ContDiff ℝ 1 P) (hQ : ContDiff ℝ 1 Q) : Continuous (TauCeti.Green.curl P Q)

Globally real C¹ fields have continuous curl.

theorem HasCompactSupport.curl {P Q : ℂ → ℝ} (hcP : HasCompactSupport P) (hcQ : HasCompactSupport Q) : HasCompactSupport (TauCeti.Green.curl P Q)

Compact support of the field implies compact support of its curl.

theorem TauCeti.Green.curl_eq_deriv_slices {P Q : ℂ → ℝ} {z : ℂ} (hP : DifferentiableAt ℝ P z) (hQ : DifferentiableAt ℝ Q z) : curl P Q z = deriv (fun (x : ℝ) => Q { re := x, im := z.im }) z.re - deriv (fun (y : ℝ) => P { re := z.re, im := y }) z.im

For differentiable fields the curl agrees with the difference of the directional slice derivatives used in the graph-cell identities.

theorem TauCeti.Green.curveIntegral_oneForm_eq {p q : ℂ} (γ : Path p q) (P Q : ℂ → ℝ) : curveIntegral (oneForm P Q) γ = ∫ (t : ℝ) in 0..1, circulationFun P Q (⇑γ.extend) t

Mathlib's curve integral is the circulation integral in real coordinates.

theorem TauCeti.Green.intervalIntegrable_circulationFun_segment {p q : ℂ} {P Q : ℂ → ℝ} (hP : ContinuousOn P (segment ℝ p q)) (hQ : ContinuousOn Q (segment ℝ p q)) : IntervalIntegrable (circulationFun P Q ⇑(Path.segment p q).extend) MeasureTheory.volume 0 1

Continuous coefficients are genuinely Bochner integrable along a straight segment.