Integral of a 1-form along a path

In this file we define the integral of a 1-form along a path indexed by [0, 1] and prove basic properties of this operation.

The integral ∫ᶜ x in γ, ω x is defined as $\int_0^1 \omega(\gamma(t))(\gamma'(t))$. More precisely, we use

• Path.extend γ t instead of γ t, because both derivatives and intervalIntegral expect globally defined functions;
• derivWithin γ.extend (Set.Icc 0 1) t, not deriv γ.extend t, for the derivative, so that it takes meaningful values at t = 0 and t = 1, even though this does not affect the integral.

The argument ω : E → E →L[𝕜] F is a 𝕜-linear 1-form on E taking values in F, where 𝕜 is ℝ or ℂ. The definition does not depend on 𝕜, see curveIntegral_restrictScalars and nearby lemmas. However, the fact that 𝕜 = ℝ is not hardcoded allows us to avoid inserting ContinuousLinearMap.restrictScalars here and there.

Main definitions

• curveIntegral ω γ, notation ∫ᶜ x in γ, ω x, is the integral of a 1-form ω along a path γ.
• CurveIntegrable ω γ is the predicate saying that the above integral makes sense.

Main results

We prove that curveIntegral well behaves with respect to

• operations on Paths, see curveIntegral_refl, curveIntegral_symm, curveIntegral_trans etc;
• algebraic operations on 1-forms, see curveIntegral_add etc.

We also show that the derivative of fun b ↦ ∫ᶜ x in Path.segment a b, ω x has derivative ω a at b = a. We provide 2 versions of this result: one for derivative (HasFDerivWithinAt) within a convex set and one for HasFDerivAt.

Implementation notes

Naming

In literature, the integral of a function or a 1-form along a path is called “line integral”, “path integral”, “curve integral”, or “curvelinear integral”.

We use the name “curve integral” instead of other names for the following reasons:

• for many people whose mother tongue is not English, “line integral” sounds like an integral along a straight line;

• we reserve the name "path integral" for Feynmann-style integrals over the space of paths.

Usage of ContinuousLinearMaps for 1-forms

Similarly to the way fderiv uses continuous linear maps while higher order derivatives use continuous multilinear maps, this file uses E → E →L[𝕜] F instead of continuous alternating maps for 1-forms.

Differentiability assumptions

The definitions in this file make sense if the path is a piecewise $C^1$ curve. Poincaré lemma (formalization WIP, see #24019) implies that for a closed 1-form on an open set U, the integral depends on the homotopy class of the path only, thus we can define the integral along a continuous path or an element of the fundamental groupoid of U.

Usage of an extra field

The definitions in this file deal with 𝕜-linear 1-forms. This allows us to avoid using ContinuousLinearMap.restrictScalars in HasFDerivWithinAt.curveIntegral_segment_source and a future formalization of Poincaré lemma.

@[irreducible]

noncomputable def curveIntegralFun {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} (ω : E → E →L[𝕜] F) (γ : Path a b) (t : ℝ) : F

The function t ↦ ω (γ t) (γ' t) which appears in the definition of a curve integral.

This definition is used to factor out common parts of lemmas about CurveIntegrable and curveIntegral.

Equations

• curveIntegralFun ω γ t = (ω (γ.extend t)) (derivWithin (⇑γ.extend) unitInterval t)

theorem curveIntegralFun_def' {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} (ω : E → E →L[𝕜] F) (γ : Path a b) (t : ℝ) : curveIntegralFun ω γ t = (ω (γ.extend t)) (derivWithin (⇑γ.extend) unitInterval t)

def CurveIntegrable {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} (ω : E → E →L[𝕜] F) (γ : Path a b) : Prop

A 1-form ω is curve integrable along a path γ, if the function curveIntegralFun ω γ t = ω (γ t) (γ' t) is integrable on [0, 1].

The actual definition uses Path.extend γ, because both interval integrals and derivatives expect globally defined functions.

Equations

• CurveIntegrable ω γ = IntervalIntegrable (curveIntegralFun ω γ) MeasureTheory.volume 0 1

theorem curveIntegral_def' {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} (ω : E → E →L[𝕜] F) (γ : Path a b) : curveIntegral ω γ = ∫ (t : ℝ) in 0..1, curveIntegralFun ω γ t

@[irreducible]

noncomputable def curveIntegral {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} (ω : E → E →L[𝕜] F) (γ : Path a b) : F

Integral of a 1-form ω : E → E →L[𝕜] F along a path γ, defined as $\int_0^1 \omega(\gamma(t))(\gamma'(t))$.

The actual definition uses curveIntegralFun which uses Path.extend γ and derivWithin (Path.extend γ) (Set.Icc 0 1) t, because calculus-related definitions in Mathlib expect globally defined functions as arguments.

Equations

• curveIntegral ω γ = ∫ (t : ℝ) in 0..1, curveIntegralFun ω γ t

def «term∫ᶜ_In_,_» : Lean.ParserDescr

Integral of a 1-form ω : E → E →L[𝕜] F along a path γ, defined as $\int_0^1 \omega(\gamma(t))(\gamma'(t))$.

The actual definition uses curveIntegralFun which uses Path.extend γ and derivWithin (Path.extend γ) (Set.Icc 0 1) t, because calculus-related definitions in Mathlib expect globally defined functions as arguments.

Equations

• One or more equations did not get rendered due to their size.

theorem curveIntegral_of_not_completeSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} (h : ¬CompleteSpace F) (ω : E → E →L[𝕜] F) (γ : Path a b) : ∫ᶜ (x : E) in γ, ω x = 0

curve integral is defined using Bochner integral, thus it is defined as zero whenever the codomain is not a complete space.

theorem curveIntegralFun_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} [NormedSpace ℝ E] (ω : E → E →L[𝕜] F) (γ : Path a b) (t : ℝ) : curveIntegralFun ω γ t = (ω (γ.extend t)) (derivWithin (⇑γ.extend) unitInterval t)

theorem curveIntegral_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} [NormedSpace ℝ F] (ω : E → E →L[𝕜] F) (γ : Path a b) : curveIntegral ω γ = ∫ (t : ℝ) in 0..1, curveIntegralFun ω γ t

theorem curveIntegral_eq_intervalIntegral_deriv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} [NormedSpace ℝ E] [NormedSpace ℝ F] (ω : E → E →L[𝕜] F) (γ : Path a b) : ∫ᶜ (x : E) in γ, ω x = ∫ (t : ℝ) in 0..1, (ω (γ.extend t)) (deriv (⇑γ.extend) t)

Operations on paths

@[simp]

theorem curveIntegralFun_refl {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (ω : E → E →L[𝕜] F) (a : E) : curveIntegralFun ω (Path.refl a) = 0

@[simp]

theorem curveIntegral_refl {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (ω : E → E →L[𝕜] F) (a : E) : ∫ᶜ (x : E) in Path.refl a, ω x = 0

@[simp]

theorem CurveIntegrable.refl {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (ω : E → E →L[𝕜] F) (a : E) : CurveIntegrable ω (Path.refl a)

@[simp]

theorem curveIntegralFun_cast {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b c d : E} (ω : E → E →L[𝕜] F) (γ : Path a b) (hc : c = a) (hd : d = b) : curveIntegralFun ω (γ.cast hc hd) = curveIntegralFun ω γ

@[simp]

theorem curveIntegral_cast {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b c d : E} (ω : E → E →L[𝕜] F) (γ : Path a b) (hc : c = a) (hd : d = b) : ∫ᶜ (x : E) in γ.cast hc hd, ω x = ∫ᶜ (x : E) in γ, ω x

@[simp]

theorem curveIntegrable_cast_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b c d : E} {ω : E → E →L[𝕜] F} {γ : Path a b} (hc : c = a) (hd : d = b) : CurveIntegrable ω (γ.cast hc hd) ↔ CurveIntegrable ω γ

theorem CurveIntegrable.cast {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b c d : E} {ω : E → E →L[𝕜] F} {γ : Path a b} (hc : c = a) (hd : d = b) : CurveIntegrable ω γ → CurveIntegrable ω (γ.cast hc hd)

Alias of the reverse direction of curveIntegrable_cast_iff.

theorem curveIntegralFun_symm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} (ω : E → E →L[𝕜] F) (γ : Path a b) (t : ℝ) : curveIntegralFun ω γ.symm t = -curveIntegralFun ω γ (1 - t)

@[simp]

theorem curveIntegralFun_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} (ω : E → E →L[𝕜] F) (γ : Path a b) : curveIntegralFun ω γ.symm = fun (x : ℝ) => (-curveIntegralFun ω γ) (1 - x)

theorem CurveIntegrable.symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} (h : CurveIntegrable ω γ) : CurveIntegrable ω γ.symm

@[simp]

theorem curveIntegrable_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} : CurveIntegrable ω γ.symm ↔ CurveIntegrable ω γ

