The additive sewing lemma: partition comparison

Over a LinearOrder time set, two fine partitions of the same interval have Riemann sums within K·(ε^{θ−1} + ε'^{θ−1})·ω(s,t) of each other: each is compared with their common refinement through ChainRefine. This is the quantitative core of the additive sewing lemma; the limit construction lives in RoughPaths.Sewing.AdditiveLimit.

noncomputable def RoughPaths.Sewing.sewingConst (θ : ℝ) : ENNReal

The sewing constant K(θ) = Σ_j (2/(j+1))^θ.

Equations

• RoughPaths.Sewing.sewingConst θ = ∑' (j : ℕ), (2 / (↑j + 1)) ^ θ

theorem RoughPaths.Sewing.sewingConst_ne_top {θ : ℝ} (hθ : 1 < θ) : sewingConst θ ≠ ⊤

theorem RoughPaths.Sewing.germ_diag_eq_zero {T : Type u} [LinearOrder T] {E : Type v} [NormedAddCommGroup 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 ^ θ) (t : T) : Ξ t t = 0

The germ of a sewing problem vanishes on the diagonal.

theorem RoughPaths.Sewing.chain_mem_bounds {T : Type u} [LinearOrder T] {mid : List T} {x t : T} : List.IsChain (fun (x1 x2 : T) => x1 ≤ x2) (x :: (mid ++ [t])) → ∀ z ∈ x :: (mid ++ [t]), x ≤ z ∧ z ≤ t

Every element of a monotone chain lies between the endpoints.

theorem RoughPaths.Sewing.pairSum_eq_zero_of_const {T : Type u} {E : Type v} [NormedAddCommGroup E] {Ξ : T → T → E} (hdiag : ∀ (t : T), Ξ t t = 0) {l : List T} {t : T} : (∀ z ∈ l, z = t) → pairSum Ξ l = 0

Riemann sums over chains from t to t vanish.

theorem RoughPaths.Sewing.pairSum_sub_pairSum_le_of_refines {T : Type u} [LinearOrder T] {E : Type v} [NormedAddCommGroup E] (ω : Control T) (Ξ : T → T → E) {θ : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : 0 ≤ θ - 1) (hδ : ∀ ⦃a b c : T⦄, a ≤ b → b ≤ c → ‖Ξ a c - Ξ a b - Ξ b c‖ₑ ≤ ω.toFun a c ^ θ) {s t : T} {midp midr : List T} {ε : ENNReal} (hp : List.IsChain (fun (a b : T) => a ≤ b ∧ ω.toFun a b ≤ ε) (s :: (midp ++ [t]))) (hpstrict : List.IsChain (fun (x1 x2 : T) => x1 < x2) (s :: (midp ++ [t]))) (hr : List.IsChain (fun (x1 x2 : T) => x1 < x2) (s :: (midr ++ [t]))) (hsub : ∀ z ∈ s :: (midp ++ [t]), z ∈ s :: (midr ++ [t])) : ‖pairSum Ξ (s :: (midr ++ [t])) - pairSum Ξ (s :: (midp ++ [t]))‖ₑ ≤ sewingConst θ * (ε ^ (θ - 1) * ω.toFun s t)

Refinement comparison: the Riemann sum of a fine chain is close to that of any strict chain refining it.

theorem RoughPaths.Sewing.pairSum_sub_pairSum_le_of_fine {T : Type u} [LinearOrder T] {E : Type v} [NormedAddCommGroup E] (ω : Control T) (Ξ : T → T → E) {θ : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : 0 ≤ θ - 1) (hδ : ∀ ⦃a b c : T⦄, a ≤ b → b ≤ c → ‖Ξ a c - Ξ a b - Ξ b c‖ₑ ≤ ω.toFun a c ^ θ) {s t : T} (hst : s < t) {midp midq : List T} {ε ε' : ENNReal} (hp : List.IsChain (fun (a b : T) => a ≤ b ∧ ω.toFun a b ≤ ε) (s :: (midp ++ [t]))) (hpstrict : List.IsChain (fun (x1 x2 : T) => x1 < x2) (s :: (midp ++ [t]))) (hq : List.IsChain (fun (a b : T) => a ≤ b ∧ ω.toFun a b ≤ ε') (s :: (midq ++ [t]))) (hqstrict : List.IsChain (fun (x1 x2 : T) => x1 < x2) (s :: (midq ++ [t]))) : ‖pairSum Ξ (s :: (midp ++ [t])) - pairSum Ξ (s :: (midq ++ [t]))‖ₑ ≤ sewingConst θ * (ε ^ (θ - 1) * ω.toFun s t) + sewingConst θ * (ε' ^ (θ - 1) * ω.toFun s t)

Mesh comparison of two fine chains via their common refinement.