The maximal inequality behind the sewing lemma

The core estimate of rough integration theory (Friz–Hairer, Lemma 4.2; Cass–Salvi lecture notes, arXiv:2404.06583): if a two-parameter map Ξ has its Chen defect δΞ(s,u,t) = Ξ s t - Ξ s u - Ξ u t controlled by ω^θ for a control ω, then Riemann sums of Ξ along any partition of [s,t] stay within a uniform multiple of ω(s,t)^θ of Ξ s t.

The proof is the classical point-removal argument: any partition with k ≥ 2 intervals contains an interior point whose neighbouring control mass is at most 2 ω(s,t) / (k-1) (by superadditivity of ω applied to alternating subchains), and removing it changes the Riemann sum by at most (2 ω(s,t) / (k-1))^θ; iterating yields the bound Σ_{j≥1} (2 ω(s,t)/j)^θ.

All estimates are stated in ENNReal via the extended norm ‖·‖ₑ, so no summability side conditions are needed for the maximal inequality itself.

def RoughPaths.Sewing.pairSum {T : Type u} {E : Type v} [AddCommMonoid E] (f : T → T → E) : List T → E

The sum of a two-parameter function along the consecutive pairs of a partition, Σᵢ f pᵢ pᵢ₊₁.

Equations

• RoughPaths.Sewing.pairSum f (x_1 :: y :: rest) = f x_1 y + RoughPaths.Sewing.pairSum f (y :: rest)
• RoughPaths.Sewing.pairSum f x✝ = 0

@[simp]

theorem RoughPaths.Sewing.pairSum_nil {T : Type u} {E : Type v} [AddCommMonoid E] (f : T → T → E) : pairSum f [] = 0

@[simp]

theorem RoughPaths.Sewing.pairSum_single {T : Type u} {E : Type v} [AddCommMonoid E] (f : T → T → E) (x : T) : pairSum f [x] = 0

@[simp]

theorem RoughPaths.Sewing.pairSum_cons_cons {T : Type u} {E : Type v} [AddCommMonoid E] (f : T → T → E) (x y : T) (rest : List T) : pairSum f (x :: y :: rest) = f x y + pairSum f (y :: rest)

def RoughPaths.Sewing.triples {T : Type u} : List T → List (T × T × T)

The list of consecutive triples of a partition.

Equations

• RoughPaths.Sewing.triples (x_1 :: y :: z :: rest) = (x_1, y, z) :: RoughPaths.Sewing.triples (y :: z :: rest)
• RoughPaths.Sewing.triples x✝ = []

@[simp]

theorem RoughPaths.Sewing.triples_nil {T : Type u} : triples [] = []

@[simp]

theorem RoughPaths.Sewing.triples_single {T : Type u} (x : T) : triples [x] = []

@[simp]

theorem RoughPaths.Sewing.triples_pair {T : Type u} (x y : T) : triples [x, y] = []

@[simp]

theorem RoughPaths.Sewing.triples_cons_cons_cons {T : Type u} (x y z : T) (rest : List T) : triples (x :: y :: z :: rest) = (x, y, z) :: triples (y :: z :: rest)

theorem RoughPaths.Sewing.length_triples {T : Type u} (p : List T) : (triples p).length = p.length - 2

theorem RoughPaths.Sewing.eq_append_of_mem_triples {T : Type u} {p : List T} {x y z : T} : (x, y, z) ∈ triples p → ∃ (u : List T) (v : List T), p = u ++ x :: y :: z :: v

A membership in the triple list decomposes the partition.

theorem RoughPaths.Sewing.isChain_head_le_getLast {T : Type u} [Preorder T] (a : T) (l : List T) : List.IsChain (fun (x1 x2 : T) => x1 ≤ x2) (a :: l) → a ≤ (a :: l).getLast ⋯

The head of a chained list is below its last element.

