Mackey completeness through Lipschitz curves

Glöckner–Neeb (Definition 1.1.17) call a curve γ : [a, b] → E Lipschitz if its difference quotients (γ s - γ t) / (s - t) form a bounded set, and call E Mackey complete if every Lipschitz curve has a weak integral. This file proves that this agrees with MackeyComplete, defined through Mackey–Cauchy sequences (Glöckner–Neeb, Remark 1.1.18(e); Kriegl–Michor, 2.2 and 2.14):

• MackeyComplete.exists_hasWeakIntegral_of_isLipschitzCurve: if Mackey–Cauchy sequences converge, Lipschitz curves have weak integrals (the dyadic Riemann sums of a Lipschitz curve form a Mackey–Cauchy sequence);
• MackeyComplete.of_integratesLipschitzCurves: conversely, if Lipschitz curves have weak integrals, Mackey–Cauchy sequences converge. Given a Mackey–Cauchy sequence u, we pass to a fast subsequence u (n j) and place the increments u (n (j + 1)) - u (n j) on tents supported on the intervals [1 - 2⁻ʲ, 1 - 2⁻ʲ⁻¹]. The resulting curve is Lipschitz on [0, 1], and its weak integral is lim u (n j) - u (n 0).
• mackeyComplete_iff_integratesLipschitzCurves: the equivalence.

def LCAnalysis.diffQuot {F : Type v} [AddCommGroup F] [Module ℝ F] (γ : ℝ → F) (a b : ℝ) : Set F

The difference quotients of γ on [a, b].

Equations

• LCAnalysis.diffQuot γ a b = {v : F | ∃ s ∈ Set.Icc a b, ∃ t ∈ Set.Icc a b, s ≠ t ∧ v = (s - t)⁻¹ • (γ s - γ t)}

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

A Lipschitz curve on [a, b] (Glöckner–Neeb, Definition 1.1.17(a)): its difference quotients form a bounded set.

Equations

• LCAnalysis.IsLipschitzCurve γ a b = Bornology.IsVonNBounded ℝ (LCAnalysis.diffQuot γ a b)

def LCAnalysis.IntegratesLipschitzCurves (F : Type v) [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] : Prop

Mackey completeness in the sense of Glöckner–Neeb, Definition 1.1.17(b): Lipschitz curves have weak integrals.

Equations

• LCAnalysis.IntegratesLipschitzCurves F = ∀ (γ : ℝ → F) (a b : ℝ), a < b → LCAnalysis.IsLipschitzCurve γ a b → ∃ (y : F), LCAnalysis.HasWeakIntegral γ a b y

theorem LCAnalysis.sub_eq_smul_diffQuot {F : Type v} [AddCommGroup F] [Module ℝ F] {γ : ℝ → F} {a b s t : ℝ} (hs : s ∈ Set.Icc a b) (ht : t ∈ Set.Icc a b) (hst : s ≠ t) : ∃ q ∈ diffQuot γ a b, γ s - γ t = (s - t) • q

