Genuine label sensitivity of the stationary source history. All constants below are computed from the supplied smooth coefficient paths; no continuity or estimate for the solved history is assumed.

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketActivationLipschitz1 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (U →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz1 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz2 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketActivationLipschitz3 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz3 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz4 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketActivationLipschitz5 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} : NormedAddCommGroup C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz5 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketActivationLipschitz6 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} : NormedSpace ℝ C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz6 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketActivationLipschitz7 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] U →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz7 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz8 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketActivationLipschitz9 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] U →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz9 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz10 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketActivationLipschitz11 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} : NormedAddCommGroup C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] U →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz11 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketActivationLipschitz12 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} : NormedSpace ℝ C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] U →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz12 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketActivationLipschitz13 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz13 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketActivationLipschitz14 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz14 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketActivationLipschitz15 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz15 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketActivationLipschitz16 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz16 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketActivationLipschitz17 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} : NormedAddCommGroup C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz17 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketActivationHistory.instPacketActivationLipschitz18 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} : NormedSpace ℝ C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerPacketActivationHistory.instPacketActivationLipschitz18 = inferInstance

noncomputable def EulerPacketActivationHistory.historyTransportCost {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} : ℝ

History transport cost as an element of ℝ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerPacketActivationHistory.historyLabelSizeCost {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) : ℝ

History label size cost, constructed using historyCost.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerPacketActivationHistory.historyLabelDifferenceCost {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) : ℝ

History label difference cost, constructed using historyDifferenceCost.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerPacketActivationHistory.historyTransportCost_nonneg {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} : 0 ≤ historyTransportCost

theorem EulerPacketActivationHistory.label_transportCost_le {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) (x : EulerSmoothLimit.Space) : EulerTimeH1FrameTransport.transportCost D.T (B.coefficients.labelFrame x) (B.coefficients.labelFrameDerivative x) D.frameLower ≤ historyTransportCost

theorem EulerPacketActivationHistory.label_derivative_size {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) (x : EulerSmoothLimit.Space) : D.T * ‖B.coefficients.labelFrameDerivative x‖ + ‖B.coefficients.labelFrame x‖ ≤ D.T * ‖D.frameDerivative.field‖ + ‖D.frame.field‖

theorem EulerPacketActivationHistory.label_energy_size {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) (x : EulerSmoothLimit.Space) : 1 + D.T ^ 2 * ‖B.coefficients.labelHessian x‖ ≤ 1 + D.T ^ 2 * ‖B.H.field‖

theorem EulerPacketActivationHistory.historyLabelDifferenceCost_nonneg {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) : 0 ≤ historyLabelDifferenceCost B

theorem EulerPacketActivationHistory.labelVelocity_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) (x : EulerSmoothLimit.Space) : ‖B.coefficients.labelVelocity x‖ ≤ historyLabelSizeCost B

theorem EulerPacketActivationHistory.labelVelocity_difference {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) (x y : EulerSmoothLimit.Space) : ‖B.coefficients.labelVelocity x - B.coefficients.labelVelocity y‖ ≤ historyLabelDifferenceCost B * ‖x - y‖

theorem EulerPacketActivationHistory.labelVelocity_point_difference {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) (x y : EulerSmoothLimit.Space) (ξ : U) (t : ↑(Set.Icc 0 D.T)) : ‖((B.coefficients.labelVelocity x) ξ) t - ((B.coefficients.labelVelocity y) ξ) t‖ ≤ historyLabelDifferenceCost B * ‖x - y‖ * ‖ξ‖