Banach's theorem applied to the actual singular Volterra integral on continuous paths.

theorem EulerVolterraConvolution.convolution_sub {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : ℝ) (hT : 0 ≤ T) (K : ℝ → Y →L[ℝ] X) (k : ℝ → ℝ) (hK : ContinuousOn (fun (p : ℝ × Y) => (K p.1) p.2) (Set.Ioi 0 ×ˢ Set.univ)) (hk : MeasureTheory.IntegrableOn k (Set.Ioc 0 T) MeasureTheory.volume) (hk0 : ∀ r ∈ Set.Ioc 0 T, 0 ≤ k r) (hbound : ∀ r ∈ Set.Ioc 0 T, ∀ (y : Y), ‖(K r) y‖ ≤ k r * ‖y‖) (f g : C(↑(Set.Icc 0 T), Y)) : convolution T hT K k hK hk hk0 hbound (f - g) = convolution T hT K k hK hk hk0 hbound f - convolution T hT K k hK hk hk0 hbound g

The actual Bochner convolution commutes with subtraction of continuous paths.

theorem EulerVolterraConvolution.convolution_sub_bound {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : ℝ) (hT : 0 ≤ T) (K : ℝ → Y →L[ℝ] X) (k : ℝ → ℝ) (hK : ContinuousOn (fun (p : ℝ × Y) => (K p.1) p.2) (Set.Ioi 0 ×ˢ Set.univ)) (hk : MeasureTheory.IntegrableOn k (Set.Ioc 0 T) MeasureTheory.volume) (hk0 : ∀ r ∈ Set.Ioc 0 T, 0 ≤ k r) (hbound : ∀ r ∈ Set.Ioc 0 T, ∀ (y : Y), ‖(K r) y‖ ≤ k r * ‖y‖) (f g : C(↑(Set.Icc 0 T), Y)) : ‖convolution T hT K k hK hk hk0 hbound f - convolution T hT K k hK hk hk0 hbound g‖ ≤ kernelMass T k * ‖f - g‖

The actual convolution is Lipschitz with constant equal to its scalar kernel mass.

def EulerVolterraConvolution.pathNonlinearity {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedAddCommGroup Y] (T : ℝ) (F : ↑(Set.Icc 0 T) → X → Y) (hF : Continuous fun (p : ↑(Set.Icc 0 T) × X) => F p.1 p.2) (u : C(↑(Set.Icc 0 T), X)) : C(↑(Set.Icc 0 T), Y)

Pointwise application of an actual continuous time-dependent nonlinearity to a path.

Equations

• EulerVolterraConvolution.pathNonlinearity T F hF u = { toFun := fun (t : ↑(Set.Icc 0 T)) => F t (u t), continuous_toFun := ⋯ }

theorem EulerVolterraConvolution.pathNonlinearity_bound {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedAddCommGroup Y] (T : ℝ) (F : ↑(Set.Icc 0 T) → X → Y) (hF : Continuous fun (p : ↑(Set.Icc 0 T) × X) => F p.1 p.2) (R M : ℝ) (hM : 0 ≤ M) (hFM : ∀ (t : ↑(Set.Icc 0 T)) (x : X), ‖x‖ ≤ R → ‖F t x‖ ≤ M) (u : C(↑(Set.Icc 0 T), X)) (hu : ‖u‖ ≤ R) : ‖pathNonlinearity T F hF u‖ ≤ M

The pointwise nonlinear bound on a ball gives the same bound on continuous paths.

theorem EulerVolterraConvolution.pathNonlinearity_sub_bound {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedAddCommGroup Y] (T : ℝ) (F : ↑(Set.Icc 0 T) → X → Y) (hF : Continuous fun (p : ↑(Set.Icc 0 T) × X) => F p.1 p.2) (R L : ℝ) (hL : 0 ≤ L) (hFL : ∀ (t : ↑(Set.Icc 0 T)) (x y : X), ‖x‖ ≤ R → ‖y‖ ≤ R → ‖F t x - F t y‖ ≤ L * ‖x - y‖) (u v : C(↑(Set.Icc 0 T), X)) (hu : ‖u‖ ≤ R) (hv : ‖v‖ ≤ R) : ‖pathNonlinearity T F hF u - pathNonlinearity T F hF v‖ ≤ L * ‖u - v‖

A local Lipschitz nonlinearity induces the same local Lipschitz bound on path space.

noncomputable def EulerVolterraConvolution.picard {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : ℝ) (hT : 0 ≤ T) (K : ℝ → Y →L[ℝ] X) (k : ℝ → ℝ) (hK : ContinuousOn (fun (p : ℝ × Y) => (K p.1) p.2) (Set.Ioi 0 ×ˢ Set.univ)) (hk : MeasureTheory.IntegrableOn k (Set.Ioc 0 T) MeasureTheory.volume) (hk0 : ∀ r ∈ Set.Ioc 0 T, 0 ≤ k r) (hbound : ∀ r ∈ Set.Ioc 0 T, ∀ (y : Y), ‖(K r) y‖ ≤ k r * ‖y‖) (a : C(↑(Set.Icc 0 T), X)) (F : ↑(Set.Icc 0 T) → X → Y) (hF : Continuous fun (p : ↑(Set.Icc 0 T) × X) => F p.1 p.2) (u : C(↑(Set.Icc 0 T), X)) : C(↑(Set.Icc 0 T), X)

