Integration of one-forms along curves

The integral of a 1-form φ on a manifold M along a curve γ : ℝ → M over the oriented interval a..b is the interval integral of φ evaluated on the velocity of γ,

∫_γ φ = ∫ t in a..b, φ (γ t) (γ' t),

where the velocity TauCeti.Manifold.curveVelocity I γ t is the manifold derivative of γ on the unit vector. Equivalently, it is the interval integral of the pullback γ^* φ, a 1-form on ℝ, evaluated on the unit vector (TauCeti.pathIntegral_eq_integral_mpullback). For a real-valued form and a < b, it is the canonical oriented integral over [a, b] of the pullback of φ along γ (TauCeti.integralTopForm_mpullback_Icc_eq_pathIntegral).

Line integrals are the basic tool for detecting de Rham cohomology classes in degree one. The integral of the differential of a C¹ function is its endpoint difference (TauCeti.pathIntegral_mextDeriv_ofFunction, TauCeti.pathIntegral_mextDeriv), so exact forms integrate to zero around closed curves (TauCeti.pathIntegral_eq_zero_of_mem_exactForms). The integral is invariant under C¹ reparametrization (TauCeti.pathIntegral_comp), changes sign when the curve is reversed (TauCeti.pathIntegral_comp_sub_left), is additive under concatenation of curves (TauCeti.pathIntegral_curveConcat), is natural under pullback (TauCeti.pathIntegral_mpullback), and only depends on the values of the form along the curve (TauCeti.pathIntegral_congr) and on the curve away from the endpoints (TauCeti.pathIntegral_congr_of_eqOn_uIoo).

Main declarations

• TauCeti.pathIntegral φ γ a b: the integral of the 1-form φ along γ from a to b.
• TauCeti.continuousAt_apply_curveVelocity and TauCeti.IsSmoothForm.continuous_apply_curveVelocity: the integrand is continuous at every parameter where the curve is C¹ and the form is continuous at the point of the curve, so for a continuous form along a C¹ curve it is continuous.
• TauCeti.intervalIntegrable_apply_curveVelocity_of_contMDiffAt: the integrand is interval integrable on a..b as soon as, at every point of [[a, b]], the curve is C¹ and the form is continuous at the point of the curve. Since C¹ at a point is a condition on a neighbourhood of that point, the curve has to be C¹ near [[a, b]], while the form only has to be continuous at each point of the arc; both are arbitrary elsewhere.
• TauCeti.pathIntegral_mextDeriv_ofFunction and TauCeti.pathIntegral_mextDeriv: the fundamental theorem of calculus for line integrals.
• TauCeti.pathIntegral_eq_zero_of_mem_exactForms: exact 1-forms integrate to zero around closed C¹ curves.
• TauCeti.pathIntegral_comp: invariance under C¹ reparametrization.
• TauCeti.pathIntegral_curveConcat: additivity under concatenation of curves.
• TauCeti.exists_contMDiff_loop_pathIntegral_eq_sub: two smooth curves with common endpoints form a smooth loop whose line integral is the difference of theirs.
• TauCeti.pathIntegral_mpullback: naturality under pullback.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 11, section Line Integrals.

noncomputable def TauCeti.pathIntegral {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : RoughForm I M F 1) (γ : ℝ → M) (a b : ℝ) : F

The integral of a 1-form φ along a curve γ : ℝ → M over the oriented interval a..b: the interval integral of φ evaluated on the velocity of γ.

theorem TauCeti.pathIntegral_def {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : RoughForm I M F 1) (γ : ℝ → M) (a b : ℝ) : pathIntegral φ γ a b = ∫ (t : ℝ) in a..b, (φ (γ t)) fun (x : Fin 1) => Manifold.curveVelocity I γ t

The line integral is the interval integral of the form on the velocity of the curve.

theorem TauCeti.pathIntegral_eq_integral_mpullback {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : RoughForm I M F 1) (γ : ℝ → M) (a b : ℝ) : pathIntegral φ γ a b = ∫ (t : ℝ) in a..b, (mpullback (modelWithCornersSelf ℝ ℝ) I γ φ t) fun (x : Fin 1) => 1

The line integral is the interval integral of the pullback of the form to the parameter line, evaluated on the unit vector.

theorem TauCeti.pathIntegral_congr {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] {φ ψ : RoughForm I M F 1} {γ : ℝ → M} {a b : ℝ} (h : ∀ t ∈ Set.uIcc a b, φ (γ t) = ψ (γ t)) : pathIntegral φ γ a b = pathIntegral ψ γ a b

Line integrals only depend on the values of the form along the curve.

theorem TauCeti.pathIntegral_congr_of_eqOn_uIoo {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] {φ : RoughForm I M F 1} {γ γ' : ℝ → M} {a b : ℝ} (h : Set.EqOn γ γ' (Set.uIoo a b)) : pathIntegral φ γ a b = pathIntegral φ γ' a b

Line integrals along two curves agree when the curves agree on the open interval between the endpoints: the velocities then agree there, and the endpoints are a null set.

The interval of integration

@[simp]

theorem TauCeti.pathIntegral_same {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : RoughForm I M F 1) (γ : ℝ → M) (a : ℝ) : pathIntegral φ γ a a = 0

The line integral over a degenerate interval vanishes.

theorem TauCeti.pathIntegral_symm {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : RoughForm I M F 1) (γ : ℝ → M) (a b : ℝ) : pathIntegral φ γ b a = -pathIntegral φ γ a b

Reversing the interval of integration changes the sign of the line integral.

theorem TauCeti.pathIntegral_add_adjacent {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] {φ : RoughForm I M F 1} {γ : ℝ → M} {a b c : ℝ} (hab : IntervalIntegrable (fun (t : ℝ) => (φ (γ t)) fun (x : Fin 1) => Manifold.curveVelocity I γ t) MeasureTheory.volume a b) (hbc : IntervalIntegrable (fun (t : ℝ) => (φ (γ t)) fun (x : Fin 1) => Manifold.curveVelocity I γ t) MeasureTheory.volume b c) : pathIntegral φ γ a b + pathIntegral φ γ b c = pathIntegral φ γ a c

Line integrals over adjacent intervals add up, as soon as the form evaluated on the velocity is interval integrable on both intervals. For a continuous form along a C¹ curve this is TauCeti.IsSmoothForm.intervalIntegrable_apply_curveVelocity.

@[simp]

theorem TauCeti.pathIntegral_const_curve {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : RoughForm I M F 1) (x : M) (a b : ℝ) : pathIntegral φ (fun (x_1 : ℝ) => x) a b = 0

The line integral along a constant curve vanishes.

Linearity in the form

@[simp]

theorem TauCeti.pathIntegral_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] (γ : ℝ → M) (a b : ℝ) : pathIntegral 0 γ a b = 0