theorem LCAnalysis.IsLipschitzCurve.continuousOn {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {γ : ℝ → F} {a b : ℝ} [IsTopologicalAddGroup F] (h : IsLipschitzCurve γ a b) : ContinuousOn γ (Set.Icc a b)

Lipschitz curves are continuous.

theorem LCAnalysis.sub_mem_smul_convexHull_diffQuot {F : Type v} [AddCommGroup F] [Module ℝ F] {γ : ℝ → F} {a b h : ℝ} (hh : 0 < h) {s t : ℝ} (hs : s ∈ Set.Icc a b) (ht : t ∈ Set.Icc a b) (hts : t ≤ s) (hst : s - t ≤ h) : γ s - γ t ∈ h • (convexHull ℝ) (insert 0 (diffQuot γ a b))

Increments of a curve over steps of length at most h lie in h • convexHull (insert 0 D), where D is the set of difference quotients.

theorem LCAnalysis.MackeyComplete.exists_hasWeakIntegral_of_isLipschitzCurve {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {γ : ℝ → F} {a b : ℝ} [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] [MackeyComplete F] (hab : a < b) (hγ : IsLipschitzCurve γ a b) : ∃ (y : F), HasWeakIntegral γ a b y

In a Mackey complete space, Lipschitz curves have weak integrals.

theorem LCAnalysis.MackeyComplete.integratesLipschitzCurves {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] [MackeyComplete F] : IntegratesLipschitzCurves F

Tents

noncomputable def LCAnalysis.tentLeft (j : ℕ) : ℝ

Left endpoint 1 - 2⁻ʲ of the j-th interval.

Equations

• LCAnalysis.tentLeft j = 1 - (1 / 2) ^ j

noncomputable def LCAnalysis.tentWidth (j : ℕ) : ℝ

Width 2⁻ʲ⁻¹ of the j-th interval.

Equations

• LCAnalysis.tentWidth j = (1 / 2) ^ (j + 1)

noncomputable def LCAnalysis.tent (j : ℕ) (t : ℝ) : ℝ

The tent of height tentWidth j / 2 on [tentLeft j, tentLeft (j + 1)].

Equations

• LCAnalysis.tent j t = max 0 (LCAnalysis.tentWidth j / 2 - |t - (LCAnalysis.tentLeft j + LCAnalysis.tentWidth j / 2)|)

theorem LCAnalysis.tentLeft_succ (j : ℕ) : tentLeft (j + 1) = tentLeft j + tentWidth j

theorem LCAnalysis.tentWidth_pos (j : ℕ) : 0 < tentWidth j

theorem LCAnalysis.tentWidth_le (j : ℕ) : tentWidth j ≤ 1 / 2

theorem LCAnalysis.tentLeft_mono : Monotone tentLeft

theorem LCAnalysis.tentLeft_nonneg (j : ℕ) : 0 ≤ tentLeft j

theorem LCAnalysis.tentLeft_lt_one (j : ℕ) : tentLeft j < 1

theorem LCAnalysis.tent_nonneg (j : ℕ) (t : ℝ) : 0 ≤ tent j t

theorem LCAnalysis.tent_le_one (j : ℕ) (t : ℝ) : tent j t ≤ 1

theorem LCAnalysis.tent_eq_zero_of_le {j : ℕ} {t : ℝ} (ht : t ≤ tentLeft j) : tent j t = 0

theorem LCAnalysis.tent_eq_zero_of_ge {j : ℕ} {t : ℝ} (ht : tentLeft (j + 1) ≤ t) : tent j t = 0

theorem LCAnalysis.abs_tent_sub_le (j : ℕ) (s t : ℝ) : |tent j s - tent j t| ≤ |s - t|

theorem LCAnalysis.tent_eq_left {j : ℕ} {t : ℝ} (ht : t ∈ Set.Icc (tentLeft j) (tentLeft j + tentWidth j / 2)) : tent j t = t - tentLeft j

theorem LCAnalysis.tent_eq_right {j : ℕ} {t : ℝ} (ht : t ∈ Set.Icc (tentLeft j + tentWidth j / 2) (tentLeft j + tentWidth j)) : tent j t = tentLeft j + tentWidth j - t

theorem LCAnalysis.continuous_tent (j : ℕ) : Continuous (tent j)

theorem LCAnalysis.integral_tent (j : ℕ) : ∫ (t : ℝ) in 0..1, tent j t = tentWidth j ^ 2 / 4

noncomputable def LCAnalysis.tentSum {F : Type v} [AddCommGroup F] [Module ℝ F] (e : ℕ → F) (N : ℕ) (t : ℝ) : F

The partial sums ∑_{j < N} tent j t • e j.

Equations

• LCAnalysis.tentSum e N t = ∑ j ∈ Finset.range N, LCAnalysis.tent j t • e j

noncomputable def LCAnalysis.tentCurve {F : Type v} [AddCommGroup F] [Module ℝ F] (e : ℕ → F) (t : ℝ) : F

The curve ∑_j tent j t • e j (a finite sum for each t).

Equations

• LCAnalysis.tentCurve e t = if h : ∃ (N : ℕ), t ≤ LCAnalysis.tentLeft N then LCAnalysis.tentSum e (Nat.find h) t else 0

theorem LCAnalysis.tentSum_stable {F : Type v} [AddCommGroup F] [Module ℝ F] (e : ℕ → F) {M N : ℕ} (hMN : M ≤ N) {t : ℝ} (ht : t ≤ tentLeft M) : tentSum e N t = tentSum e M t

theorem LCAnalysis.tentSum_eq_zero_of_one_le {F : Type v} [AddCommGroup F] [Module ℝ F] (e : ℕ → F) (N : ℕ) {t : ℝ} (ht : 1 ≤ t) : tentSum e N t = 0

theorem LCAnalysis.eventually_tentCurve_eq {F : Type v} [AddCommGroup F] [Module ℝ F] (e : ℕ → F) (t : ℝ) : ∀ᶠ (N : ℕ) in Filter.atTop, tentCurve e t = tentSum e N t

Sums in multiples of a convex set

theorem LCAnalysis.smul_mem_smul_of_abs_le {F : Type v} [AddCommGroup F] [Module ℝ F] {K : Set F} (hK : Convex ℝ K) (h0 : 0 ∈ K) (hneg : ∀ x ∈ K, -x ∈ K) {x : F} (hx : x ∈ K) {μ c : ℝ} (hμ : |μ| ≤ c) : μ • x ∈ c • K

theorem LCAnalysis.sum_mem_smul {F : Type v} [AddCommGroup F] [Module ℝ F] {K : Set F} (hK : Convex ℝ K) (h0 : 0 ∈ K) {ι : Type u_1} (s : Finset ι) {x : ι → F} {c : ι → ℝ} (hc : ∀ i ∈ s, 0 ≤ c i) (hx : ∀ i ∈ s, x i ∈ c i • K) : ∑ i ∈ s, x i ∈ (∑ i ∈ s, c i) • K

theorem LCAnalysis.mem_smul_of_le {F : Type v} [AddCommGroup F] [Module ℝ F] {K : Set F} (hK : Convex ℝ K) (h0 : 0 ∈ K) {x : F} {c d : ℝ} (hx : x ∈ c • K) (hc : 0 ≤ c) (hcd : c ≤ d) : x ∈ d • K

theorem LCAnalysis.sum_Ico_half_pow {N M : ℕ} (h : N ≤ M) : ∑ j ∈ Finset.Ico N M, (1 / 2) ^ (j + 1) = (1 / 2) ^ N - (1 / 2) ^ M

Mackey–Cauchy sequences with a convergent subsequence

theorem LCAnalysis.tendsto_of_mackeyCauchy_of_subseq {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] {u : ℕ → F} {B : Set F} {r : ℕ → ℝ} (hB : Bornology.IsVonNBounded ℝ B) (hr : Filter.Tendsto r Filter.atTop (nhds 0)) (hu : ∀ (k l : ℕ), k ≤ l → u l - u k ∈ r k • B) {n : ℕ → ℕ} (hn : StrictMono n) {x : F} (hx : Filter.Tendsto (fun (j : ℕ) => u (n j)) Filter.atTop (nhds x)) : Filter.Tendsto u Filter.atTop (nhds x)

A Mackey–Cauchy sequence with a convergent subsequence converges.

theorem LCAnalysis.MackeyComplete.of_integratesLipschitzCurves {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] (h : IntegratesLipschitzCurves F) : MackeyComplete F

If Lipschitz curves have weak integrals, then Mackey–Cauchy sequences converge.

theorem LCAnalysis.mackeyComplete_iff_integratesLipschitzCurves {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] : MackeyComplete F ↔ IntegratesLipschitzCurves F

Mackey completeness through Mackey–Cauchy sequences agrees with the definition of Glöckner–Neeb (Definition 1.1.17(b)) through Lipschitz curves.