Spatial restriction of joint derivatives, preserving all primitive bounds.

noncomputable def AVenhance.Infra.Section4.amnrRestrictState {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : (ℝ × E →L[ℝ] F) →L[ℝ] E →L[ℝ] F

Restrict a joint time-state operator to state directions.

Equations

• AVenhance.Infra.Section4.amnrRestrictState = { toFun := fun (A : ℝ × E →L[ℝ] F) => A ∘SL ContinuousLinearMap.inr ℝ ℝ E, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

theorem AVenhance.Infra.Section4.amnrRestrictState_norm_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : ‖amnrRestrictState‖ ≤ 1

Restricting to state directions has unit operator cost.

noncomputable def AVenhance.Infra.Section4.amnrStateDerivative {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : ℝ × E → F) (z : ℝ × E) : E →L[ℝ] F

The actual state derivative of a joint primitive field.

Equations

• AVenhance.Infra.Section4.amnrStateDerivative f z = AVenhance.Infra.Section4.amnrRestrictState (fderiv ℝ f z)

theorem AVenhance.Infra.Section4.amnrStateDerivative_contDiff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (amnrStateDerivative f)

The actual state derivative retains all joint smoothness.

theorem AVenhance.Infra.Section4.amnrStateDerivative_iteratedFDeriv_norm_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) {C : ℝ} (hbound : ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ (n + 1) f z‖ ≤ C) (z : ℝ × E) : ‖iteratedFDeriv ℝ n (amnrStateDerivative f) z‖ ≤ C

Every next derivative of the primitive field supplies the corresponding operator bound for its actual state derivative.