theorem RoughPaths.Sewing.pairSum_le_head_getLast {T : Type u} [Preorder T] (ω : Control T) (x : T) (q : List T) : List.IsChain (fun (x1 x2 : T) => x1 ≤ x2) (x :: q) → pairSum (fun (a b : T) => ω.toFun a b) (x :: q) ≤ ω.toFun x ((x :: q).getLast ⋯)

The pair sum of a control along any chained list is bounded by the control between the head and the last point.

theorem RoughPaths.Sewing.control_mono {T : Type u} [Preorder T] (ω : Control T) {s a b t : T} (hsa : s ≤ a) (hab : a ≤ b) (hbt : b ≤ t) : ω.toFun a b ≤ ω.toFun s t

Monotonicity of controls in nested intervals.

def RoughPaths.Sewing.tripleSum {T : Type u} [Preorder T] (ω : Control T) (p : List T) : ENNReal

The sum of the control over the consecutive triples of a partition.

Equations

• RoughPaths.Sewing.tripleSum ω p = (List.map (fun (t : T × T × T) => ω.toFun t.1 t.2.2) (RoughPaths.Sewing.triples p)).sum

@[simp]

theorem RoughPaths.Sewing.tripleSum_cons_cons_cons {T : Type u} [Preorder T] (ω : Control T) (x y z : T) (rest : List T) : tripleSum ω (x :: y :: z :: rest) = ω.toFun x z + tripleSum ω (y :: z :: rest)

theorem RoughPaths.Sewing.tripleSum_le {T : Type u} [Preorder T] (ω : Control T) (x y : T) (q : List T) : List.IsChain (fun (x1 x2 : T) => x1 ≤ x2) (x :: y :: q) → tripleSum ω (x :: y :: q) ≤ ω.toFun x ((x :: y :: q).getLast ⋯) + ω.toFun y ((x :: y :: q).getLast ⋯)

The alternating superadditivity bound: the triple sum of a control along a chained partition is at most twice the control between the extreme points (the even- and odd-indexed subchains each contribute one copy).

theorem RoughPaths.Sewing.exists_length_mul_le_sum {α : Type v} (f : α → ENNReal) (l : List α) : l ≠ [] → ∃ a ∈ l, ↑l.length * f a ≤ (List.map f l).sum

A nonempty list contains an element whose value is at most the average: length * f a ≤ Σ f.

theorem RoughPaths.Sewing.pairSum_append {T : Type u} {E : Type v} [AddCommMonoid E] (f : T → T → E) (u : List T) (x : T) (w : List T) : pairSum f (u ++ x :: w) = pairSum f (u ++ [x]) + pairSum f (x :: w)

Splitting a pair sum at an interior point.

theorem RoughPaths.Sewing.maximal_inequality {T : Type u} [Preorder T] {E : Type v} [SeminormedAddCommGroup E] (ω : Control T) (Ξ : T → T → E) (θ : ℝ) (hθ : 0 ≤ θ) (hδ : ∀ ⦃a b c : T⦄, a ≤ b → b ≤ c → ‖Ξ a c - Ξ a b - Ξ b c‖ₑ ≤ ω.toFun a c ^ θ) (n : ℕ) (p : List T) (hne : p ≠ []) : p.length = n + 2 → List.IsChain (fun (x1 x2 : T) => x1 ≤ x2) p → ‖pairSum Ξ p - Ξ (p.head hne) (p.getLast hne)‖ₑ ≤ ∑ j ∈ Finset.range n, (2 * ω.toFun (p.head hne) (p.getLast hne) / (↑j + 1)) ^ θ

The maximal inequality of the sewing lemma (Friz–Hairer, Lemma 4.2; Cass–Salvi, arXiv:2404.06583, the key estimate behind rough integration): if the Chen defect δΞ(a,b,c) = Ξ a c - Ξ a b - Ξ b c is bounded by ω(a,c)^θ for a control ω, then the Riemann sum of Ξ along any chained partition with n + 1 intervals differs from Ξ of the endpoints by at most Σ_{j=1}^{n} (2 ω(s,t)/j)^θ.