The actual nonlinear Volterra map, including the prescribed free evolution.

Equations

• EulerVolterraConvolution.picard T hT K k hK hk hk0 hbound a F hF u = a + EulerVolterraConvolution.convolution T hT K k hK hk hk0 hbound (EulerVolterraConvolution.pathNonlinearity T F hF u)

theorem EulerVolterraConvolution.picard_bound {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : ℝ) (hT : 0 ≤ T) (K : ℝ → Y →L[ℝ] X) (k : ℝ → ℝ) (hK : ContinuousOn (fun (p : ℝ × Y) => (K p.1) p.2) (Set.Ioi 0 ×ˢ Set.univ)) (hk : MeasureTheory.IntegrableOn k (Set.Ioc 0 T) MeasureTheory.volume) (hk0 : ∀ r ∈ Set.Ioc 0 T, 0 ≤ k r) (hbound : ∀ r ∈ Set.Ioc 0 T, ∀ (y : Y), ‖(K r) y‖ ≤ k r * ‖y‖) (a : C(↑(Set.Icc 0 T), X)) (F : ↑(Set.Icc 0 T) → X → Y) (hF : Continuous fun (p : ↑(Set.Icc 0 T) × X) => F p.1 p.2) (R M : ℝ) (hM : 0 ≤ M) (hFM : ∀ (t : ↑(Set.Icc 0 T)) (x : X), ‖x‖ ≤ R → ‖F t x‖ ≤ M) (hbudget : ‖a‖ + kernelMass T k * M ≤ R) (u : C(↑(Set.Icc 0 T), X)) (hu : ‖u‖ ≤ R) : ‖picard T hT K k hK hk hk0 hbound a F hF u‖ ≤ R

The genuine Picard map preserves the chosen path ball under the explicit scalar budget.

theorem EulerVolterraConvolution.picard_sub_bound {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : ℝ) (hT : 0 ≤ T) (K : ℝ → Y →L[ℝ] X) (k : ℝ → ℝ) (hK : ContinuousOn (fun (p : ℝ × Y) => (K p.1) p.2) (Set.Ioi 0 ×ˢ Set.univ)) (hk : MeasureTheory.IntegrableOn k (Set.Ioc 0 T) MeasureTheory.volume) (hk0 : ∀ r ∈ Set.Ioc 0 T, 0 ≤ k r) (hbound : ∀ r ∈ Set.Ioc 0 T, ∀ (y : Y), ‖(K r) y‖ ≤ k r * ‖y‖) (a : C(↑(Set.Icc 0 T), X)) (F : ↑(Set.Icc 0 T) → X → Y) (hF : Continuous fun (p : ↑(Set.Icc 0 T) × X) => F p.1 p.2) (R L : ℝ) (hL : 0 ≤ L) (hFL : ∀ (t : ↑(Set.Icc 0 T)) (x y : X), ‖x‖ ≤ R → ‖y‖ ≤ R → ‖F t x - F t y‖ ≤ L * ‖x - y‖) (u v : C(↑(Set.Icc 0 T), X)) (hu : ‖u‖ ≤ R) (hv : ‖v‖ ≤ R) : ‖picard T hT K k hK hk hk0 hbound a F hF u - picard T hT K k hK hk hk0 hbound a F hF v‖ ≤ kernelMass T k * L * ‖u - v‖

The actual Picard map has contraction coefficient equal to kernel mass times nonlinear Lipschitz constant.

theorem EulerVolterraConvolution.exists_mild_solution {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : ℝ) (hT : 0 ≤ T) (K : ℝ → Y →L[ℝ] X) (k : ℝ → ℝ) (hK : ContinuousOn (fun (p : ℝ × Y) => (K p.1) p.2) (Set.Ioi 0 ×ˢ Set.univ)) (hk : MeasureTheory.IntegrableOn k (Set.Ioc 0 T) MeasureTheory.volume) (hk0 : ∀ r ∈ Set.Ioc 0 T, 0 ≤ k r) (hbound : ∀ r ∈ Set.Ioc 0 T, ∀ (y : Y), ‖(K r) y‖ ≤ k r * ‖y‖) [CompleteSpace X] (a : C(↑(Set.Icc 0 T), X)) (F : ↑(Set.Icc 0 T) → X → Y) (hF : Continuous fun (p : ↑(Set.Icc 0 T) × X) => F p.1 p.2) (R M L : ℝ) (hR : 0 ≤ R) (hM : 0 ≤ M) (hL : 0 ≤ L) (hFM : ∀ (t : ↑(Set.Icc 0 T)) (x : X), ‖x‖ ≤ R → ‖F t x‖ ≤ M) (hFL : ∀ (t : ↑(Set.Icc 0 T)) (x y : X), ‖x‖ ≤ R → ‖y‖ ≤ R → ‖F t x - F t y‖ ≤ L * ‖x - y‖) (hbudget : ‖a‖ + kernelMass T k * M ≤ R) (hsmall : kernelMass T k * L < 1) : ∃ (u : C(↑(Set.Icc 0 T), X)), ‖u‖ ≤ R ∧ ∀ (t : ↑(Set.Icc 0 T)), u t = a t + ∫ (r : ℝ) in 0..↑t, (K r) (F (Set.projIcc 0 T hT (↑t - r)) (u (Set.projIcc 0 T hT (↑t - r))))

An actual continuous mild solution exists by contraction of the explicitly defined Volterra integral.