Sewing with a constant-scaled control

The additive sewing lemma packaged for germs whose defect is bounded by C·ω^θ: the scaling constant is absorbed into the control, so all three rough-integral constructions (word, branched, planarly branched) reduce to one application.

theorem RoughPaths.Sewing.sewing_const_mul {T : Type u_1} [LinearOrder T] {E : Type u_2} [NormedAddCommGroup E] [CompleteSpace E] (ω : Control T) (Ξ : T → T → E) {θ : ℝ} {C : ENNReal} (hθ : 1 < θ) (hθ0 : θ ≠ 0) (hC : C ≠ ⊤) (hδ : ∀ ⦃a b c : T⦄, a ≤ b → b ≤ c → ‖Ξ a c - Ξ a b - Ξ b c‖ₑ ≤ 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 θ * (C * ω.toFun s t ^ θ)) ∧ ∀ ⦃s t : T⦄, s ≤ t → ∀ (ε : ENNReal) (mid : List T), List.IsChain (fun (a b : T) => a ≤ b ∧ (Control.constMul (C ^ θ⁻¹) ω).toFun a b ≤ ε) (s :: (mid ++ [t])) → ‖I s t - pairSum Ξ (s :: (mid ++ [t]))‖ₑ ≤ sewingConst θ * (ε ^ (θ - 1) * (Control.constMul (C ^ θ⁻¹) ω).toFun s t)

Scaled sewing: a germ with defect bound C·ω^θ, θ > 1, sews into an additive primitive with the correspondingly scaled estimates.