The center error in a geometric packet choice is the gradient of the actual increment between its two Euler states.

@[reducible, inline]

noncomputable abbrev EulerParentPacketFrames.GeometryJoinedChoice.residual {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : EulerPacketInitial.Input U) (S : SmoothState I.parent) (k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : GeometryJoinedChoice I S k hk nextEll hnext hnext1) : EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯ (EulerPacketTerminalDatum.initializedCorrectionData I.meanData I.data ⋯ I.historyTime ⋯ ⋯ I.history I.geometry.δ ⋯ I.terminal ⋯ I.alpha ⋯ (EulerPacketSourceFrequency.truncation k) ⋯ k ⋯)

Residual type used in parent geometry choice center.

Equations

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

theorem EulerParentPacketFrames.GeometryJoinedChoice.increment_fderiv {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : EulerPacketInitial.Input U) (S : SmoothState I.parent) (k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : GeometryJoinedChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space) : fderiv ℝ (S.velocityIncrement (state I S k hk nextEll hnext hnext1 F hSym) ↑t) x = fderiv ℝ (I.parent.normalizedPacketVelocity I.normal ⋯ I.coordinates I.support ⋯ F.Q (residual I S k hk nextEll hnext hnext1 F) k S.evolution.inverse t) (I.parent.ell⁻¹ • x)

theorem EulerParentPacketFrames.GeometryJoinedChoice.center_error {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : EulerPacketInitial.Input U) (S : SmoothState I.parent) (k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : GeometryJoinedChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (t : ↑(Set.Icc 0 I.parent.T)) : ‖fderiv ℝ (S.velocityIncrement (state I S k hk nextEll hnext hnext1 F hSym) ↑t) 0 - EulerPacketPhysicalLowBounds.shearTerm (I.geometry.primaryAmplitude ⋯) (deriv (EulerPeriodicProfile.profile I.geometry.δ) (k * inner ℝ I.normal (S.evolution.inverse.normalized t 0))) ((I.data.normal.field t) (S.evolution.inverse.normalized t 0)) (EulerPacketPrimaryFactorization.canonicalVelocity I.historyTime ⋯ ⋯ I.history (EulerPacketSourceGeometry.Guards.terminal ⋯ ⋯ I.frame (I.parent.historyOn I.low I.normal ⋯ I.coordinates I.support ⋯ I.historyTime ⋯ ⋯) I.geometry) ⋯ (↑t) (S.evolution.inverse.normalized t 0))‖ ≤ k ^ (-(1 / 4))

@[reducible, inline]

noncomputable abbrev EulerParentPacketFrames.GeometryForwardChoice.residual {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (S : SmoothState I.parent) (k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) : EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯ (EulerPacketTerminalDatum.forwardInitializedCorrectionData I.meanData I.data ⋯ I.geometry.δ ⋯ I.geometry.initialCoordinate ⋯ I.alpha ⋯ (EulerPacketSourceFrequency.truncation k) ⋯ k ⋯)

Residual type used in parent geometry choice center.

Equations

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

theorem EulerParentPacketFrames.GeometryForwardChoice.increment_fderiv {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (S : SmoothState I.parent) (k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space) : fderiv ℝ (S.velocityIncrement (state I S k hk nextEll hnext hnext1 F hSym) ↑t) x = fderiv ℝ (I.parent.normalizedPacketVelocity I.normal ⋯ I.coordinates I.support ⋯ F.Q (residual I S k hk nextEll hnext hnext1 F) k S.evolution.inverse t) (I.parent.ell⁻¹ • x)

theorem EulerParentPacketFrames.GeometryForwardChoice.center_error {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (S : SmoothState I.parent) (k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (t : ↑(Set.Icc 0 I.parent.T)) : ‖fderiv ℝ (S.velocityIncrement (state I S k hk nextEll hnext hnext1 F hSym) ↑t) 0 - EulerPacketPhysicalLowBounds.shearTerm (I.geometry.primaryAmplitude ⋯) (deriv (EulerPeriodicProfile.profile I.geometry.δ) (k * inner ℝ I.normal (S.evolution.inverse.normalized t 0))) ((I.data.normal.field t) (S.evolution.inverse.normalized t 0)) (EulerPacketForwardFactorization.canonicalVelocity I.data I.geometry.initialCoordinate (↑t) (S.evolution.inverse.normalized t 0))‖ ≤ k ^ (-(1 / 4))