Existence of weak integrals #
Weak integrals of continuous curves need not exist in a general locally convex space; they do under completeness hypotheses (Glöckner–Neeb, §1.1; Kriegl–Michor, §2):
- if
Fis sequentially complete, every continuous curve[a, b] → Fhas a weak integral; - if
Fis Mackey complete, everyC^1curve has a weak integral.
In both cases the integral is the limit of the dyadic Riemann sums. Mackey completeness is
strictly weaker than sequential completeness, and it is the natural hypothesis for smooth
calculus. As an application, parameter-dependent integrals of C^k maps are C^k
(sequentially complete case), or C^k maps give C^{k-1} integrals (Mackey complete case),
with no existence hypotheses.
Completeness notions are stated directly in terms of the topological vector space structure
(u n - u m eventually in every neighborhood of 0), so no uniform structure is needed; for a
uniform additive group, completeness implies sequential completeness.
A topological vector space is sequentially complete if every Cauchy sequence converges.
- exists_tendsto (u : ℕ → F) : (∀ W ∈ nhds 0, ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, u n - u m ∈ W) → ∃ (y : F), Filter.Tendsto u Filter.atTop (nhds y)
Instances
A topological vector space is Mackey complete if every Mackey–Cauchy sequence converges:
u l - u k ∈ r k • B for k ≤ l, with B bounded and r k → 0.
- exists_tendsto (u : ℕ → F) (B : Set F) (r : ℕ → ℝ) : Bornology.IsVonNBounded ℝ B → Filter.Tendsto r Filter.atTop (nhds 0) → (∀ (k l : ℕ), k ≤ l → u l - u k ∈ r k • B) → ∃ (y : F), Filter.Tendsto u Filter.atTop (nhds y)
Instances
A one-sided Cauchy condition implies the two-sided one.
Complete uniform additive groups are sequentially complete.
Riemann sums #
The Riemann sum of γ over [a, b] with N equal subintervals and left endpoints.
Equations
- LCAnalysis.riemannSum γ a b N = ((b - a) / ↑N) • ∑ i ∈ Finset.range N, γ (a + ↑i * ((b - a) / ↑N))
Instances For
Comparison of a Riemann sum with a refinement: if the increments of γ over steps of
length at most (b - a) / N lie in a convex set V, then the difference lies in (b - a) • V.
Riemann sums of a continuous real function converge to its integral.
Existence of weak integrals #
If the dyadic Riemann sums of a continuous curve converge, the limit is its weak integral.
Uniform continuity of continuous curves on compact intervals.
In a sequentially complete space, continuous curves have weak integrals.
In a sequentially complete space, continuous curves have weak integrals.
In a locally convex space, the convex hull of a bounded set is bounded.
Mean value inclusion for curves: increments over steps of length at most h lie in
h • B, where B is the closed convex hull of [0, 1] • γ'([a, b]).
In a Mackey complete space, C^1 curves have weak integrals.
In a Mackey complete space, C^1 curves have weak integrals.
Parameter-dependent integrals #
The weak integral of γ over [a, b] (junk value 0 if it does not exist).
Equations
- LCAnalysis.weakIntegral γ a b = if h : ∃ (y : F), LCAnalysis.HasWeakIntegral γ a b y then h.choose else 0
Instances For
The induction behind the C^k results: if every C^m map on U ×ˢ T has weak integrals
along [a, b] in the second variable, then C^(k + m) maps give C^k integrals.
Parameter-dependent integrals in sequentially complete spaces: if f is C^k on
U ×ˢ T, then x ↦ ∫_a^b f (x, t) dt is C^k on U.
Parameter-dependent integrals in Mackey complete spaces: if f is C^(k+1) on
U ×ˢ T, then x ↦ ∫_a^b f (x, t) dt is C^k on U.
Smooth parameter-dependent integrals in Mackey complete spaces.
Differentiation under the integral sign, sequentially complete case:
d(∫_a^b f(·, t) dt)(x)(h) = ∫_a^b d₁f((x, t), h) dt for f of class C^1.