Actual time derivatives of uniformly continuous bounded fields

Pointwise derivatives identify a derivative in the bounded-field norm when both the field and prescribed derivative are continuous in that norm. The proof uses the Bochner fundamental theorem of calculus and bounded evaluation.

theorem EulerBoundedFieldTimeDerivative.integral_eq_sub {X : Type u_1} {W : Type u_2} [TopologicalSpace X] [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] (T : ℝ) (hT : 0 ≤ T) (A A' : C(↑(Set.Icc 0 T), BoundedContinuousFunction X W)) (hpoint : ∀ t ∈ Set.Icc 0 T, ∀ (x : X), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT A s) x) ((EulerVolterraConvolution.extendPath T hT A' t) x) (Set.Icc 0 T) t) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : ∫ (s : ℝ) in 0..t, EulerVolterraConvolution.extendPath T hT A' s = EulerVolterraConvolution.extendPath T hT A t - EulerVolterraConvolution.extendPath T hT A 0

Pointwise derivatives imply the exact integral identity in the bounded-field space.

theorem EulerBoundedFieldTimeDerivative.hasDerivWithinAt {X : Type u_1} {W : Type u_2} [TopologicalSpace X] [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] (T : ℝ) (hT : 0 ≤ T) (A A' : C(↑(Set.Icc 0 T), BoundedContinuousFunction X W)) (hpoint : ∀ t ∈ Set.Icc 0 T, ∀ (x : X), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT A s) x) ((EulerVolterraConvolution.extendPath T hT A' t) x) (Set.Icc 0 T) t) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (EulerVolterraConvolution.extendPath T hT A' t) (Set.Icc 0 T) t

This is a genuine derivative in the uniform bounded-field norm.