Young integration

For f an α-Hölder family of operators and g a β-Hölder path with α + β > 1, the germ Ξ s t = f s (g t − g s) sews into an additive Young integral ∫ f dg with the Young–Loève estimate ‖∫_s^t f dg − f s (g t − g s)‖ₑ ≤ K·Cf·Cg·(t−s)^{α+β}, characterised as the limit of Riemann sums along any mesh-fine sequence of partitions, and unique among additive maps with such a germ bound.

noncomputable def RoughPaths.youngGerm {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : ℝ → E →L[ℝ] F) (g : ℝ → E) : ℝ → ℝ → F

The Young germ Ξ s t = f s (g t − g s).

Equations

• RoughPaths.youngGerm f g s t = (f s) (g t - g s)

@[simp]

theorem RoughPaths.youngGerm_apply {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : ℝ → E →L[ℝ] F) (g : ℝ → E) (s t : ℝ) : youngGerm f g s t = (f s) (g t - g s)

noncomputable def RoughPaths.youngControl (Cf Cg : NNReal) (θ : ℝ) : Control ℝ

The Young control: linear with rate (Cf·Cg)^{1/(α+β)}.

Equations

• RoughPaths.youngControl Cf Cg θ = RoughPaths.Control.ofReal ((↑Cf * ↑Cg) ^ (1 / θ))

theorem RoughPaths.youngControl_ne_top {Cf Cg : NNReal} {θ : ℝ} (hθ : 0 < θ) {s t : ℝ} : (youngControl Cf Cg θ).toFun s t ≠ ⊤

theorem RoughPaths.youngControl_hasFinePartitions {Cf Cg : NNReal} {θ : ℝ} (hθ : 0 < θ) : Sewing.HasFinePartitions (youngControl Cf Cg θ)

theorem RoughPaths.youngControl_rpow {Cf Cg : NNReal} {θ : ℝ} (hθ : 0 < θ) (s t : ℝ) : (youngControl Cf Cg θ).toFun s t ^ θ = ↑Cf * ↑Cg * ENNReal.ofReal (t - s) ^ θ

The θ-th power of the Young control in closed form.

theorem RoughPaths.youngGerm_defect {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → E →L[ℝ] F} {g : ℝ → E} {Cf Cg α β : NNReal} (hf : HolderWith Cf α f) (hg : HolderWith Cg β g) (hα : 0 < α) (hβ : 0 < β) ⦃a b c : ℝ⦄ : a ≤ b → b ≤ c → ‖youngGerm f g a c - youngGerm f g a b - youngGerm f g b c‖ₑ ≤ (youngControl Cf Cg (↑α + ↑β)).toFun a c ^ (↑α + ↑β)

The Chen defect of the Young germ: δΞ a b c = (f a − f b)(g c − g b) is bounded by the Young control to the power θ = α + β.

theorem RoughPaths.exists_youngIntegral {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : ℝ → E →L[ℝ] F} {g : ℝ → E} {Cf Cg α β : NNReal} (hf : HolderWith Cf α f) (hg : HolderWith Cg β g) (hα : 0 < α) (hβ : 0 < β) (hθ : 1 < ↑α + ↑β) : ∃ (I : ℝ → ℝ → F), (∀ ⦃s u t : ℝ⦄, s ≤ u → u ≤ t → I s u + I u t = I s t) ∧ (∀ ⦃s t : ℝ⦄, s ≤ t → ‖I s t - (f s) (g t - g s)‖ₑ ≤ Sewing.sewingConst (↑α + ↑β) * (↑Cf * ↑Cg * ENNReal.ofReal (t - s) ^ (↑α + ↑β))) ∧ ∀ ⦃s t : ℝ⦄, s ≤ t → ∀ (ε : ENNReal) (mid : List ℝ), List.IsChain (fun (a b : ℝ) => a ≤ b ∧ (youngControl Cf Cg (↑α + ↑β)).toFun a b ≤ ε) (s :: (mid ++ [t])) → ‖I s t - Sewing.pairSum (youngGerm f g) (s :: (mid ++ [t]))‖ₑ ≤ Sewing.sewingConst (↑α + ↑β) * (ε ^ (↑α + ↑β - 1) * (youngControl Cf Cg (↑α + ↑β)).toFun s t)

Existence of the Young integral (Young 1936; Lyons–Caruana–Lévy Ch. 1): an additive I with the Young–Loève bound ‖I s t − f s (g t − g s)‖ₑ ≤ K·Cf·Cg·(t−s)^{α+β}, approximating the Riemann sums of every fine partition.

theorem RoughPaths.youngIntegral_unique {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → E →L[ℝ] F} {g : ℝ → E} {Cf Cg α β : NNReal} (hθ : 1 < ↑α + ↑β) {C C' : ENNReal} (hC : C ≠ ⊤) (hC' : C' ≠ ⊤) {I I' : ℝ → ℝ → F} (hadd : ∀ ⦃a u b : ℝ⦄, a ≤ u → u ≤ b → I a u + I u b = I a b) (hadd' : ∀ ⦃a u b : ℝ⦄, a ≤ u → u ≤ b → I' a u + I' u b = I' a b) (hI : ∀ ⦃a b : ℝ⦄, a ≤ b → ‖I a b - youngGerm f g a b‖ₑ ≤ C * (youngControl Cf Cg (↑α + ↑β)).toFun a b ^ (↑α + ↑β)) (hI' : ∀ ⦃a b : ℝ⦄, a ≤ b → ‖I' a b - youngGerm f g a b‖ₑ ≤ C' * (youngControl Cf Cg (↑α + ↑β)).toFun a b ^ (↑α + ↑β)) {s t : ℝ} (hst : s ≤ t) : I s t = I' s t

Uniqueness of the Young integral among additive maps with a Young–Loève-type germ bound.