The line integral of the zero form vanishes.

@[simp]

theorem TauCeti.pathIntegral_neg {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : RoughForm I M F 1) (γ : ℝ → M) (a b : ℝ) : pathIntegral (-φ) γ a b = -pathIntegral φ γ a b

The line integral commutes with negation of the form.

@[simp]

theorem TauCeti.pathIntegral_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] (c : ℝ) (φ : RoughForm I M F 1) (γ : ℝ → M) (a b : ℝ) : pathIntegral (c • φ) γ a b = c • pathIntegral φ γ a b

The line integral commutes with scalar multiplication of the form.

theorem TauCeti.pathIntegral_add {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] {φ ψ : RoughForm I M F 1} {γ : ℝ → M} {a b : ℝ} (hφ : IntervalIntegrable (fun (t : ℝ) => (φ (γ t)) fun (x : Fin 1) => Manifold.curveVelocity I γ t) MeasureTheory.volume a b) (hψ : IntervalIntegrable (fun (t : ℝ) => (ψ (γ t)) fun (x : Fin 1) => Manifold.curveVelocity I γ t) MeasureTheory.volume a b) : pathIntegral (φ + ψ) γ a b = pathIntegral φ γ a b + pathIntegral ψ γ a b

The line integral of a sum of forms is the sum of the line integrals, as soon as both forms evaluated on the velocity are interval integrable. For continuous forms along a C¹ curve this is TauCeti.IsSmoothForm.intervalIntegrable_apply_curveVelocity.