@[simp]

theorem curveIntegral_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} (ω : E → E →L[𝕜] F) (γ : Path a b) : ∫ᶜ (x : E) in γ.symm, ω x = -∫ᶜ (x : E) in γ, ω x

theorem curveIntegralFun_trans_of_lt_half {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b c : E} {t : ℝ} (ω : E → E →L[𝕜] F) (γab : Path a b) (γbc : Path b c) (ht : t < 1 / 2) : curveIntegralFun ω (γab.trans γbc) t = 2 • curveIntegralFun ω γab (2 * t)

theorem curveIntegralFun_trans_aeeq_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b c : E} (ω : E → E →L[𝕜] F) (γab : Path a b) (γbc : Path b c) : curveIntegralFun ω (γab.trans γbc) =ᵐ[MeasureTheory.volume.restrict (Set.uIoc 0 (1 / 2))] fun (t : ℝ) => 2 • curveIntegralFun ω γab (2 * t)

theorem curveIntegralFun_trans_of_half_lt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b c : E} {t : ℝ} (ω : E → E →L[𝕜] F) (γab : Path a b) (γbc : Path b c) (ht₀ : 1 / 2 < t) : curveIntegralFun ω (γab.trans γbc) t = 2 • curveIntegralFun ω γbc (2 * t - 1)

