The actual source coefficient differences retain a factor ell. The stationary history sensitivity is linear in these differences, so its computed Lipschitz constant retains that factor as well.

@[instance_reducible]

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.instParentPacketNeighborBounds1 {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] V)

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

Equations

• EulerMeanCoefficients.SmoothCoefficientPath.instParentPacketNeighborBounds1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.instParentPacketNeighborBounds2 {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] V)

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

Equations

• EulerMeanCoefficients.SmoothCoefficientPath.instParentPacketNeighborBounds2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.instParentPacketNeighborBounds3 {V : Type} [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

• EulerMeanCoefficients.SmoothCoefficientPath.instParentPacketNeighborBounds3 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.instParentPacketNeighborBounds4 {V : Type} [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

• EulerMeanCoefficients.SmoothCoefficientPath.instParentPacketNeighborBounds4 = inferInstance

theorem EulerMeanCoefficients.SmoothCoefficientPath.derivative_norm_le_of_bound {J V : Type} [TopologicalSpace J] [CompactSpace J] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath J V) (C : ℝ) (hC : 0 ≤ C) (hb : ∀ (t : J) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ 1 (⇑(A.field t)) x‖ ≤ C) : ‖A.derivative.field‖ ≤ C

noncomputable def EulerParentPacketFrames.LabelData.frameDifferenceCost {G : Parent} (L : LabelData G) : ℝ

Frame difference cost, given by frameAmplitude L.K*coefficientRadius L.K.

Equations

• L.frameDifferenceCost = EulerPacketParentLabelBounds.frameAmplitude L.K * EulerPacketParentLabelBounds.coefficientRadius L.K

noncomputable def EulerParentPacketFrames.LabelData.firstDifferenceCost {G : Parent} (L : LabelData G) : ℝ

First difference cost, given by gradientAmplitude L.K*coefficientRadius L.K.

Equations

• L.firstDifferenceCost = EulerPacketParentLabelBounds.gradientAmplitude L.K * EulerPacketParentLabelBounds.coefficientRadius L.K

noncomputable def EulerParentPacketFrames.LabelData.normalDifferenceCost {G : Parent} (L : LabelData G) : ℝ

Normal difference cost, given by 9*(frameAmplitude L.K)^2*coefficientRadius L.K.

Equations

• L.normalDifferenceCost = 9 * EulerPacketParentLabelBounds.frameAmplitude L.K ^ 2 * EulerPacketParentLabelBounds.coefficientRadius L.K

noncomputable def EulerParentPacketFrames.LabelData.strainDifferenceCost {G : Parent} (L : LabelData G) : ℝ

Strain difference cost, given by 27*(frameAmplitude L.K)^2*gradientAmplitude L.K*coefficientRadius L.K.

Equations

• L.strainDifferenceCost = 27 * EulerPacketParentLabelBounds.frameAmplitude L.K ^ 2 * EulerPacketParentLabelBounds.gradientAmplitude L.K * EulerPacketParentLabelBounds.coefficientRadius L.K

theorem EulerParentPacketFrames.LabelData.scaled_first_majorant {G : Parent} (L : LabelData G) (A : ℝ) : A * EulerGevrey.majorant L.scaledRadius 0 1 = A * EulerPacketParentLabelBounds.coefficientRadius L.K * G.ell

theorem EulerParentPacketFrames.LabelData.source_frame_derivative_norm {G : Parent} (L : LabelData G) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) : ‖(G.transverseData m hm R S hS).frame.derivative.field‖ ≤ L.frameDifferenceCost * G.ell

theorem EulerParentPacketFrames.LabelData.source_first_derivative_norm {G : Parent} (L : LabelData G) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) : ‖(G.transverseData m hm R S hS).frameDerivative.derivative.field‖ ≤ L.firstDifferenceCost * G.ell

theorem EulerParentPacketFrames.LabelData.source_normal_derivative_norm {G : Parent} (L : LabelData G) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) : ‖(G.transverseData m hm R S hS).normal.derivative.field‖ ≤ L.normalDifferenceCost * G.ell

theorem EulerParentPacketFrames.LabelData.source_strain_derivative_norm {G : Parent} (L : LabelData G) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) : ‖(G.transverseData m hm R S hS).M.derivative.field‖ ≤ L.strainDifferenceCost * G.ell

theorem EulerParentPacketFrames.LabelData.source_curvature_derivative_norm {G : Parent} (L : LabelData G) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (H : LowBounds G) : ‖(G.historyData m hm R S hS H).H.derivative.field‖ ≤ L.strainDifferenceCost * G.ell

noncomputable def EulerParentPacketFrames.LabelData.historyDifferenceScaleCost {G : Parent} (L : LabelData G) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (H : LowBounds G) : ℝ

History difference scale cost as an element of ℝ.

Equations

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

theorem EulerParentPacketFrames.LabelData.source_history_derivative_scale {G : Parent} (L : LabelData G) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (H : LowBounds G) : EulerPacketActivationHistory.historyLabelDifferenceCost (G.historyData m hm R S hS H) ≤ L.historyDifferenceScaleCost m hm R S hS H * G.ell