Bounded operators on continuous time paths

The multiplier and initial integral are actual continuous linear maps. The primitive has the prescribed derivative, including the one-sided endpoint statements, and the uniform bound is exactly the interval length.

noncomputable def EulerContinuousTimeIntegral.multiplierLinear {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : C(K, E →L[ℝ] F)) : C(K, E) →ₗ[ℝ] C(K, F)

Pointwise multiplication by an operator-valued continuous path.

Equations

• EulerContinuousTimeIntegral.multiplierLinear A = { toFun := fun (f : C(K, E)) => { toFun := fun (t : K) => (A t) (f t), continuous_toFun := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

theorem EulerContinuousTimeIntegral.multiplierLinear_bound {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : C(K, E →L[ℝ] F)) (f : C(K, E)) : ‖(multiplierLinear A) f‖ ≤ ‖A‖ * ‖f‖

The multiplier has the literal coefficient bound.

noncomputable def EulerContinuousTimeIntegral.multiplier {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : C(K, E →L[ℝ] F)) : C(K, E) →L[ℝ] C(K, F)

The genuine bounded multiplier on continuous time paths.

Equations

• EulerContinuousTimeIntegral.multiplier A = (EulerContinuousTimeIntegral.multiplierLinear A).mkContinuous ‖A‖ ⋯

@[simp]

theorem EulerContinuousTimeIntegral.multiplier_apply {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : C(K, E →L[ℝ] F)) (f : C(K, E)) (t : K) : ((multiplier A) f) t = (A t) (f t)

theorem EulerContinuousTimeIntegral.multiplier_norm {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : C(K, E →L[ℝ] F)) : ‖multiplier A‖ ≤ ‖A‖

No derivative-dependent loss enters continuous path multiplication.

noncomputable def EulerContinuousTimeIntegral.realIntegral {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), E)) : ℝ → E

The literal zero-initial-time integral.

Equations

• EulerContinuousTimeIntegral.realIntegral T hT f t = ∫ (s : ℝ) in 0..t, EulerVolterraConvolution.extendPath T hT f s

theorem EulerContinuousTimeIntegral.realIntegral_hasDerivAt {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), E)) (t : ℝ) : HasDerivAt (realIntegral T hT f) (EulerVolterraConvolution.extendPath T hT f t) t

The integral has the actual classical derivative.

noncomputable def EulerContinuousTimeIntegral.integralLinear {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) : C(↑(Set.Icc 0 T), E) →ₗ[ℝ] C(↑(Set.Icc 0 T), E)

The actual integral is a continuous time path.

Equations

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

theorem EulerContinuousTimeIntegral.integralLinear_bound {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), E)) : ‖(integralLinear T hT) f‖ ≤ T * ‖f‖

The uniform norm of the primitive is bounded by time length times the input norm.

noncomputable def EulerContinuousTimeIntegral.integral {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) : C(↑(Set.Icc 0 T), E) →L[ℝ] C(↑(Set.Icc 0 T), E)

The zero-initial-time integral as a bounded linear operator.

Equations

• EulerContinuousTimeIntegral.integral T hT = (EulerContinuousTimeIntegral.integralLinear T hT).mkContinuous T ⋯

@[simp]

theorem EulerContinuousTimeIntegral.integral_apply {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), E)) (t : ↑(Set.Icc 0 T)) : ((integral T hT) f) t = realIntegral T hT f ↑t

theorem EulerContinuousTimeIntegral.integral_norm {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) : ‖integral T hT‖ ≤ T

The exact operator bound for the initial primitive.

theorem EulerContinuousTimeIntegral.integral_initial {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), E)) : ((integral T hT) f) ⟨0, ⋯⟩ = 0

theorem EulerContinuousTimeIntegral.integral_hasDerivWithinAt {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), E)) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT ((integral T hT) f)) (f t) (Set.Icc 0 T) ↑t

The primitive has the prescribed within-interval derivative at every time.

theorem EulerContinuousTimeIntegral.eq_initial_add_integral {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), E)) (a : ℝ → E) (ha : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt a (f t) (Set.Icc 0 T) ↑t) (t : ↑(Set.Icc 0 T)) : a ↑t = a 0 + ((integral T hT) f) t

A path with this derivative is its initial value plus the actual integral.