Curve-space operators for higher flow dependence on the initial point.

def AVenhance.Infra.Section4.amnrCurveApply {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)) (u : C(K, E)) : C(K, F)

Pointwise application of a continuous operator curve to a state curve.

Equations

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

theorem AVenhance.Infra.Section4.amnrCurveApply_norm_le {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)) (u : C(K, E)) : ‖amnrCurveApply A u‖ ≤ ‖A‖ * ‖u‖

Uniform application costs the product of the two actual curve norms.

noncomputable def AVenhance.Infra.Section4.amnrCurveOperator {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 actual operator curve acts as a bounded linear operator on curves.

Equations

• AVenhance.Infra.Section4.amnrCurveOperator A = { toFun := AVenhance.Infra.Section4.amnrCurveApply A, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous ‖A‖ ⋯

@[simp]

theorem AVenhance.Infra.Section4.amnrCurveOperator_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)) (u : C(K, E)) (t : K) : ((amnrCurveOperator A) u) t = (A t) (u t)

theorem AVenhance.Infra.Section4.amnrCurveOperator_norm_le {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)) : ‖amnrCurveOperator A‖ ≤ ‖A‖

No compact-domain cardinality enters the operator bound.

noncomputable def AVenhance.Infra.Section4.amnrCurveOperatorMap {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : C(K, E →L[ℝ] F) →L[ℝ] C(K, E) →L[ℝ] C(K, F)

Taking an operator curve to its curve-space action is itself bounded linear. This will preserve every finite differentiability order.

Equations

• AVenhance.Infra.Section4.amnrCurveOperatorMap = { toFun := fun (A : C(K, E →L[ℝ] F)) => AVenhance.Infra.Section4.amnrCurveOperator A, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

def AVenhance.Infra.Section4.amnrCurveCompose {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [NormedAddCommGroup E] [NormedAddCommGroup F] (f : K → E → F) (hf : Continuous fun (z : K × E) => f z.1 z.2) (u : C(K, E)) : C(K, F)

Composition of a time-dependent field with an actual continuous curve.

Equations

• AVenhance.Infra.Section4.amnrCurveCompose f hf u = { toFun := fun (t : K) => f t (u t), continuous_toFun := ⋯ }