A genuine singular-kernel Volterra convolution on continuous Banach-valued paths.

noncomputable def EulerVolterraConvolution.extendPath {Y : Type u_2} [NormedAddCommGroup Y] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), Y)) (t : ℝ) : Y

Continuous extension of a compact-interval path by clamping its time argument.

Equations

• EulerVolterraConvolution.extendPath T hT f t = f (Set.projIcc 0 T hT t)

theorem EulerVolterraConvolution.extendPath_continuous {Y : Type u_2} [NormedAddCommGroup Y] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), Y)) : Continuous (extendPath T hT f)

The clamped extension of a continuous path is continuous.

theorem EulerVolterraConvolution.extendPath_norm_le {Y : Type u_2} [NormedAddCommGroup Y] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), Y)) (t : ℝ) : ‖extendPath T hT f t‖ ≤ ‖f‖

The clamped extension is bounded by the actual uniform path norm.

noncomputable def EulerVolterraConvolution.causalIntegrand {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : ℝ) (hT : 0 ≤ T) (K : ℝ → Y →L[ℝ] X) (f : C(↑(Set.Icc 0 T), Y)) (t : ↑(Set.Icc 0 T)) (r : ℝ) : X

The fixed-domain integrand for a causal, possibly singular, time convolution.

Equations

• EulerVolterraConvolution.causalIntegrand T hT K f t r = (Set.Iic ↑t).indicator (fun (r : ℝ) => (K r) (EulerVolterraConvolution.extendPath T hT f (↑t - r))) r

theorem EulerVolterraConvolution.causalIntegrand_measurable {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : ℝ) (hT : 0 ≤ T) (K : ℝ → Y →L[ℝ] X) (hK : ContinuousOn (fun (p : ℝ × Y) => (K p.1) p.2) (Set.Ioi 0 ×ˢ Set.univ)) (f : C(↑(Set.Icc 0 T), Y)) (t : ↑(Set.Icc 0 T)) : MeasureTheory.AEStronglyMeasurable (causalIntegrand T hT K f t) (MeasureTheory.volume.restrict (Set.Ioc 0 T))

The translated path integrand is measurable despite the possible kernel singularity at zero.

theorem EulerVolterraConvolution.causalIntegrand_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 : ℝ → ℝ) (hk0 : ∀ r ∈ Set.Ioc 0 T, 0 ≤ k r) (hbound : ∀ r ∈ Set.Ioc 0 T, ∀ (y : Y), ‖(K r) y‖ ≤ k r * ‖y‖) (f : C(↑(Set.Icc 0 T), Y)) (t : ↑(Set.Icc 0 T)) (r : ℝ) (hr : r ∈ Set.Ioc 0 T) : ‖causalIntegrand T hT K f t r‖ ≤ k r * ‖f‖

The causal integrand is bounded by an integrable scalar kernel times the path norm.

theorem EulerVolterraConvolution.causalIntegrand_integrable {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 : C(↑(Set.Icc 0 T), Y)) (t : ↑(Set.Icc 0 T)) : MeasureTheory.Integrable (causalIntegrand T hT K f t) (MeasureTheory.volume.restrict (Set.Ioc 0 T))

The actual causal kernel integral is a Bochner-integrable Banach-valued function.

theorem EulerVolterraConvolution.causalIntegrand_continuousAt {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : ℝ) (hT : 0 ≤ T) (K : ℝ → Y →L[ℝ] X) (f : C(↑(Set.Icc 0 T), Y)) (t : ↑(Set.Icc 0 T)) (r : ℝ) (hr : r ≠ ↑t) : ContinuousAt (fun (s : ↑(Set.Icc 0 T)) => causalIntegrand T hT K f s r) t

Away from the moving upper endpoint, the causal integrand is continuous in time.

theorem EulerVolterraConvolution.causalIntegral_continuous {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 : C(↑(Set.Icc 0 T), Y)) : Continuous fun (t : ↑(Set.Icc 0 T)) => ∫ (r : ℝ) in Set.Ioc 0 T, causalIntegrand T hT K f t r

Dominated convergence proves continuity of the actual singular causal integral.

noncomputable def EulerVolterraConvolution.convolution {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 : C(↑(Set.Icc 0 T), Y)) : C(↑(Set.Icc 0 T), X)

The actual causal convolution as a continuous path.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerVolterraConvolution.kernelMass (T : ℝ) (k : ℝ → ℝ) : ℝ

The scalar mass of an integrable time-kernel bound on the chosen time interval.

Equations

• EulerVolterraConvolution.kernelMass T k = ∫ (r : ℝ) in Set.Ioc 0 T, k r

theorem EulerVolterraConvolution.kernelMass_nonneg (T : ℝ) (k : ℝ → ℝ) (hk0 : ∀ r ∈ Set.Ioc 0 T, 0 ≤ k r) : 0 ≤ kernelMass T k

A nonnegative kernel has nonnegative mass.

theorem EulerVolterraConvolution.convolution_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 : C(↑(Set.Icc 0 T), Y)) : ‖convolution T hT K k hK hk hk0 hbound f‖ ≤ kernelMass T k * ‖f‖

The actual time convolution has the sharp path-norm estimate by the kernel mass.

theorem EulerVolterraConvolution.convolution_eq_interval {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 : C(↑(Set.Icc 0 T), Y)) (t : ↑(Set.Icc 0 T)) : (convolution T hT K k hK hk hk0 hbound f) t = ∫ (r : ℝ) in 0..↑t, (K r) (extendPath T hT f (↑t - r))

The fixed-domain causal integral equals the usual shifted Duhamel interval integral.