Proved by the point-removal argument: the pigeonhole applied to the alternating superadditivity bound produces an interior point whose removal costs at most (2 ω(s,t)/n)^θ.

theorem RoughPaths.Sewing.maximal_inequality_tsum {T : Type u} [Preorder T] {E : Type v} [SeminormedAddCommGroup E] (ω : Control T) (Ξ : T → T → E) (θ : ℝ) (hθ : 0 ≤ θ) (hδ : ∀ ⦃a b c : T⦄, a ≤ b → b ≤ c → ‖Ξ a c - Ξ a b - Ξ b c‖ₑ ≤ ω.toFun a c ^ θ) (n : ℕ) (p : List T) (hne : p ≠ []) (hlen : p.length = n + 2) (hchain : List.IsChain (fun (x1 x2 : T) => x1 ≤ x2) p) : ‖pairSum Ξ p - Ξ (p.head hne) (p.getLast hne)‖ₑ ≤ (∑' (j : ℕ), (2 / (↑j + 1)) ^ θ) * ω.toFun (p.head hne) (p.getLast hne) ^ θ

The maximal inequality with a partition-independent constant: Riemann sums along any chained partition stay within (Σ_j (2/(j+1))^θ) · ω(s,t)^θ of the endpoint increment.

def RoughPaths.Sewing.HasFinePartitions {T : Type u} [Preorder T] (ω : Control T) : Prop

A control admits fine partitions if between any two comparable times there is an interpolating chain all of whose consecutive control increments are at most ε. This holds e.g. for controls continuous on a compact time interval.

Equations

• RoughPaths.Sewing.HasFinePartitions ω = ∀ ⦃s t : T⦄, s ≤ t → ∀ (ε : ENNReal), 0 < ε → ∃ (q : List T), List.IsChain (fun (a b : T) => a ≤ b ∧ ω.toFun a b ≤ ε) (s :: (q ++ [t]))

theorem RoughPaths.Sewing.sewing_unique {T : Type u} [Preorder T] {E : Type v} [NormedAddCommGroup E] (ω : Control T) (Ξ : T → T → E) {θ : ℝ} (hθ : 1 < θ) {C : ENNReal} (hC : C ≠ ⊤) (hfine : HasFinePartitions ω) {I I' : T → E} (hI : ∀ ⦃a b : T⦄, a ≤ b → ‖I b - I a - Ξ a b‖ₑ ≤ C * ω.toFun a b ^ θ) (hI' : ∀ ⦃a b : T⦄, a ≤ b → ‖I' b - I' a - Ξ a b‖ₑ ≤ C * ω.toFun a b ^ θ) {s t : T} (hst : s ≤ t) (hω : ω.toFun s t ≠ ⊤) : I t - I s = I' t - I' s

Uniqueness in the sewing lemma (Friz–Hairer, Lemma 4.2; Cass–Salvi, arXiv:2404.06583): two primitives of Ξ with remainder O(ω^θ), θ > 1, have equal increments, provided the control admits fine partitions.

def RoughPaths.Sewing.glue {T : Type u} : List (T × List T) → T → List T

Glue a partition (given as segment starting points with interpolating interior chains) into a single refined partition ending at t.

Equations

• RoughPaths.Sewing.glue [] x✝ = [x✝]
• RoughPaths.Sewing.glue ((x_2, q) :: rest) x✝ = x_2 :: (q ++ RoughPaths.Sewing.glue rest x✝)

@[simp]

theorem RoughPaths.Sewing.glue_nil {T : Type u} (t : T) : glue [] t = [t]

@[simp]

theorem RoughPaths.Sewing.glue_cons {T : Type u} (x : T) (q : List T) (rest : List (T × List T)) (t : T) : glue ((x, q) :: rest) t = x :: (q ++ glue rest t)

def RoughPaths.Sewing.basePoints {T : Type u} : List (T × List T) → T → List T

The coarse partition underlying a glued refinement.

Equations

• RoughPaths.Sewing.basePoints [] x✝ = [x✝]
• RoughPaths.Sewing.basePoints ((x_2, q) :: rest) x✝ = x_2 :: RoughPaths.Sewing.basePoints rest x✝

@[simp]

theorem RoughPaths.Sewing.basePoints_nil {T : Type u} (t : T) : basePoints [] t = [t]

@[simp]

theorem RoughPaths.Sewing.basePoints_cons {T : Type u} (x : T) (q : List T) (rest : List (T × List T)) (t : T) : basePoints ((x, q) :: rest) t = x :: basePoints rest t

theorem RoughPaths.Sewing.glue_ne_nil {T : Type u} (ps : List (T × List T)) (t : T) : glue ps t ≠ []

theorem RoughPaths.Sewing.head_glue {T : Type u} (x : T) (q : List T) (rest : List (T × List T)) (t : T) : (glue ((x, q) :: rest) t).head ⋯ = x

theorem RoughPaths.Sewing.head_basePoints {T : Type u} (x : T) (q : List T) (rest : List (T × List T)) (t : T) : (basePoints ((x, q) :: rest) t).head ⋯ = x

The head of a glued partition is the head of its base.

theorem RoughPaths.Sewing.pairSum_glue {T : Type u} {E : Type v} [SeminormedAddCommGroup E] (f : T → T → E) (ps : List (T × List T)) (t : T) : pairSum f (glue ps t) = List.foldr (fun (seg : (T × List T) × T) (acc : E) => pairSum f (seg.1.1 :: (seg.1.2 ++ [seg.2])) + acc) 0 (ps.zip ((List.map Prod.fst ps).tail ++ [t]))

The pair sum along a glued partition splits into the segment sums.

theorem RoughPaths.Sewing.refine_bound {T : Type u} [Preorder T] {E : Type v} [SeminormedAddCommGroup E] (ω : Control T) (Ξ : T → T → E) (θ : ℝ) (hθ : 0 ≤ θ) (hδ : ∀ ⦃a b c : T⦄, a ≤ b → b ≤ c → ‖Ξ a c - Ξ a b - Ξ b c‖ₑ ≤ ω.toFun a c ^ θ) (ps : List (T × List T)) (t : T) : List.IsChain (fun (x1 x2 : T) => x1 ≤ x2) (glue ps t) → ‖pairSum Ξ (glue ps t) - pairSum Ξ (basePoints ps t)‖ₑ ≤ (∑' (j : ℕ), (2 / (↑j + 1)) ^ θ) * pairSum (fun (a b : T) => ω.toFun a b ^ θ) (basePoints ps t)

The refinement bound: refining each interval of a partition changes the Riemann sum by at most the sewing constant times the θ-mass of the coarse partition (Friz–Hairer, Lemma 4.2, the refinement step).

theorem RoughPaths.Sewing.pairSum_rpow_le_of_fine {T : Type u} [Preorder T] (ω : Control T) {θ : ℝ} (hθ1 : 0 ≤ θ - 1) {ε : ENNReal} (x : T) (q : List T) (t : T) : List.IsChain (fun (a b : T) => a ≤ b ∧ ω.toFun a b ≤ ε) (x :: (q ++ [t])) → pairSum (fun (a b : T) => ω.toFun a b ^ θ) (x :: (q ++ [t])) ≤ ε ^ (θ - 1) * ω.toFun x t

The θ-mass of a fine partition is small: if every interval of a chained partition has control at most ε, its θ-mass is bounded by ε^{θ-1} ω(s,t).

theorem RoughPaths.Sewing.sewingConst_lt_top {θ : ℝ} (hθ : 1 < θ) : ∑' (j : ℕ), (2 / (↑j + 1)) ^ θ < ⊤

The sewing constant is finite for θ > 1: the harmonic-power series Σ_j (2/(j+1))^θ converges.

theorem RoughPaths.Sewing.exists_fine_refinement {T : Type u} [Preorder T] (ω : Control T) (hfine : HasFinePartitions ω) {ε : ENNReal} (hε : 0 < ε) (q : List T) (x t : T) : List.IsChain (fun (x1 x2 : T) => x1 ≤ x2) (x :: (q ++ [t])) → ∃ (ps : List (T × List T)), basePoints ps t = x :: (q ++ [t]) ∧ List.IsChain (fun (a b : T) => a ≤ b ∧ ω.toFun a b ≤ ε) (glue ps t)

Every chained partition admits a fine refinement: given fine partitions of the control, each interval can be interpolated by a chain with control increments at most ε, assembling into a glued refinement of the whole partition.

theorem RoughPaths.Sewing.glue_eq_concat {T : Type u} (ps : List (T × List T)) (t : T) : ∃ (mid : List T), glue ps t = mid ++ [t]

Every glued partition ends at its endpoint.

theorem RoughPaths.Sewing.refine_step {T : Type u} [Preorder T] {E : Type v} [SeminormedAddCommGroup E] (ω : Control T) (Ξ : T → T → E) {θ : ℝ} (hθ1 : 0 ≤ θ - 1) (hθ0 : 0 ≤ θ) (hδ : ∀ ⦃a b c : T⦄, a ≤ b → b ≤ c → ‖Ξ a c - Ξ a b - Ξ b c‖ₑ ≤ ω.toFun a c ^ θ) (hfine : HasFinePartitions ω) {ε ε' : ENNReal} (hε' : 0 < ε') (q : List T) (x t : T) (hchain : List.IsChain (fun (a b : T) => a ≤ b ∧ ω.toFun a b ≤ ε) (x :: (q ++ [t]))) : ∃ (q' : List T), List.IsChain (fun (a b : T) => a ≤ b ∧ ω.toFun a b ≤ ε') (x :: (q' ++ [t])) ∧ ‖pairSum Ξ (x :: (q' ++ [t])) - pairSum Ξ (x :: (q ++ [t]))‖ₑ ≤ (∑' (j : ℕ), (2 / (↑j + 1)) ^ θ) * (ε ^ (θ - 1) * ω.toFun x t)

The combined refinement step: a partition that is fine at level ε admits a refinement fine at any level ε' > 0 whose Riemann sum moves by at most K ε^{θ-1} ω(x,t).

theorem RoughPaths.Sewing.sewing_exists {T : Type u} [Preorder T] {E : Type v} [NormedAddCommGroup E] [CompleteSpace E] (ω : Control T) (Ξ : T → T → E) {θ : ℝ} (hθ : 1 < θ) (hδ : ∀ ⦃a b c : T⦄, a ≤ b → b ≤ c → ‖Ξ a c - Ξ a b - Ξ b c‖ₑ ≤ ω.toFun a c ^ θ) (hfine : HasFinePartitions ω) {s t : T} (hst : s ≤ t) (hω : ω.toFun s t ≠ ⊤) : ∃ (L : E) (Q : ℕ → List T), (∀ (n : ℕ), ∃ (q : List T), Q n = s :: (q ++ [t]) ∧ List.IsChain (fun (x1 x2 : T) => x1 ≤ x2) (Q n)) ∧ Filter.Tendsto (fun (n : ℕ) => pairSum Ξ (Q n)) Filter.atTop (nhds L) ∧ ‖L - Ξ s t‖ₑ ≤ (∑' (j : ℕ), (2 / (↑j + 1)) ^ θ) * ω.toFun s t ^ θ

The sewing lemma, existence (Friz–Hairer, Lemma 4.2; Cass–Salvi, arXiv:2404.06583): if the Chen defect of Ξ is controlled by ω^θ with θ > 1 and the control admits fine partitions, then over every interval the Riemann sums along a refining sequence of partitions converge to a limit L — the rough integral — with the sewing remainder bound ‖L - Ξ s t‖ ≤ K ω(s,t)^θ.