Weak integrals of curves and parameter-dependent integrals

For a curve γ : ℝ → F in a locally convex space, y is a weak integral of γ over [a, b] if φ y = ∫_a^b φ (γ t) dt for every continuous linear functional φ (Glöckner–Neeb, §1.1). It is unique when it exists (Hahn–Banach), but in general it need not exist in F.

• Mean value inclusion: if γ takes values in a closed convex set W ∋ 0, then y ∈ (b - a + 1) • W; so weak integrals of uniformly small curves are small.
• Continuity of parameter-dependent weak integrals.
• Differentiation under the integral sign: if f (x, t) has jointly continuous partial derivatives in x and the relevant weak integrals exist, then d(∫_a^b f(·, t) dt)(x)(h) = ∫_a^b d₁f((x, t), h) dt.

Existence of weak integrals under completeness hypotheses is in LCAnalysis.IntegralExistence.

def LCAnalysis.HasWeakIntegral {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (γ : ℝ → F) (a b : ℝ) (y : F) : Prop

y is a weak integral of γ over [a, b].

Equations

• LCAnalysis.HasWeakIntegral γ a b y = ∀ (φ : F →L[ℝ] ℝ), φ y = ∫ (t : ℝ) in a..b, φ (γ t)

theorem LCAnalysis.HasWeakIntegral.unique {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] [T2Space F] {γ : ℝ → F} {a b : ℝ} {y z : F} (hy : HasWeakIntegral γ a b y) (hz : HasWeakIntegral γ a b z) : y = z

theorem LCAnalysis.HasWeakIntegral.sub {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {γ η : ℝ → F} {a b : ℝ} {y z : F} (hab : a ≤ b) (hγ : ContinuousOn γ (Set.Icc a b)) (hη : ContinuousOn η (Set.Icc 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_smul {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {γ : ℝ → F} {a b : ℝ} {y : F} (hy : HasWeakIntegral γ a b y) (c : ℝ) : HasWeakIntegral (fun (t : ℝ) => c • γ t) a b (c • y)

theorem LCAnalysis.HasWeakIntegral.mem_smul {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] {γ : ℝ → F} {a b : ℝ} {y : F} (hab : a ≤ b) (hγ : ContinuousOn γ (Set.Icc a b)) (hy : HasWeakIntegral γ a b y) {W : Set F} (hWc : Convex ℝ W) (hWcl : IsClosed W) (hW0 : 0 ∈ W) (hγW : ∀ t ∈ Set.Icc a b, γ t ∈ W) : y ∈ (b - a + 1) • W

Mean value inclusion for weak integrals.

theorem LCAnalysis.exists_nhds_weakIntegral_mem {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] {a b : ℝ} (hab : a ≤ b) {N : Set F} (hN : N ∈ nhds 0) : ∃ W ∈ nhds 0, ∀ (γ : ℝ → F) (y : F), ContinuousOn γ (Set.Icc a b) → HasWeakIntegral γ a b y → (∀ t ∈ Set.Icc a b, γ t ∈ W) → y ∈ N

Weak integrals of uniformly small curves are small.

theorem LCAnalysis.continuousOn_weakIntegral {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] {a b : ℝ} {X : Type u_1} [TopologicalSpace X] {f : X × ℝ → F} {U : Set X} {T : Set ℝ} (hU : IsOpen U) (hT : IsOpen T) (hab : a ≤ b) (hTab : Set.Icc a b ⊆ T) (hf : ContinuousOn f (U ×ˢ T)) {I : X → F} (hI : ∀ x ∈ U, HasWeakIntegral (fun (t : ℝ) => f (x, t)) a b (I x)) : ContinuousOn I U

Parameter-dependent weak integrals of continuous maps are continuous.

theorem LCAnalysis.hasDirDerivAt_weakIntegral {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] [T2Space F] {a b : ℝ} {f : E × ℝ → F} {U : Set E} {T : Set ℝ} (hU : IsOpen U) (hT : IsOpen T) (hab : a ≤ b) (hTab : Set.Icc a b ⊆ T) (hf : ContinuousOn f (U ×ˢ T)) {D : E × ℝ → E → F} (hd : ∀ p ∈ U ×ˢ T, ∀ (h : E), HasDirDerivAt f p (h, 0) (D p h)) (hD : ContinuousOn (fun (q : (E × ℝ) × E) => D q.1 q.2) ((U ×ˢ T) ×ˢ Set.univ)) {I : E → F} (hI : ∀ x ∈ U, HasWeakIntegral (fun (t : ℝ) => f (x, t)) a b (I x)) {x : E} (hx : x ∈ U) (h : E) {J : F} (hJ : HasWeakIntegral (fun (t : ℝ) => D (x, t) h) a b J) : HasDirDerivAt I x h J

Differentiation under the integral sign, for weak integrals.

theorem LCAnalysis.ContDiffMBOn.contDiffMBOn_one_of_hasWeakIntegral {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] [T2Space F] {a b : ℝ} {f : E × ℝ → F} {U : Set E} {T : Set ℝ} (hU : IsOpen U) (hT : IsOpen T) (hab : a ≤ b) (hTab : Set.Icc a b ⊆ T) (hf : ContDiffMBOn 1 f (U ×ˢ T)) {I : E → F} (hI : ∀ x ∈ U, HasWeakIntegral (fun (t : ℝ) => f (x, t)) a b (I x)) {J : E × E → F} (hJ : ∀ x ∈ U, ∀ (h : E), HasWeakIntegral (fun (t : ℝ) => dMB f ((x, t), h, 0)) a b (J (x, h))) : ContDiffMBOn 1 I U ∧ ∀ x ∈ U, ∀ (h : E), dMB I (x, h) = J (x, h)

Parameter-dependent weak integrals of C^1 maps are C^1, provided the weak integrals of the partial derivatives exist: d(∫_a^b f(·, t) dt)(x)(h) = ∫_a^b d₁f((x, t), h) dt.