Actual composition and adjoint calculus on continuous paths

The pointwise operator operations are built from bounded maps in the uniform norm. Their regularity and factorial bounds are consequently genuine derivative statements in that norm.

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition1 {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup (E →L[ℝ] F)

Cache the standard NormedAddCommGroup (E →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition1 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition2 {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ (E →L[ℝ] F)

Cache the standard NormedSpace ℝ (E →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition2 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition3 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] : NormedAddCommGroup (U →L[ℝ] E)

Cache the standard NormedAddCommGroup (U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition3 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition4 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] : NormedSpace ℝ (U →L[ℝ] E)

Cache the standard NormedSpace ℝ (U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition4 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition5 {U : Type u_2} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup (U →L[ℝ] F)

Cache the standard NormedAddCommGroup (U →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition5 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition6 {U : Type u_2} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ (U →L[ℝ] F)

Cache the standard NormedSpace ℝ (U →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition6 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition7 {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup ((U →L[ℝ] E) →L[ℝ] U →L[ℝ] F)

Cache the standard NormedAddCommGroup ((U →L[ℝ] E) →L[ℝ] U →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition7 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition8 {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ ((U →L[ℝ] E) →L[ℝ] U →L[ℝ] F)

Cache the standard NormedSpace ℝ ((U →L[ℝ] E) →L[ℝ] U →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition8 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition9 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup C(K, E →L[ℝ] F)

Cache the standard NormedAddCommGroup C(K,E →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition9 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition10 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ C(K, E →L[ℝ] F)

Cache the standard NormedSpace ℝ C(K,E →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition10 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition11 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] : NormedAddCommGroup C(K, U →L[ℝ] E)

Cache the standard NormedAddCommGroup C(K,U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition11 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition12 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] : NormedSpace ℝ C(K, U →L[ℝ] E)

Cache the standard NormedSpace ℝ C(K,U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition12 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition13 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup C(K, U →L[ℝ] F)

Cache the standard NormedAddCommGroup C(K,U →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition13 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition14 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ C(K, U →L[ℝ] F)

Cache the standard NormedSpace ℝ C(K,U →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition14 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition15 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup C(K, (U →L[ℝ] E) →L[ℝ] U →L[ℝ] F)

Cache the standard NormedAddCommGroup C(K,(U →L[ℝ] E) →L[ℝ] U →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition15 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition16 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ C(K, (U →L[ℝ] E) →L[ℝ] U →L[ℝ] F)

Cache the standard NormedSpace ℝ C(K,(U →L[ℝ] E) →L[ℝ] U →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition16 = inferInstance

theorem EulerContinuousPathComposition.postcomposition_norm {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : E →L[ℝ] F) : ‖ContinuousLinearMap.compLeftContinuous ℝ K A‖ ≤ ‖A‖

A fixed bounded map acts pointwise on continuous paths with the same norm bound.

noncomputable def EulerContinuousPathComposition.compositionLift {K : Type u_1} [TopologicalSpace K] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : C(K, E →L[ℝ] F) →L[ℝ] C(K, (U →L[ℝ] E) →L[ℝ] U →L[ℝ] F)

Lift the actual operator composition bilinear map to the coefficient path.

Equations

• EulerContinuousPathComposition.compositionLift = ContinuousLinearMap.compLeftContinuous ℝ K (ContinuousLinearMap.compL ℝ U E F)

theorem EulerContinuousPathComposition.compositionLift_norm {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : ‖compositionLift‖ ≤ 1

noncomputable def EulerContinuousPathComposition.compose {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : C(K, E →L[ℝ] F)) (B : C(K, U →L[ℝ] E)) : C(K, U →L[ℝ] F)

Literal pointwise composition of two continuous coefficient paths.

Equations

• EulerContinuousPathComposition.compose A B = (EulerContinuousTimeIntegral.multiplier (EulerContinuousPathComposition.compositionLift A)) B

@[simp]

theorem EulerContinuousPathComposition.compose_apply {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : C(K, E →L[ℝ] F)) (B : C(K, U →L[ℝ] E)) (t : K) : (compose A B) t = A t ∘SL B t

theorem EulerContinuousPathComposition.contDiff_compose {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → C(K, E →L[ℝ] F)) (B : P → C(K, U →L[ℝ] E)) {n : WithTop ℕ∞} (hA : ContDiff ℝ n A) (hB : ContDiff ℝ n B) : ContDiff ℝ n fun (x : P) => compose (A x) (B x)

Actual uniform-norm smoothness of pointwise composition.

theorem EulerContinuousPathComposition.compose_bound {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → C(K, E →L[ℝ] F)) (B : P → C(K, U →L[ℝ] E)) (hA : ContDiff ℝ (↑⊤) A) (hB : ContDiff ℝ (↑⊤) B) (R C D : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) (c d : ℕ) (hbA : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n A x‖ ≤ C * EulerGevrey.majorant R c n) (hbB : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n B x‖ ≤ D * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => compose (A y) (B y)) x‖ ≤ 3 * C * D * EulerGevrey.majorant R (c + d) n

Pointwise composition has the same fixed factorial product constant.

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition17 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (U →L[ℝ] E)

Cache the standard NormedAddCommGroup (U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition17 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition18 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (U →L[ℝ] E)

Cache the standard NormedSpace ℝ (U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition18 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition19 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (E →L[ℝ] U)

Cache the standard NormedAddCommGroup (E →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition19 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition20 {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (E →L[ℝ] U)

Cache the standard NormedSpace ℝ (E →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition20 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition21 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup C(K, U →L[ℝ] E)

Cache the standard NormedAddCommGroup C(K,U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition21 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition22 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ C(K, U →L[ℝ] E)

Cache the standard NormedSpace ℝ C(K,U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition22 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition23 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup C(K, E →L[ℝ] U)

Cache the standard NormedAddCommGroup C(K,E →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition23 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathComposition.instContinuousPathComposition24 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ C(K, E →L[ℝ] U)

Cache the standard NormedSpace ℝ C(K,E →L[ℝ] U) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathComposition.instContinuousPathComposition24 = inferInstance

noncomputable def EulerContinuousPathComposition.adjointMap {K : Type u_1} [TopologicalSpace K] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : C(K, U →L[ℝ] E) →L[ℝ] C(K, E →L[ℝ] U)

Actual adjoint at every parameter in the compact path domain.

Equations

• EulerContinuousPathComposition.adjointMap = ContinuousLinearMap.compLeftContinuous ℝ K EulerTransverseGramInverse.realAdjoint

@[simp]

theorem EulerContinuousPathComposition.adjointMap_apply {K : Type u_1} [TopologicalSpace K] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (A : C(K, U →L[ℝ] E)) (t : K) : (adjointMap A) t = ContinuousLinearMap.adjoint (A t)

theorem EulerContinuousPathComposition.adjointMap_norm {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : ‖adjointMap‖ ≤ 1

theorem EulerContinuousPathComposition.contDiff_adjoint {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → C(K, U →L[ℝ] E)) {n : WithTop ℕ∞} (hA : ContDiff ℝ n A) : ContDiff ℝ n fun (x : P) => adjointMap (A x)

theorem EulerContinuousPathComposition.adjoint_bound {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → C(K, U →L[ℝ] E)) (hA : ContDiff ℝ (↑⊤) A) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (d : ℕ) (hb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n A x‖ ≤ C * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => adjointMap (A y)) x‖ ≤ C * EulerGevrey.majorant R d n