theorem curveIntegralFun_trans_aeeq_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b c : E} (ω : E → E →L[𝕜] F) (γab : Path a b) (γbc : Path b c) : curveIntegralFun ω (γab.trans γbc) =ᵐ[MeasureTheory.volume.restrict (Set.uIoc (1 / 2) 1)] fun (t : ℝ) => 2 • curveIntegralFun ω γbc (2 * t - 1)

theorem CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b c : E} {ω : E → E →L[𝕜] F} {γab : Path a b} (h : CurveIntegrable ω γab) (γbc : Path b c) : IntervalIntegrable (curveIntegralFun ω (γab.trans γbc)) MeasureTheory.volume 0 (1 / 2)

theorem CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b c : E} {ω : E → E →L[𝕜] F} {γbc : Path b c} (γab : Path a b) (h : CurveIntegrable ω γbc) : IntervalIntegrable (curveIntegralFun ω (γab.trans γbc)) MeasureTheory.volume (1 / 2) 1

theorem CurveIntegrable.trans {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b c : E} {ω : E → E →L[𝕜] F} {γab : Path a b} {γbc : Path b c} (h₁ : CurveIntegrable ω γab) (h₂ : CurveIntegrable ω γbc) : CurveIntegrable ω (γab.trans γbc)

theorem curveIntegral_trans {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b c : E} {ω : E → E →L[𝕜] F} {γab : Path a b} {γbc : Path b c} (h₁ : CurveIntegrable ω γab) (h₂ : CurveIntegrable ω γbc) : ∫ᶜ (x : E) in γab.trans γbc, ω x = ∫ᶜ (x : E) in γab, ω x + ∫ᶜ (x : E) in γbc, ω x

