Calculus with weak integrals: algebra, change of variables, fundamental theorem

For curves in a locally convex space F (Glöckner–Neeb, §1.1):

• Algebraic rules: weak integrals are additive in the integrand and in the interval, and commute with continuous linear maps.
• Change of variables: for a C^1 real function φ, ∫_a^b φ'(t) • γ(φ t) dt = ∫_{φ a}^{φ b} γ, as an equivalence of the two existence statements.
• Fundamental theorem of calculus, first part (Glöckner–Neeb, Prop. 1.1.5): if γ has a continuous derivative γ', then γ b - γ a is the weak integral of γ' over [a, b]; no completeness assumption on F is needed. The same holds for t ↦ df(x + t h)(h) when f is C^1 on a set containing the segment (the mean value theorem, Glöckner–Neeb, Prop. 1.2.6).
• Fundamental theorem of calculus, second part (Glöckner–Neeb, Prop. 1.1.12): if the weak integrals η s = ∫_a^s γ of a continuous curve exist, then η is differentiable with derivative γ. In a sequentially complete space they always exist.

Algebraic rules

theorem LCAnalysis.HasWeakIntegral.neg {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {γ : ℝ → F} {a b : ℝ} {y : F} (hy : HasWeakIntegral γ a b y) : HasWeakIntegral (fun (t : ℝ) => -γ t) a b (-y)

theorem LCAnalysis.HasWeakIntegral.add {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {γ η : ℝ → F} {a b : ℝ} {y z : F} (hγ : ContinuousOn γ (Set.uIcc a b)) (hη : ContinuousOn η (Set.uIcc a b)) (hy : HasWeakIntegral γ a b y) (hz : HasWeakIntegral η a b z) : HasWeakIntegral (fun (t : ℝ) => γ t + η t) a b (y + z)

theorem LCAnalysis.hasWeakIntegral_const {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (v : F) (a b : ℝ) : HasWeakIntegral (fun (x : ℝ) => v) a b ((b - a) • v)

theorem LCAnalysis.HasWeakIntegral.map {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {G : Type w} [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] {γ : ℝ → F} {a b : ℝ} {y : F} (hy : HasWeakIntegral γ a b y) (L : F →L[ℝ] G) : HasWeakIntegral (fun (t : ℝ) => L (γ t)) a b (L y)

Weak integrals commute with continuous linear maps.

theorem LCAnalysis.HasWeakIntegral.add_adjacent {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {γ : ℝ → F} {a b c : ℝ} {y z : F} (hγab : ContinuousOn γ (Set.uIcc a b)) (hγbc : ContinuousOn γ (Set.uIcc b c)) (hy : HasWeakIntegral γ a b y) (hz : HasWeakIntegral γ b c z) : HasWeakIntegral γ a c (y + z)

Additivity in the interval.

Change of variables

theorem LCAnalysis.hasWeakIntegral_comp_smul_deriv_iff {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {γ : ℝ → F} {a b : ℝ} {y : F} {φ φ' : ℝ → ℝ} (hφ : ∀ t ∈ Set.uIcc a b, HasDerivAt φ (φ' t) t) (hφ' : ContinuousOn φ' (Set.uIcc a b)) (hγ : ContinuousOn γ (φ '' Set.uIcc a b)) : HasWeakIntegral (fun (t : ℝ) => φ' t • γ (φ t)) a b y ↔ HasWeakIntegral γ (φ a) (φ b) y

Change of variables in weak integrals: if φ is C^1 on [a, b] and γ is continuous on φ '' [a, b], then y is a weak integral of γ over [φ a, φ b] if and only if it is a weak integral of t ↦ φ' t • γ (φ t) over [a, b].

theorem LCAnalysis.hasWeakIntegral_affine_iff {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {γ : ℝ → F} {y : F} {t s : ℝ} (hγ : ContinuousOn γ (Set.uIcc t (t + s))) : HasWeakIntegral (fun (r : ℝ) => s • γ (t + s * r)) 0 1 y ↔ HasWeakIntegral γ t (t + s) y

The affine case: ∫_t^{t+s} γ = s • ∫_0^1 γ(t + s r) dr.

The fundamental theorem of calculus

theorem LCAnalysis.hasWeakIntegral_sub_of_hasDirDerivAt {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {γ : ℝ → F} {a b : ℝ} {γ' : ℝ → F} (hγ : ∀ t ∈ Set.uIcc a b, HasDirDerivAt γ t 1 (γ' t)) (hγ' : ContinuousOn γ' (Set.uIcc a b)) : HasWeakIntegral γ' a b (γ b - γ a)

Fundamental theorem of calculus, first part: if γ has a continuous derivative γ' on [a, b], then γ b - γ a is the weak integral of γ' over [a, b]. No completeness of F is needed.

theorem LCAnalysis.ContDiffMBOn.hasWeakIntegral_dMB {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {f : E → F} {U : Set E} (hf : ContDiffMBOn 1 f U) {x h : E} (hxh : ∀ t ∈ Set.Icc 0 1, x + t • h ∈ U) : HasWeakIntegral (fun (t : ℝ) => dMB f (x + t • h, h)) 0 1 (f (x + h) - f x)

Fundamental theorem of calculus along a segment: if f is C^1 on a set containing the segment [x, x + h], then f (x + h) - f x = ∫₀¹ df(x + t h)(h) dt, the weak integral existing in F (no completeness assumption).

theorem LCAnalysis.exists_closed_convex_two_smul_subset {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] {N : Set F} (hN : N ∈ nhds 0) : ∃ W ∈ nhds 0, IsClosed W ∧ Convex ℝ W ∧ 2 • W ⊆ N

For a neighborhood N of 0 there is a closed convex neighborhood W of 0 with 2 • W ⊆ N.

theorem LCAnalysis.weakIntegral_eq_sub_of_hasDirDerivAt {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {γ : ℝ → F} {a b : ℝ} [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] [T2Space F] {γ' : ℝ → F} (hγ : ∀ t ∈ Set.uIcc a b, HasDirDerivAt γ t 1 (γ' t)) (hγ' : ContinuousOn γ' (Set.uIcc a b)) : weakIntegral γ' a b = γ b - γ a

theorem LCAnalysis.hasDirDerivAt_weakIntegral_right_of_exists {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {γ : ℝ → F} {a : ℝ} [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] [T2Space F] {I : Set ℝ} (hI : IsOpen I) (hIc : I.OrdConnected) (hγ : ContinuousOn γ I) (ha : a ∈ I) (hex : ∀ s ∈ I, ∃ (y : F), HasWeakIntegral γ a s y) {t : ℝ} (ht : t ∈ I) : HasDirDerivAt (fun (s : ℝ) => weakIntegral γ a s) t 1 (γ t)

Fundamental theorem of calculus, second part: if γ is continuous on an open interval I and the weak integrals ∫_a^s γ exist for s ∈ I, then s ↦ ∫_a^s γ is differentiable on I, with derivative γ.

theorem LCAnalysis.hasDirDerivAt_weakIntegral_right {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {γ : ℝ → F} {a : ℝ} [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] [T2Space F] [SeqComplete F] {I : Set ℝ} (hI : IsOpen I) (hIc : I.OrdConnected) (hγ : ContinuousOn γ I) (ha : a ∈ I) {t : ℝ} (ht : t ∈ I) : HasDirDerivAt (fun (s : ℝ) => weakIntegral γ a s) t 1 (γ t)

Fundamental theorem of calculus, second part, in a sequentially complete space: the indefinite integral of a curve that is continuous on an open interval I is differentiable on I, with derivative the curve itself.