The additive sewing lemma: limit construction

Along a geometric sequence of finenesses the Riemann sums of fine partitions form a Cauchy sequence; its limit is the sewing I s t. The resulting two-parameter map is additive (I s u + I u t = I s t), close to the germ (‖I s t − Ξ s t‖ₑ ≤ K·ω^θ), and approximates every fine partition's Riemann sum — hence is the mesh limit and is unique among additive maps with a germ bound.

theorem RoughPaths.Sewing.pow_rpow_exchange {θ : ℝ} (k : ℕ) : (2⁻¹ ^ k) ^ (θ - 1) = (2⁻¹ ^ (θ - 1)) ^ k

The rpow/pow exchange for the geometric fineness sequence.

theorem RoughPaths.Sewing.exists_sewing_limit {T : Type u} [LinearOrder 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), ∀ (ε : ENNReal) (mid : List T), List.IsChain (fun (a b : T) => a ≤ b ∧ ω.toFun a b ≤ ε) (s :: (mid ++ [t])) → ‖L - pairSum Ξ (s :: (mid ++ [t]))‖ₑ ≤ sewingConst θ * (ε ^ (θ - 1) * ω.toFun s t)

Existence of the sewing limit on one interval: there is L within K·ε^{θ−1}·ω(s,t) of the Riemann sum of every ε-fine partition.

theorem RoughPaths.Sewing.sewing {T : Type u} [LinearOrder 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 ω) (hω : ∀ ⦃s t : T⦄, s ≤ t → ω.toFun s t ≠ ⊤) : ∃ (I : T → T → E), (∀ ⦃s u t : T⦄, s ≤ u → u ≤ t → I s u + I u t = I s t) ∧ (∀ ⦃s t : T⦄, s ≤ t → ‖I s t - Ξ s t‖ₑ ≤ sewingConst θ * ω.toFun s t ^ θ) ∧ ∀ ⦃s t : T⦄, s ≤ t → ∀ (ε : ENNReal) (mid : List T), List.IsChain (fun (a b : T) => a ≤ b ∧ ω.toFun a b ≤ ε) (s :: (mid ++ [t])) → ‖I s t - pairSum Ξ (s :: (mid ++ [t]))‖ₑ ≤ sewingConst θ * (ε ^ (θ - 1) * ω.toFun s t)

The additive sewing lemma (Friz–Hairer Lemma 4.2, additive form): there is an additive two-parameter primitive I with the germ bound ‖I s t − Ξ s t‖ₑ ≤ K·ω(s,t)^θ, and I s t approximates the Riemann sum of every ε-fine partition to within K·ε^{θ−1}·ω(s,t).