theorem curveIntegralFun_segment {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ E] (ω : E → E →L[𝕜] F) (a b : E) {t : ℝ} (ht : t ∈ unitInterval) : curveIntegralFun ω (Path.segment a b) t = (ω ((AffineMap.lineMap a b) t)) (b - a)

theorem curveIntegrable_segment {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} [NormedSpace ℝ E] : CurveIntegrable ω (Path.segment a b) ↔ IntervalIntegrable (fun (t : ℝ) => (ω ((AffineMap.lineMap a b) t)) (b - a)) MeasureTheory.volume 0 1

theorem curveIntegral_segment {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ E] [NormedSpace ℝ F] (ω : E → E →L[𝕜] F) (a b : E) : ∫ᶜ (x : E) in Path.segment a b, ω x = ∫ (t : ℝ) in 0..1, (ω ((AffineMap.lineMap a b) t)) (b - a)

@[simp]

theorem curveIntegral_segment_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ E] [CompleteSpace F] (ω : E →L[𝕜] F) (a b : E) : ∫ᶜ (x : E) in Path.segment a b, ω = ω (b - a)

theorem norm_curveIntegral_segment_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} [NormedSpace ℝ E] {C : ℝ} (h : ∀ z ∈ segment ℝ a b, ‖ω z‖ ≤ C) : ‖∫ᶜ (x : E) in Path.segment a b, ω x‖ ≤ C * ‖b - a‖

If ‖ω z‖ ≤ C at all points of the segment [a -[ℝ] b], then the curve integral ∫ᶜ x in .segment a b, ω x has norm at most C * ‖b - a‖.

theorem ContinuousOn.curveIntegrable_of_contDiffOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} [NormedSpace ℝ E] {s : Set E} (hω : ContinuousOn ω s) (hγ : ContDiffOn ℝ 1 (⇑γ.extend) unitInterval) (hγs : ∀ (t : ↑unitInterval), γ t ∈ s) : CurveIntegrable ω γ

If a 1-form ω is continuous on a set s, then it is curve integrable along any $C^1$ path in this set.

Algebraic operations on the 1-form

@[simp]

theorem curveIntegralFun_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b} : curveIntegralFun (ω₁ + ω₂) γ = curveIntegralFun ω₁ γ + curveIntegralFun ω₂ γ

theorem CurveIntegrable.add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b} (h₁ : CurveIntegrable ω₁ γ) (h₂ : CurveIntegrable ω₂ γ) : CurveIntegrable (ω₁ + ω₂) γ

theorem curveIntegral_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b} (h₁ : CurveIntegrable ω₁ γ) (h₂ : CurveIntegrable ω₂ γ) : curveIntegral (ω₁ + ω₂) γ = ∫ᶜ (x : E) in γ, ω₁ x + ∫ᶜ (x : E) in γ, ω₂ x

theorem curveIntegral_fun_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b} (h₁ : CurveIntegrable ω₁ γ) (h₂ : CurveIntegrable ω₂ γ) : ∫ᶜ (x : E) in γ, (ω₁ x + ω₂ x) = ∫ᶜ (x : E) in γ, ω₁ x + ∫ᶜ (x : E) in γ, ω₂ x

@[simp]

theorem curveIntegralFun_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {γ : Path a b} : curveIntegralFun 0 γ = 0

@[simp]

theorem curveIntegralFun_fun_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {γ : Path a b} : curveIntegralFun (fun (x : E) => 0) γ = 0

theorem CurveIntegrable.zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {γ : Path a b} : CurveIntegrable 0 γ

theorem CurveIntegrable.fun_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {γ : Path a b} : CurveIntegrable (fun (x : E) => 0) γ

@[simp]

