The initial traces of the actual chosen Euler states are the same compact high and mean increments used in the initial-data convergence proof. Restriction to a shorter horizon preserves these equalities.

theorem EulerParentPacketFrames.SmoothState.velocityIncrement_restrictTime {A B : Parent} (S : SmoothState A) (T : SmoothState B) (s : ℝ) (hs : 0 < s) (hA : s ≤ A.T) (hB : s ≤ B.T) : (S.restrictTime s hs hA).velocityIncrement (T.restrictTime s hs hB) = S.velocityIncrement T

theorem EulerParentPacketFrames.GeometryJoinedChoice.normalized_initial {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) : I.parent.normalizedPacketVelocity I.normal ⋯ I.coordinates I.support ⋯ F.Q (residual I S k hk nextEll hnext hnext1 F) k S.evolution.inverse I.parent.zeroTime = EulerPacketTerminalDatum.initializedExactPhysicalVelocity I.meanData I.data ⋯ I.historyTime ⋯ ⋯ I.history I.geometry.δ ⋯ I.terminal ⋯ I.alpha ⋯ (EulerPacketSourceFrequency.truncation k) ⋯ k ⋯ F.Q I.parent.zeroTime id

theorem EulerParentPacketFrames.GeometryJoinedChoice.initial_increment {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) : S.velocityIncrement (state I S k hk nextEll hnext hnext1 F hSym) 0 = I.exactInitial k ⋯ ⋯ F.Q

theorem EulerParentPacketFrames.GeometryJoinedChoice.initial_increment_eq {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) : S.velocityIncrement (state I S k hk nextEll hnext hnext1 F hSym) 0 = I.high k + I.mean k

theorem EulerParentPacketFrames.GeometryJoinedChoice.state_velocity_initial {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) : (fun (x : EulerSmoothLimit.Space) => (state I S k hk nextEll hnext hnext1 F hSym).evolution.velocity (0, x)) = (fun (x : EulerSmoothLimit.Space) => S.evolution.velocity (0, x)) + (I.high k + I.mean k)

theorem EulerParentPacketFrames.GeometryJoinedChoice.restricted_initial_increment {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) (s : ℝ) (hs : 0 < s) (hT : s ≤ I.parent.T) : (S.restrictTime s hs hT).velocityIncrement ((state I S k hk nextEll hnext hnext1 F hSym).restrictTime s hs hT) 0 = I.high k + I.mean k

noncomputable def EulerParentPacketFrames.GeometryForwardInput.high {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (k : ℝ) : EulerSmoothLimit.Space → EulerSmoothLimit.Space

High, constructed using forwardInitializedInitialHigh.

Equations

• I.high k = EulerPacketTerminalDatum.forwardInitializedInitialHigh I.meanData I.data I.geometry.δ ⋯ I.geometry.initialCoordinate ⋯ I.alpha (EulerPacketSourceFrequency.truncation k) k

noncomputable def EulerParentPacketFrames.GeometryForwardInput.mean {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (k : ℝ) : EulerSmoothLimit.Space → EulerSmoothLimit.Space

Mean, constructed using forwardInitializedInitialMean.

Equations

• I.mean k = EulerPacketTerminalDatum.forwardInitializedInitialMean I.meanData I.data I.geometry.δ ⋯ I.geometry.initialCoordinate ⋯ I.alpha (EulerPacketSourceFrequency.truncation k) k

noncomputable def EulerParentPacketFrames.GeometryForwardInput.exactInitial {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (k : ℝ) (hk : 4 ≤ k) (hn : 1 ≤ EulerPacketSourceFrequency.truncation k) (Q : I.correctionBudget k hk hn) : EulerSmoothLimit.Space → EulerSmoothLimit.Space

Exact initial, constructed using scale.

Equations

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

theorem EulerParentPacketFrames.GeometryForwardInput.exactInitial_eq {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (k : ℝ) (hk : 4 ≤ k) (hn : 1 ≤ EulerPacketSourceFrequency.truncation k) (Q : I.correctionBudget k hk hn) : I.exactInitial k hk hn Q = I.high k + I.mean k

theorem EulerParentPacketFrames.GeometryForwardChoice.normalized_initial {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) : I.parent.normalizedPacketVelocity I.normal ⋯ I.coordinates I.support ⋯ F.Q (residual I S k hk nextEll hnext hnext1 F) k S.evolution.inverse I.parent.zeroTime = EulerPacketTerminalDatum.forwardInitializedExactPhysicalVelocity I.meanData I.data ⋯ I.geometry.δ ⋯ I.geometry.initialCoordinate ⋯ I.alpha ⋯ (EulerPacketSourceFrequency.truncation k) ⋯ k ⋯ F.Q I.parent.zeroTime id

theorem EulerParentPacketFrames.GeometryForwardChoice.initial_increment {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) : S.velocityIncrement (state I S k hk nextEll hnext hnext1 F hSym) 0 = I.exactInitial k ⋯ ⋯ F.Q

theorem EulerParentPacketFrames.GeometryForwardChoice.initial_increment_eq {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) : S.velocityIncrement (state I S k hk nextEll hnext hnext1 F hSym) 0 = I.high k + I.mean k

theorem EulerParentPacketFrames.GeometryForwardChoice.state_velocity_initial {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) : (fun (x : EulerSmoothLimit.Space) => (state I S k hk nextEll hnext hnext1 F hSym).evolution.velocity (0, x)) = (fun (x : EulerSmoothLimit.Space) => S.evolution.velocity (0, x)) + (I.high k + I.mean k)

theorem EulerParentPacketFrames.GeometryForwardChoice.restricted_initial_increment {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) (s : ℝ) (hs : 0 < s) (hT : s ≤ I.parent.T) : (S.restrictTime s hs hT).velocityIncrement ((state I S k hk nextEll hnext hnext1 F hSym).restrictTime s hs hT) 0 = I.high k + I.mean k