Circulation of raw polygonal curves #
Affine interpolation on each closed subdivision interval identifies the actual raw circulation with the curve integral of its straight segment. Summing over the finite subdivision gives the integer-chain integral of the successive vertices, without replacing the raw curve or assuming any equality of integrals as input.
theorem
TauCeti.Green.integral_circulationFun_eq_curveIntegral_segment
{γ : ℝ → ℂ}
{a b : ℝ}
{p q : ℂ}
(hab : a < b)
(hγ : ∀ t ∈ Set.Icc a b, γ t = p + ((t - a) / (b - a)) • (q - p))
(P Q : ℂ → ℝ)
:
A raw curve that agrees with affine interpolation on a nondegenerate interval has the same circulation as the corresponding existing straight path.
theorem
TauCeti.Green.integral_circulationFun_eq_polygon
{γ : ℝ → ℂ}
{a b : ℝ}
{N : ℕ}
{s : Fin (N + 1) → ℝ}
(hs : StrictMono s)
(ha : s 0 = a)
(hb : s (Fin.last N) = b)
(hsegments :
∀ (i : Fin N),
∀ t ∈ Set.Icc (s i.castSucc) (s i.succ),
γ t = γ (s i.castSucc) + ((t - s i.castSucc) / (s i.succ - s i.castSucc)) • (γ (s i.succ) - γ (s i.castSucc)))
{P Q : ℂ → ℝ}
(hP : ContinuousOn P (γ '' Set.uIcc a b))
(hQ : ContinuousOn Q (γ '' Set.uIcc a b))
:
∫ (t : ℝ) in a..b, circulationFun P Q γ t = (Finsupp.linearCombination ℤ fun (η : Arc) => curveIntegral (oneForm P Q) η.snd.snd) (BoundaryChain.polygon (γ ∘ s))
The circulation of an absolutely continuous raw polygonal curve is the actual finite integer-chain sum of its segment curve integrals. The partition may be nonuniform.