Spatial variation of the actual activation history retains the parent's label scale. The constants are computed from the prescribed coefficients and the older frame, not from an estimate on the new primary.

theorem EulerParentPacketFrames.LabelData.initial_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) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) : ‖((G.transverseData m hm R S hS).initial τ hτ ⋯).frame.derivative.field‖ ≤ L.frameDifferenceCost * G.ell

theorem EulerParentPacketFrames.LabelData.initial_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) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) : ‖((G.transverseData m hm R S hS).initial τ hτ ⋯).frameDerivative.derivative.field‖ ≤ L.firstDifferenceCost * G.ell

theorem EulerParentPacketFrames.LabelData.initial_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) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) : ‖(G.historyOn H m hm R S hS τ hτ hτT).H.derivative.field‖ ≤ L.strainDifferenceCost * G.ell

noncomputable def EulerParentPacketFrames.LabelData.initialHistoryDifferenceScaleCost {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) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) : ℝ

The coefficient of the label scale in the actual history difference bound. All zeroth norms belong to the restricted source coefficients.

Equations

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

theorem EulerParentPacketFrames.LabelData.initial_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) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) : EulerPacketActivationHistory.historyLabelDifferenceCost (G.historyOn H m hm R S hS τ hτ hτT) ≤ L.initialHistoryDifferenceScaleCost m hm R S hS H τ hτ hτT * G.ell

noncomputable def EulerParentPacketFrames.LabelData.neighborScaleCost {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) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) (P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ) (CM CH : ℝ) : ℝ

The actual neighbor coefficient after extracting the one factor of ell supplied by the parent spatial derivative estimates.

Equations

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

theorem EulerParentPacketFrames.LabelData.source_neighbor_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) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) (P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ) (CM CH : ℝ) (_hCM : 0 ≤ CM) (hCH : 0 ≤ CH) (hshear : 0 < P.shear) (heps : 0 < P.epsilon) : P.neighborCost hτ hτT (G.historyOn H m hm R S hS τ hτ hτT) CM CH ≤ L.neighborScaleCost m hm R S hS H τ hτ hτT P CM CH * G.ell

theorem EulerParentPacketFrames.LabelData.source_totalError_bound {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) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) (P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ) (CM CH ρ e n : ℝ) (hCM : 0 ≤ CM) (hCH : 0 ≤ CH) (hshear : 0 < P.shear) (heps : 0 < P.epsilon) (hρ : 0 ≤ ρ) (herr : P.error ≤ e) (hn : L.neighborScaleCost m hm R S hS H τ hτ hτT P CM CH * G.ell * ρ ≤ n) : P.totalError hτ hτT (G.historyOn H m hm R S hS τ hτ hτT) CM CH ρ ≤ e + n