7.5. Path.LineIntegral🔗

Jacobians.Path.LineIntegral — source

pathSpeed

Complex speed of γ at t, expressed in the chart around γ t.

noncomputable def pathSpeed {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (γ : ℝ → X) (t : ℝ)
    : ℂ

lineIntegral

Line integral of a holomorphic 1-form α along a smooth path γ.

∫_γ α := ∫ t in 0..1, α(γ t)(γ'(t)), where γ'(t) is computed via pathSpeed.

noncomputable def lineIntegral {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (α : HolomorphicOneForms X)
    (γ : ℝ → X) : ℂ

pathSpeed_const

pathSpeed (fun _ => P) t = 0: the tangent of a constant curve is zero. Chart pullback of a constant map is constant in ℂ, whose fderiv is zero.

theorem pathSpeed_const {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (P : X) (t : ℝ) :
    pathSpeed (fun _ : ℝ => P) t = 0

reverse

Time-reversal of a path: reverse γ t := γ (1 - t).

def reverse {X : Type*} (γ : ℝ → X) : ℝ → X

reverse_apply

@[simp] theorem reverse_apply {X : Type*} (γ : ℝ → X) (t : ℝ) :
    reverse γ t = γ (1 - t)

pathSpeed_reverse

pathSpeed under reversal: sign flip + reparametrization. Requires chart-pullback (chartAt ℂ (γ(1-t))).toFun ∘ γ to be differentiable at 1 - t (which holds for smooth γ at points in the chart source).

theorem pathSpeed_reverse {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (γ : ℝ → X) (t : ℝ)
    (hdiff : DifferentiableAt ℝ
      ((chartAt (H := ℂ) (γ (1 - t))).toFun ∘ γ) (1 - t)) :
    pathSpeed (reverse γ) t = -pathSpeed γ (1 - t)

lineIntegral_reverse

Line integral reverses sign under path reversal, under differentiability of the chart pullback on [0, 1].

theorem lineIntegral_reverse {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (α : HolomorphicOneForms X)
    (γ : ℝ → X)
    (hdiff : ∀ t ∈ Set.uIcc (0 : ℝ) 1,
      DifferentiableAt ℝ ((chartAt (H := ℂ) (γ (1 - t))).toFun ∘ γ) (1 - t)) :
    lineIntegral α (reverse γ) = -lineIntegral α γ

concat

Concatenation of paths: concat γ γ' t := γ(2t) on [0, 1/2], γ'(2t - 1) on [1/2, 1]. Typical basepoint-matching requirement γ 1 = γ' 0 is not enforced in the definition itself (it's needed for the concatenation to be continuous at t = 1/2, which is assumed when invoking lineIntegral_concat).

noncomputable def concat {X : Type*} (γ γ' : ℝ → X) : ℝ → X

concat_apply_left

theorem concat_apply_left {X : Type*} (γ γ' : ℝ → X) {t : ℝ} (ht : t ≤ 1/2) :
    concat γ γ' t = γ (2 * t)

concat_apply_right

theorem concat_apply_right {X : Type*} (γ γ' : ℝ → X) {t : ℝ} (ht : ¬ t ≤ 1/2) :
    concat γ γ' t = γ' (2 * t - 1)

pathSpeed_concat_left

pathSpeed of concat γ γ' on the strict left half: equals 2 * pathSpeed γ (2t) via chain rule on γ ∘ (2·).

theorem pathSpeed_concat_left {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (γ γ' : ℝ → X)
    (t : ℝ) (ht : t < 1/2)
    (hdiff : DifferentiableAt ℝ
      ((chartAt (H := ℂ) (γ (2 * t))).toFun ∘ γ) (2 * t)) :
    pathSpeed (concat γ γ') t = 2 * pathSpeed γ (2 * t)

pathSpeed_concat_right

pathSpeed of concat γ γ' on the strict right half: equals 2 * pathSpeed γ' (2t - 1) via chain rule on γ' ∘ (2·-1).

theorem pathSpeed_concat_right {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (γ γ' : ℝ → X)
    (t : ℝ) (ht : 1/2 < t)
    (hdiff : DifferentiableAt ℝ
      ((chartAt (H := ℂ) (γ' (2 * t - 1))).toFun ∘ γ') (2 * t - 1)) :
    pathSpeed (concat γ γ') t = 2 * pathSpeed γ' (2 * t - 1)

lineIntegral_concat

Concatenation identity for the line integral. lineIntegral α (concat γ γ') = lineIntegral α γ + lineIntegral α γ' assuming smoothness of each half in the chart pullback, the matching condition at t = 1/2, and integrability / pointwise identities expressing pathSpeed (concat) via the chain rule on each half.

theorem lineIntegral_concat {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (α : HolomorphicOneForms X)
    (γ γ' : ℝ → X)
    (hint_γ : IntervalIntegrable
      (fun u : ℝ => α.toFun (γ u) (pathSpeed γ u)) volume 0 1)
    (hint_γ' : IntervalIntegrable
      (fun u : ℝ => α.toFun (γ' u) (pathSpeed γ' u)) volume 0 1)
    (hint_concat_left : IntervalIntegrable
      (fun t : ℝ => α.toFun ((concat γ γ') t) (pathSpeed (concat γ γ') t))
      volume 0 (1/2))
    (hint_concat_right : IntervalIntegrable
      (fun t : ℝ => α.toFun ((concat γ γ') t) (pathSpeed (concat γ γ') t))
      volume (1/2) 1)
    (h_ae_left : ∀ᵐ t ∂(volume.restrict (Set.uIoc (0 : ℝ) (1/2))),
      α.toFun ((concat γ γ') t) (pathSpeed (concat γ γ') t) =
        (2 : ℂ) * α.toFun (γ (2 * t)) (pathSpeed γ (2 * t)))
    (h_ae_right : ∀ᵐ t ∂(volume.restrict (Set.uIoc ((1 : ℝ)/2) 1)),
      α.toFun ((concat γ γ') t) (pathSpeed (concat γ γ') t) =
        (2 : ℂ) * α.toFun (γ' (2 * t - 1)) (pathSpeed γ' (2 * t - 1))) :
    lineIntegral α (concat γ γ') = lineIntegral α γ + lineIntegral α γ'

pathSpeed_comp_eq_mfderiv

Core pointwise identity for the chain rule. Under differentiability of γ in the chart pullback at t (i.e., γ is C¹-smooth in chart coordinates at t) and smoothness of f, the tangent of f ∘ γ at t equals the manifold derivative mfderiv f applied to the tangent of γ at t.

The proof (complete below) is a three-step chart computation:

1. Chart-pullback chain rule: fderiv ℝ (chart\_Y ∘ f ∘ γ) t 1 = (fderiv ℝ f\_loc (chart\_X (γ t))) (pathSpeed γ t) via fderiv.comp on f_loc ∘ (chart_X ∘ γ) where f\_loc = chart\_Y ∘ f ∘ chart\_X.symm.

2. fderiv ℝ f_loc = (fderiv ℂ f_loc).restrictScalars ℝ via HasFDerivAt.restrictScalars.

3. fderiv ℂ f_loc (chart_X (γ t)) = mfderiv 𝓘(ℂ) 𝓘(ℂ) f (γ t) via MDifferentiableAt.mfderiv + writtenInExtChartAt unfolding.

theorem pathSpeed_comp_eq_mfderiv
    {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {Y : Type*} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y]
    [ConnectedSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (γ : ℝ → X) (t : ℝ)
    (hγ_cont : ContinuousAt γ t)
    (hγ_diff : DifferentiableAt ℝ ((chartAt (H := ℂ) (γ t)).toFun ∘ γ) t) :
    pathSpeed (f ∘ γ) t = mfderiv 𝓘(ℂ) 𝓘(ℂ) f (γ t) (pathSpeed γ t)

lineIntegral_pullback

Change of variables for the line integral (classical). Derived from pathSpeed_comp_eq_mfderiv + the definition of pullbackForm + intervalIntegral.integral_congr.

The hγ_diff hypothesis — γ is C¹-smooth in chart pullbacks for t ∈ [0, 1] — is the usual path-regularity required for line integrals to behave sensibly. For smooth closed loops (the use case in the period lattice), this holds automatically.

theorem lineIntegral_pullback {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {Y : Type*} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y]
    [ConnectedSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (α : HolomorphicOneForms Y) (γ : ℝ → X)
    (hγ_cont : Continuous γ)
    (hγ_diff : ∀ t ∈ Set.uIcc (0 : ℝ) 1,
      DifferentiableAt ℝ ((chartAt (H := ℂ) (γ t)).toFun ∘ γ) t) :
    lineIntegral α (f ∘ γ) = lineIntegral (pullbackForm f hf α) γ