theorem curveIntegral_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {γ : Path a b} : curveIntegral 0 γ = 0

@[simp]

theorem curveIntegral_fun_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {γ : Path a b} : ∫ᶜ (x : E) in γ, 0 = 0

@[simp]

theorem curveIntegralFun_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} : curveIntegralFun (-ω) γ = -curveIntegralFun ω γ

theorem CurveIntegrable.neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} (h : CurveIntegrable ω γ) : CurveIntegrable (-ω) γ

theorem CurveIntegrable.fun_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} (h : CurveIntegrable ω γ) : CurveIntegrable (fun (x : E) => -ω x) γ

@[simp]

theorem curveIntegrable_neg_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} : CurveIntegrable (-ω) γ ↔ CurveIntegrable ω γ

@[simp]

theorem curveIntegrable_fun_neg_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} : CurveIntegrable (fun (x : E) => -ω x) γ ↔ CurveIntegrable ω γ

@[simp]

theorem curveIntegral_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} : curveIntegral (-ω) γ = -∫ᶜ (x : E) in γ, ω x

@[simp]

theorem curveIntegral_fun_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} : ∫ᶜ (x : E) in γ, -ω x = -∫ᶜ (x : E) in γ, ω x

@[simp]

theorem curveIntegralFun_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b} : curveIntegralFun (ω₁ - ω₂) γ = curveIntegralFun ω₁ γ - curveIntegralFun ω₂ γ

theorem CurveIntegrable.sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b} (h₁ : CurveIntegrable ω₁ γ) (h₂ : CurveIntegrable ω₂ γ) : CurveIntegrable (ω₁ - ω₂) γ

theorem curveIntegral_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b} (h₁ : CurveIntegrable ω₁ γ) (h₂ : CurveIntegrable ω₂ γ) : curveIntegral (ω₁ - ω₂) γ = ∫ᶜ (x : E) in γ, ω₁ x - ∫ᶜ (x : E) in γ, ω₂ x

theorem curveIntegral_fun_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b} (h₁ : CurveIntegrable ω₁ γ) (h₂ : CurveIntegrable ω₂ γ) : ∫ᶜ (x : E) in γ, (ω₁ x - ω₂ x) = ∫ᶜ (x : E) in γ, ω₁ x - ∫ᶜ (x : E) in γ, ω₂ x

@[simp]

theorem curveIntegralFun_restrictScalars {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} {𝕝 : Type u_4} [RCLike 𝕝] [NormedSpace 𝕝 F] [NormedSpace 𝕝 E] [LinearMap.CompatibleSMul E F 𝕝 𝕜] : curveIntegralFun (fun (t : E) => ContinuousLinearMap.restrictScalars 𝕝 (ω t)) γ = curveIntegralFun ω γ

@[simp]

theorem curveIntegrable_restrictScalars_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} {𝕝 : Type u_4} [RCLike 𝕝] [NormedSpace 𝕝 F] [NormedSpace 𝕝 E] [LinearMap.CompatibleSMul E F 𝕝 𝕜] : CurveIntegrable (fun (t : E) => ContinuousLinearMap.restrictScalars 𝕝 (ω t)) γ ↔ CurveIntegrable ω γ

@[simp]

theorem curveIntegral_restrictScalars {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} {𝕝 : Type u_4} [RCLike 𝕝] [NormedSpace 𝕝 F] [NormedSpace 𝕝 E] [LinearMap.CompatibleSMul E F 𝕝 𝕜] : ∫ᶜ (x : E) in γ, ContinuousLinearMap.restrictScalars 𝕝 (ω x) = ∫ᶜ (x : E) in γ, ω x

@[simp]

theorem curveIntegralFun_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} {𝕝 : Type u_4} [RCLike 𝕝] [NormedSpace 𝕝 F] [SMulCommClass 𝕜 𝕝 F] {c : 𝕝} : curveIntegralFun (c • ω) γ = c • curveIntegralFun ω γ

