Genuine coefficient calculus on continuous path spaces

Pointwise multiplication by an operator-valued continuous path depends bounded-linearly on that path. Its operator norm, actual parameter derivatives, and factorial estimates therefore come directly from the coefficient, with no loss in the coefficient amplitude.

@[instance_reducible]

noncomputable def EulerContinuousPathCalculus.instContinuousPathCalculus1 {E : Type u_2} {F : Type u_3} [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

• EulerContinuousPathCalculus.instContinuousPathCalculus1 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathCalculus.instContinuousPathCalculus2 {E : Type u_2} {F : Type u_3} [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

• EulerContinuousPathCalculus.instContinuousPathCalculus2 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathCalculus.instContinuousPathCalculus3 {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] : NormedAddCommGroup C(K, E)

Cache the standard NormedAddCommGroup C(K,E) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathCalculus.instContinuousPathCalculus3 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathCalculus.instContinuousPathCalculus4 {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] : NormedSpace ℝ C(K, E)

Cache the standard NormedSpace ℝ C(K,E) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathCalculus.instContinuousPathCalculus4 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathCalculus.instContinuousPathCalculus5 {K : Type u_1} {F : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup F] : NormedAddCommGroup C(K, F)

Cache the standard NormedAddCommGroup C(K,F) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathCalculus.instContinuousPathCalculus5 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathCalculus.instContinuousPathCalculus6 {K : Type u_1} {F : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ C(K, F)

Cache the standard NormedSpace ℝ C(K,F) instance to shorten typeclass synthesis.

Equations

• EulerContinuousPathCalculus.instContinuousPathCalculus6 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathCalculus.instContinuousPathCalculus7 {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [CompactSpace K] [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

• EulerContinuousPathCalculus.instContinuousPathCalculus7 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousPathCalculus.instContinuousPathCalculus8 {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [CompactSpace K] [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

• EulerContinuousPathCalculus.instContinuousPathCalculus8 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerContinuousPathCalculus.instContinuousPathCalculus9 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerContinuousPathCalculus.instContinuousPathCalculus10 = inferInstance

noncomputable def EulerContinuousPathCalculus.coefficientLinear {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) →ₗ[ℝ] C(K, E) →L[ℝ] C(K, F)

The actual coefficient-to-continuous-multiplier map is linear.

Equations

• EulerContinuousPathCalculus.coefficientLinear = { toFun := EulerContinuousTimeIntegral.multiplier, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerContinuousPathCalculus.coefficientMap {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)

A bounded linear map in the actual uniform coefficient norm.

Equations

• EulerContinuousPathCalculus.coefficientMap = { toLinearMap := EulerContinuousPathCalculus.coefficientLinear, cont := ⋯ }

@[simp]

theorem EulerContinuousPathCalculus.coefficientMap_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)) : coefficientMap A = EulerContinuousTimeIntegral.multiplier A

theorem EulerContinuousPathCalculus.coefficientMap_norm {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : ‖coefficientMap‖ ≤ 1

Coefficient lifting to continuous paths is a norm contraction.

theorem EulerContinuousPathCalculus.contDiff_multiplier {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → C(K, E →L[ℝ] F)) {n : WithTop ℕ∞} (hA : ContDiff ℝ n A) : ContDiff ℝ n fun (x : P) => EulerContinuousTimeIntegral.multiplier (A x)

Genuine parameter regularity of the continuous multiplier.

theorem EulerContinuousPathCalculus.multiplier_bound {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → C(K, E →L[ℝ] F)) (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) => EulerContinuousTimeIntegral.multiplier (A y)) x‖ ≤ C * EulerGevrey.majorant R d n

Actual derivative estimates of the continuous multiplier have no amplitude loss.

theorem EulerContinuousPathCalculus.contDiff_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] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → C(K, E →L[ℝ] F)) (f : P → C(K, E)) {n : WithTop ℕ∞} (hA : ContDiff ℝ n A) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : P) => (EulerContinuousTimeIntegral.multiplier (A x)) (f x)

Pointwise application to a continuous path is genuinely smooth.

theorem EulerContinuousPathCalculus.apply_bound {K : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] (A : P → C(K, E →L[ℝ] F)) (f : P → C(K, E)) (hA : ContDiff ℝ (↑⊤) A) (hf : ContDiff ℝ (↑⊤) f) (R C D : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) (c d : ℕ) (hA_bound : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n A x‖ ≤ C * EulerGevrey.majorant R c n) (hf_bound : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ D * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => (EulerContinuousTimeIntegral.multiplier (A y)) (f y)) x‖ ≤ 3 * C * D * EulerGevrey.majorant R (c + d) n

The actual pointwise product obeys the fixed factorial product estimate.