Uniform label difference estimates from genuine coefficient derivatives.

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketCoefficientLipschitz1 {V : Type u_1} [NormedAddCommGroup V] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space V)

Cache the standard NormedAddCommGroup (Space →ᵇ V) instance to shorten typeclass synthesis.

Equations

• EulerPacketActivationHistory.instPacketCoefficientLipschitz1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketCoefficientLipschitz2 {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space V)

Cache the standard NormedSpace ℝ (Space →ᵇ V) instance to shorten typeclass synthesis.

Equations

• EulerPacketActivationHistory.instPacketCoefficientLipschitz2 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketCoefficientLipschitz3 {T : ℝ} {V : Type u_1} [NormedAddCommGroup V] : NormedAddCommGroup C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space V)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,Space →ᵇ V) instance to shorten typeclass synthesis.

Equations

• EulerPacketActivationHistory.instPacketCoefficientLipschitz3 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketCoefficientLipschitz4 {T : ℝ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space V)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,Space →ᵇ V) instance to shorten typeclass synthesis.

Equations

• EulerPacketActivationHistory.instPacketCoefficientLipschitz4 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketCoefficientLipschitz5 {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] V)

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

Equations

• EulerPacketActivationHistory.instPacketCoefficientLipschitz5 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketCoefficientLipschitz6 {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] V)

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

Equations

• EulerPacketActivationHistory.instPacketCoefficientLipschitz6 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketCoefficientLipschitz7 {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))

Cache the standard NormedAddCommGroup (Space →ᵇ (Space →L[ℝ] V)) instance to shorten typeclass synthesis.

Equations

• EulerPacketActivationHistory.instPacketCoefficientLipschitz7 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketCoefficientLipschitz8 {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))

Cache the standard NormedSpace ℝ (Space →ᵇ (Space →L[ℝ] V)) instance to shorten typeclass synthesis.

Equations

• EulerPacketActivationHistory.instPacketCoefficientLipschitz8 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketCoefficientLipschitz9 {T : ℝ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedAddCommGroup C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,Space →ᵇ (Space →L[ℝ] V)) instance to shorten typeclass synthesis.

Equations

• EulerPacketActivationHistory.instPacketCoefficientLipschitz9 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketCoefficientLipschitz10 {T : ℝ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] V))

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,Space →ᵇ (Space →L[ℝ] V)) instance to shorten typeclass synthesis.

Equations

• EulerPacketActivationHistory.instPacketCoefficientLipschitz10 = inferInstance

theorem EulerPacketActivationHistory.coefficient_label_norm {T : ℝ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) V) (x : EulerSmoothLimit.Space) : ‖(EulerTransverseSourceCoefficientPath.pathEvaluation x) A.field‖ ≤ ‖A.field‖

theorem EulerPacketActivationHistory.coefficient_difference {T : ℝ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) V) (t : ↑(Set.Icc 0 T)) (x y : EulerSmoothLimit.Space) : ‖(A.field t) x - (A.field t) y‖ ≤ ‖A.derivative.field‖ * ‖x - y‖

theorem EulerPacketActivationHistory.coefficient_label_difference {T : ℝ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) V) (x y : EulerSmoothLimit.Space) : ‖(EulerTransverseSourceCoefficientPath.pathEvaluation x) A.field - (EulerTransverseSourceCoefficientPath.pathEvaluation y) A.field‖ ≤ ‖A.derivative.field‖ * ‖x - y‖