Differentiation of an actual field acting on continuous trajectories.

theorem AVenhance.Infra.Section4.amnr_hasFDerivAt_of_quadratic_remainder {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {x : E} (L : E →L[ℝ] F) {C : ℝ} (hC : 0 ≤ C) (hrem : ∀ (h : E), ‖f (x + h) - f x - L h‖ ≤ C * ‖h‖ * ‖h‖) : HasFDerivAt f L x

A uniform quadratic remainder gives the actual Frechet derivative. This helper applies to the Banach space of continuous trajectories as well as to the finite-dimensional source field.

def AVenhance.Infra.Section4.amnrCurveDerivative {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (D : K → E → E →L[ℝ] F) (hD : Continuous fun (z : K × E) => D z.1 z.2) (u : C(K, E)) : C(K, E →L[ℝ] F)

Applying the primitive field derivative along a continuous curve gives an actual continuous operator curve.

Equations

• AVenhance.Infra.Section4.amnrCurveDerivative D hD u = { toFun := fun (t : K) => D t (u t), continuous_toFun := ⋯ }

theorem AVenhance.Infra.Section4.amnrCurveCompose_hasFDerivAt {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : K → E → F) (hf : Continuous fun (z : K × E) => f z.1 z.2) (D : K → E → E →L[ℝ] F) (hD : Continuous fun (z : K × E) => D z.1 z.2) {C : ℝ} (hC : 0 ≤ C) (hTaylor : ∀ (t : K) (x h : E), ‖f t (x + h) - f t x - (D t x) h‖ ≤ C * ‖h‖ * ‖h‖) (u : C(K, E)) : HasFDerivAt (amnrCurveCompose f hf) (amnrCurveOperator (amnrCurveDerivative D hD u)) u

A uniform primitive Taylor estimate differentiates the actual composition operator on the whole continuous-trajectory space.