theorem TauCeti.pathIntegral_sub {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] {φ ψ : RoughForm I M F 1} {γ : ℝ → M} {a b : ℝ} (hφ : IntervalIntegrable (fun (t : ℝ) => (φ (γ t)) fun (x : Fin 1) => Manifold.curveVelocity I γ t) MeasureTheory.volume a b) (hψ : IntervalIntegrable (fun (t : ℝ) => (ψ (γ t)) fun (x : Fin 1) => Manifold.curveVelocity I γ t) MeasureTheory.volume a b) : pathIntegral (φ - ψ) γ a b = pathIntegral φ γ a b - pathIntegral ψ γ a b

The line integral of a difference of forms is the difference of the line integrals, as soon as both forms evaluated on the velocity are interval integrable. For continuous forms along a C¹ curve this is TauCeti.IsSmoothForm.intervalIntegrable_apply_curveVelocity.

theorem TauCeti.continuousAt_apply_curveVelocity {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {φ : RoughForm I M F 1} {γ : ℝ → M} {t : ℝ} (hφ : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin 1]→L[ℝ] F))) 0 (fun (y : M) => ⟨y, φ y⟩) (γ t)) (hγ : ContMDiffAt (modelWithCornersSelf ℝ ℝ) I 1 γ t) : ContinuousAt (fun (u : ℝ) => (φ (γ u)) fun (x : Fin 1) => Manifold.curveVelocity I γ u) t

A 1-form evaluated on the velocity of a curve is continuous, as a function of the parameter, at every parameter where the curve is C¹ and the form is continuous at the point of the curve.

theorem TauCeti.IsSmoothForm.continuous_apply_curveVelocity {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {φ : RoughForm I M F 1} (hφ : IsSmoothForm I 0 φ) {γ : ℝ → M} (hγ : ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 γ) : Continuous fun (t : ℝ) => (φ (γ t)) fun (x : Fin 1) => Manifold.curveVelocity I γ t

Along a C¹ curve, a continuous 1-form evaluated on the velocity is a continuous function of the parameter.

theorem TauCeti.IsSmoothForm.intervalIntegrable_apply_curveVelocity {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {φ : RoughForm I M F 1} (hφ : IsSmoothForm I 0 φ) {γ : ℝ → M} (hγ : ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 γ) (a b : ℝ) : IntervalIntegrable (fun (t : ℝ) => (φ (γ t)) fun (x : Fin 1) => Manifold.curveVelocity I γ t) MeasureTheory.volume a b

A continuous 1-form is interval integrable along a C¹ curve.

theorem TauCeti.intervalIntegrable_apply_curveVelocity_of_contMDiffAt {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {φ : RoughForm I M F 1} {γ : ℝ → M} {a b : ℝ} (hφ : ∀ t ∈ Set.uIcc a b, ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin 1]→L[ℝ] F))) 0 (fun (y : M) => ⟨y, φ y⟩) (γ t)) (hγ : ∀ t ∈ Set.uIcc a b, ContMDiffAt (modelWithCornersSelf ℝ ℝ) I 1 γ t) : IntervalIntegrable (fun (t : ℝ) => (φ (γ t)) fun (x : Fin 1) => Manifold.curveVelocity I γ t) MeasureTheory.volume a b

A 1-form evaluated on the velocity of a curve is interval integrable on a..b when, at every point of [[a, b]], the curve is C¹ and the form is continuous at the point of the curve.

theorem TauCeti.pathIntegral_comp {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {φ : RoughForm I M F 1} (hφ : IsSmoothForm I 0 φ) {γ : ℝ → M} (hγ : ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 γ) {σ σ' : ℝ → ℝ} {a b : ℝ} (hσ : ∀ t ∈ Set.uIcc a b, HasDerivAt σ (σ' t) t) (hσ' : ContinuousOn σ' (Set.uIcc a b)) : pathIntegral φ (γ ∘ σ) a b = pathIntegral φ γ (σ a) (σ b)

