The actual Volterra integral as a bounded operator on compact-time curves.

def AVenhance.Infra.Section4.amnrClampPoint (a b : ℝ) (hab : a ≤ b) (t : ℝ) : ↑(Set.Icc a b)

Extend a compact-interval curve by clamping its time argument.

Equations

• AVenhance.Infra.Section4.amnrClampPoint a b hab t = ⟨max a (min b t), ⋯⟩

def AVenhance.Infra.Section4.amnrExtendCurve {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (hab : a ≤ b) (u : C(↑(Set.Icc a b), E)) : ℝ → E

The actual continuous clamped extension of a trajectory.

Equations

• AVenhance.Infra.Section4.amnrExtendCurve hab u t = u (AVenhance.Infra.Section4.amnrClampPoint a b hab t)

theorem AVenhance.Infra.Section4.amnrExtendCurve_continuous {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (hab : a ≤ b) (u : C(↑(Set.Icc a b), E)) : Continuous (amnrExtendCurve hab u)

Clamping preserves continuity, also at both endpoints.

theorem AVenhance.Infra.Section4.amnrExtendCurve_eq_of_mem {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (hab : a ≤ b) (u : C(↑(Set.Icc a b), E)) {t : ℝ} (ht : t ∈ Set.Icc a b) : amnrExtendCurve hab u t = u ⟨t, ht⟩

The extension agrees with the actual trajectory inside its interval.

noncomputable def AVenhance.Infra.Section4.amnrCurvePrimitive {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (s : ℝ) (u : C(↑(Set.Icc a b), E)) : C(↑(Set.Icc a b), E)

Integrate the actual trajectory from a prescribed start time.

Equations

• AVenhance.Infra.Section4.amnrCurvePrimitive hab s u = { toFun := fun (t : ↑(Set.Icc a b)) => ∫ (r : ℝ) in s..↑t, AVenhance.Infra.Section4.amnrExtendCurve hab u r, continuous_toFun := ⋯ }

theorem AVenhance.Infra.Section4.amnrCurvePrimitive_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b s : ℝ} (hab : a ≤ b) (hs : s ∈ Set.Icc a b) (u : C(↑(Set.Icc a b), E)) : ‖amnrCurvePrimitive hab s u‖ ≤ (b - a) * ‖u‖

The true compact-time integral has the interval-length operator cost.

noncomputable def AVenhance.Infra.Section4.amnrCurveIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (s : ℝ) (hs : s ∈ Set.Icc a b) : C(↑(Set.Icc a b), E) →L[ℝ] C(↑(Set.Icc a b), E)

The Volterra integral is an actual bounded linear operator on curves.

Equations

• AVenhance.Infra.Section4.amnrCurveIntegral hab s hs = { toFun := AVenhance.Infra.Section4.amnrCurvePrimitive hab s, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (b - a) ⋯

theorem AVenhance.Infra.Section4.amnrCurveIntegral_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a ≤ b) (s : ℝ) (hs : s ∈ Set.Icc a b) : ‖amnrCurveIntegral hab s hs‖ ≤ b - a

The actual integral operator has the exact interval-length upper bound.