Circulation along absolutely continuous curves #
Continuous planar fields have integrable circulation along an absolutely continuous curve.
The orientation is that of the existing intervalIntegral.
These results supply boundary integrability for Green's theorem along absolutely continuous curves.
theorem
AbsolutelyContinuousOnInterval.intervalIntegrable_circulationFun
{γ : ℝ → ℂ}
{a b : ℝ}
{P Q : ℂ → ℝ}
(hγ : AbsolutelyContinuousOnInterval γ a b)
(hP : ContinuousOn P (γ '' Set.uIcc a b))
(hQ : ContinuousOn Q (γ '' Set.uIcc a b))
:
A continuous planar field has interval-integrable circulation along an absolutely continuous curve.
theorem
AbsolutelyContinuousOnInterval.curveIntegrable_oneForm
{p q : ℂ}
{γ : Path p q}
{P Q : ℂ → ℝ}
(hγ : AbsolutelyContinuousOnInterval (⇑γ.extend) 0 1)
(hP : ContinuousOn P (⇑γ.extend '' Set.Icc 0 1))
(hQ : ContinuousOn Q (⇑γ.extend '' Set.Icc 0 1))
:
CurveIntegrable (TauCeti.Green.oneForm P Q) γ
A continuous planar 1-form is curve integrable along a path whose extension is absolutely
continuous on [0, 1].
theorem
AbsolutelyContinuousOnInterval.integral_circulationFun_comp_lineMap
{γ : ℝ → ℂ}
{a b : ℝ}
{P Q : ℂ → ℝ}
(hγ : AbsolutelyContinuousOnInterval γ a b)
(hP : ContinuousOn P (γ '' Set.uIcc a b))
(hQ : ContinuousOn Q (γ '' Set.uIcc a b))
:
∫ (t : ℝ) in 0..1, TauCeti.Green.circulationFun P Q (γ ∘ ⇑(AffineMap.lineMap a b)) t = ∫ (t : ℝ) in a..b, TauCeti.Green.circulationFun P Q γ t
Affine normalization to the unit interval preserves circulation for fields continuous on the curve trace, with reversed and constant intervals allowed.