theorem CurveIntegrable.smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} {𝕝 : Type u_4} [RCLike 𝕝] [NormedSpace 𝕝 F] [SMulCommClass 𝕜 𝕝 F] {c : 𝕝} (h : CurveIntegrable ω γ) : CurveIntegrable (c • ω) γ

@[simp]

theorem curveIntegrable_smul_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} {𝕝 : Type u_4} [RCLike 𝕝] [NormedSpace 𝕝 F] [SMulCommClass 𝕜 𝕝 F] {c : 𝕝} : CurveIntegrable (c • ω) γ ↔ c = 0 ∨ CurveIntegrable ω γ

@[simp]

theorem curveIntegral_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} {𝕝 : Type u_4} [RCLike 𝕝] [NormedSpace 𝕝 F] [SMulCommClass 𝕜 𝕝 F] {c : 𝕝} : curveIntegral (c • ω) γ = c • curveIntegral ω γ

@[simp]

theorem curveIntegral_fun_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F} {γ : Path a b} {𝕝 : Type u_4} [RCLike 𝕝] [NormedSpace 𝕝 F] [SMulCommClass 𝕜 𝕝 F] {c : 𝕝} : ∫ᶜ (x : E) in γ, c • ω x = c • ∫ᶜ (x : E) in γ, ω x

Derivative of the curve integral w.r.t. the right endpoint

In this section we prove that the integral of ω along [a -[ℝ] b], as a function of b, has derivative ω a at b = a. We provide several versions of this theorem, for HasFDerivWithinAt and HasFDerivAt, as well as for continuity near a point and for continuity on the whole set or space.

Note that we take the derivative at the left endpoint of the segment. Similar facts about the derivative at a different point are true provided that ω is a closed 1-form (formalization WIP, see #24019).

theorem HasFDerivWithinAt.curveIntegral_segment_source' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {a : E} {s : Set E} {ω : E → E →L[𝕜] F} (hs : Convex ℝ s) (hω : ∀ᶠ (x : E) in nhdsWithin a s, ContinuousWithinAt ω s x) (ha : a ∈ s) : HasFDerivWithinAt (fun (x : E) => ∫ᶜ (x : E) in Path.segment a x, ω x) (ω a) s a

The integral of ω along [a -[ℝ] b], as a function of b, has derivative ω a at b = a. This is a HasFDerivWithinAt version assuming that ω is continuous within a convex set s in a neighborhood of a within s.

theorem HasFDerivWithinAt.curveIntegral_segment_source {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {a : E} {s : Set E} {ω : E → E →L[𝕜] F} (hs : Convex ℝ s) (hω : ContinuousOn ω s) (ha : a ∈ s) : HasFDerivWithinAt (fun (x : E) => ∫ᶜ (x : E) in Path.segment a x, ω x) (ω a) s a

The integral of ω along [a -[ℝ] b], as a function of b, has derivative ω a at b = a. This is a HasFDerivWithinAt version assuming that ω is continuous on s.

theorem HasFDerivAt.curveIntegral_segment_source' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {a : E} {ω : E → E →L[𝕜] F} (hω : ∀ᶠ (z : E) in nhds a, ContinuousAt ω z) : HasFDerivAt (fun (x : E) => ∫ᶜ (x : E) in Path.segment a x, ω x) (ω a) a

The integral of ω along [a -[ℝ] b], as a function of b, has derivative ω a at b = a. This is a HasFDerivAt version assuming that ω is continuous in a neighborhood of a.

theorem HasFDerivAt.curveIntegral_segment_source {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {a : E} {ω : E → E →L[𝕜] F} (hω : Continuous ω) : HasFDerivAt (fun (x : E) => ∫ᶜ (x : E) in Path.segment a x, ω x) (ω a) a

The integral of ω along [a -[ℝ] b], as a function of b, has derivative ω a at b = a. This is a HasFDerivAt version assuming that ω is continuous on the whole space.