Reparametrization invariance. The line integral of a continuous form along γ ∘ σ, for a C¹ change of parameter σ, is the line integral along γ between the image endpoints. The change of parameter need not be monotone.

theorem TauCeti.pathIntegral_comp_mul_add {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {φ : RoughForm I M F 1} (hφ : IsSmoothForm I 0 φ) {γ : ℝ → M} (hγ : ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 γ) (c d a b : ℝ) : pathIntegral φ (fun (t : ℝ) => γ (c * t + d)) a b = pathIntegral φ γ (c * a + d) (c * b + d)

The line integral along an affine reparametrization t ↦ γ (c * t + d) is the line integral along γ between the image endpoints.

theorem TauCeti.pathIntegral_comp_sub_left {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {φ : RoughForm I M F 1} (hφ : IsSmoothForm I 0 φ) {γ : ℝ → M} (hγ : ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 γ) (d a b : ℝ) : pathIntegral φ (fun (t : ℝ) => γ (d - t)) a b = -pathIntegral φ γ (d - b) (d - a)

The line integral along the reversed curve t ↦ γ (d - t) is the negative of the line integral along γ between the image endpoints.

theorem TauCeti.pathIntegral_curveConcat {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {φ : RoughForm I M F 1} (hφ : IsSmoothForm I 0 φ) {γ₁ γ₂ : ℝ → M} {y : M} (hγ₁ : ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 γ₁) (hγ₂ : ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 γ₂) (h₁ : ∀ (t : ℝ), 1 ≤ t → γ₁ t = y) (h₂ : ∀ t ≤ 0, γ₂ t = y) : pathIntegral φ (curveConcat γ₁ γ₂) 0 1 = pathIntegral φ γ₁ 0 1 + pathIntegral φ γ₂ 0 1

The line integral along a concatenation of two C¹ curves, constant near the junction point, is the sum of the line integrals.

theorem TauCeti.exists_contMDiff_loop_pathIntegral_eq_sub {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {φ : RoughForm I M F 1} (hφ : IsSmoothForm I 0 φ) {x₀ y : M} {γ γ' : ℝ → M} (hγ : ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑⊤) γ) (hγ₀ : ∀ t ≤ 0, γ t = x₀) (hγ₁ : ∀ (t : ℝ), 1 ≤ t → γ t = y) (hγ' : ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑⊤) γ') (hγ'₀ : ∀ t ≤ 0, γ' t = x₀) (hγ'₁ : ∀ (t : ℝ), 1 ≤ t → γ' t = y) : ∃ (ℓ : ℝ → M), ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑⊤) ℓ ∧ ℓ 0 = x₀ ∧ ℓ 1 = x₀ ∧ pathIntegral φ ℓ 0 1 = pathIntegral φ γ 0 1 - pathIntegral φ γ' 0 1

Two smooth curves from x₀ to y, constant on (-∞, 0] and on [1, ∞), form a smooth loop at x₀, the first followed by the reversed second. The line integral of a continuous form along this loop is the difference of the line integrals along the two curves.

Naturality

theorem TauCeti.pathIntegral_mpullback {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] {E' : Type u_5} {H' : Type u_6} {M' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} (φ : RoughForm I' M' F 1) {γ : ℝ → M} {a b : ℝ} (hf : ∀ t ∈ Set.uIcc a b, MDiffAt f (γ t)) (hγ : ∀ t ∈ Set.uIcc a b, MDiffAt γ t) : pathIntegral (mpullback I I' f φ) γ a b = pathIntegral φ (f ∘ γ) a b

Naturality of line integrals. The line integral of the pullback f^* φ along γ is the line integral of φ along f ∘ γ, as soon as f and γ are differentiable along the interval of integration.

theorem TauCeti.pathIntegral_apply_snd {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] {α : RoughForm I M F 1} {u : ℝ × ℝ → M} (hu : ContMDiff (modelWithCornersSelf ℝ (ℝ × ℝ)) I 1 u) (x a b : ℝ) : pathIntegral α (fun (t : ℝ) => u (x, t)) a b = ∫ (t : ℝ) in a..b, (mpullback (modelWithCornersSelf ℝ (ℝ × ℝ)) I u α (x, t)) fun (x : Fin 1) => (0, 1)

The line integral of a one-form along the curve t ↦ u (x, t) is the integral of the pullback of the form along u on the second coordinate vector.

theorem TauCeti.pathIntegral_apply_fst {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] {α : RoughForm I M F 1} {u : ℝ × ℝ → M} (hu : ContMDiff (modelWithCornersSelf ℝ (ℝ × ℝ)) I 1 u) (y a b : ℝ) : pathIntegral α (fun (s : ℝ) => u (s, y)) a b = ∫ (s : ℝ) in a..b, (mpullback (modelWithCornersSelf ℝ (ℝ × ℝ)) I u α (s, y)) fun (x : Fin 1) => (1, 0)

The line integral of a one-form along the curve s ↦ u (s, y) is the integral of the pullback of the form along u on the first coordinate vector.

The fundamental theorem of calculus

theorem TauCeti.pathIntegral_mextDeriv_ofFunction {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : M → F} (hf : ContMDiff I (modelWithCornersSelf ℝ F) 1 f) {γ : ℝ → M} (hγ : ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 γ) (a b : ℝ) : pathIntegral (mextDeriv (RoughForm.ofFunction I f)) γ a b = f (γ b) - f (γ a)

The fundamental theorem of calculus for line integrals. The line integral of the differential of a C¹ function along a C¹ curve is the difference of the values of the function at the endpoints.

theorem TauCeti.pathIntegral_mextDeriv {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [IsManifold I 1 M] {ψ : RoughForm I M F 0} (hψ : IsSmoothForm I 1 ψ) {γ : ℝ → M} (hγ : ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 γ) (a b : ℝ) : pathIntegral (mextDeriv ψ) γ a b = (ψ (γ b)) 0 - (ψ (γ a)) 0

The fundamental theorem of calculus for line integrals, for a C¹ form ψ of degree zero: the line integral of dψ along a C¹ curve is the difference of the values of ψ at the endpoints.

theorem TauCeti.pathIntegral_comp_eq_sub_of_mpullback_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [TopologicalSpace N] [ChartedSpace H' N] {φ : RoughForm I M F 1} {i : N → M} {f : N → F} (hi : MDiff i) (hf : ContMDiff J (modelWithCornersSelf ℝ F) 1 f) (hφ : mpullback J I i φ = mextDeriv (RoughForm.ofFunction J f)) {c : ℝ → N} (hc : ContMDiff (modelWithCornersSelf ℝ ℝ) J 1 c) (a b : ℝ) : pathIntegral φ (i ∘ c) a b = f (c b) - f (c a)

The fundamental theorem of calculus along a map with an exact pullback. If a differentiable map i : N → M pulls the one-form φ back to the differential of a C¹ function f on N, then the line integral of φ along i ∘ c, for a C¹ curve c in N, is the difference of the values of f at the endpoints of c. For instance, i may be an exact Lagrangian map and f its primitive.

theorem TauCeti.pathIntegral_eq_zero_of_mem_exactForms {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] {φ : SmoothForm I M ℝ 1} (hφ : φ ∈ exactForms I M 1) {γ : ℝ → M} (hγ : ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 γ) {a b : ℝ} (hab : γ a = γ b) : pathIntegral (↑φ) γ a b = 0

Exact smooth 1-forms integrate to zero around closed C¹ curves.

Comparison with oriented interval integration

theorem TauCeti.integralTopForm_mpullback_Icc_eq_pathIntegral {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {a b : ℝ} [Fact (a < b)] {φ : RoughForm I M ℝ 1} (hφ : IsSmoothForm I 0 φ) {γ : ℝ → M} (hγ : ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 γ) : integralTopForm (Manifold.Orientation.interval a b) (mpullback (modelWithCornersEuclideanHalfSpace 1) I (fun (t : ↑(Set.Icc a b)) => γ ↑t) φ) = pathIntegral φ γ a b

For a < b, the line integral of a continuous real 1-form along a C¹ curve is the canonical oriented integral over [a, b] of the pullback of the form along the curve.