Uniqueness of the additive sewing

Any two additive two-parameter maps with a germ bound C·ω^θ, θ > 1, agree (telescoping over fine partitions). Consequently the additive sewing of RoughPaths.Sewing.sewing is unique.

theorem RoughPaths.Sewing.pairSum_eq_of_additive {T : Type u} {E : Type v} [LinearOrder T] [AddCommMonoid E] {I : T → T → E} (hadd : ∀ ⦃a u b : T⦄, a ≤ u → u ≤ b → I a u + I u b = I a b) {mid : List T} {s t : T} : List.IsChain (fun (x1 x2 : T) => x1 ≤ x2) (s :: (mid ++ [t])) → pairSum (fun (a b : T) => I a b) (s :: (mid ++ [t])) = I s t

Pair sums of an additive two-parameter map telescope.

theorem RoughPaths.Sewing.enorm_pairSum_le {T : Type u} {E : Type v} [Preorder T] [NormedAddCommGroup E] (h : T → T → E) (l : List T) : ‖pairSum h l‖ₑ ≤ pairSum (fun (a b : T) => ‖h a b‖ₑ) l

The extended norm of a pair sum is at most the pair sum of the extended norms.

theorem RoughPaths.Sewing.pairSum_le_pairSum_of_chain {T : Type u} [Preorder T] {h₁ h₂ : T → T → ENNReal} (hle : ∀ ⦃a b : T⦄, a ≤ b → h₁ a b ≤ h₂ a b) {l : List T} : List.IsChain (fun (x1 x2 : T) => x1 ≤ x2) l → pairSum h₁ l ≤ pairSum h₂ l

Pair sums are monotone in the summand along a chain.

theorem RoughPaths.Sewing.pairSum_const_mul {T : Type u} [Preorder T] (C : ENNReal) (h : T → T → ENNReal) (l : List T) : pairSum (fun (a b : T) => C * h a b) l = C * pairSum h l

Constants pull out of pair sums.

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

Uniqueness of the additive sewing: two additive maps with germ bounds C·ω^θ, C'·ω^θ, θ > 1, agree on comparable pairs.