Actual admissible forcing restriction and the history trace used as forward initial data.

Time restriction and changes of time variable commute with actual smooth cylinder representatives.

theorem EulerLpCylinderTranslation.timeComp_orbit_contDiff (P : ℝ) [Fact (0 < P)] {K : Type u_1} {L : Type u_2} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] (p : C(K, ↥(CylinderL2 P V))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) p) (φ : C(L, K)) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) (p.comp φ)

theorem EulerLpCylinderTranslation.timeComp_norm (P : ℝ) [Fact (0 < P)] {K : Type u_1} {L : Type u_2} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] (φ : C(L, K)) : ‖ContinuousMap.compCLM ℝ (↥(CylinderL2 P V)) φ‖ ≤ 1

theorem EulerLpCylinderTranslation.timeComp_block_le (P : ℝ) [Fact (0 < P)] {K : Type u_1} {L : Type u_2} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_4} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (q : ℕ) (p : C(K, ↥(CylinderL2 P V))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) p) (φ : C(L, K)) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P b) (p.comp φ)) n a ≤ EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P b) p) n a

theorem EulerLpCylinderTranslation.pointField_timeComp (P : ℝ) [Fact (0 < P)] {K : Type u_1} {L : Type u_2} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] (p : C(K, ↥(CylinderL2 P EulerSmoothLimit.Space))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) p) (φ : C(L, K)) (t : L) : EulerCylinderSmoothOrbit.pointField P (p.comp φ) ⋯ t = EulerCylinderSmoothOrbit.pointField P p hp (φ t)

theorem EulerLpCylinderTranslation.scalarPointField_timeComp (P : ℝ) [Fact (0 < P)] {K : Type u_1} {L : Type u_2} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] (p : C(K, ↥(CylinderL2 P ℝ))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) p) (φ : C(L, K)) (t : L) : EulerCylinderScalarPrimitive.scalarPointField P (p.comp φ) ⋯ t = EulerCylinderScalarPrimitive.scalarPointField P p hp (φ t)

def EulerTransversePacketProvider.shiftedRaw (τ : ℝ) (raw : EulerPacketProfileRecursion.VectorField) : EulerPacketProfileRecursion.VectorField

Shifted raw, defined pointwise by raw (τ+z.1,z.2).

Equations

• EulerTransversePacketProvider.shiftedRaw τ raw z = raw (τ + z.1, z.2)

noncomputable def EulerTransversePacketProvider.Forcing.initial {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (τ : ℝ) (hτ : 0 < τ) (hτT : τ ≤ D.T) : Forcing P (D.initial τ hτ hτT) raw

Restriction keeps the literal original forcing on the history interval.

Equations

• G.initial τ hτ hτT = { path := G.path.comp (EulerTimeIntervalRestriction.initialInclusion D.T τ hτT), path_orbit := ⋯, raw_eq := ⋯, mean_zero := ⋯ }

noncomputable def EulerTransversePacketProvider.Forcing.tail {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (τ : ℝ) (hτ : 0 ≤ τ) (hτT : τ < D.T) : Forcing P (D.tail τ hτ hτT) (shiftedRaw τ raw)

The forward forcing uses elapsed time s and the literal source time τ+s.

Equations

• G.tail τ hτ hτT = { path := G.path.comp (EulerTimeIntervalRestriction.tailInclusion D.T τ hτ), path_orbit := ⋯, raw_eq := ⋯, mean_zero := ⋯ }

noncomputable def EulerTransversePacketProvider.HistoryData.terminalInitial {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (B : HistoryData D) (G : Forcing P D raw) : InitialData P D

The genuine terminal coordinate velocity of the history problem, with its actual support, mixed smoothness, and zero angular mean.

Equations

• B.terminalInitial G = { value := ⟨(B.coordinatePath G) ⟨D.T, ⋯⟩, ⋯⟩, orbit := ⋯, mean_zero := ⋯ }

noncomputable def EulerTransversePacketProvider.HistoryData.forwardInitial {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (B : HistoryData D) (G : Forcing P D raw) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) : InitialData P (D.tail τ ⋯ hτT)

The history trace in the same fixed reference-plane coordinates is the actual initial datum passed to the forward interval.

Equations

• B.forwardInitial G τ hτ hτT = { value := ((B.initial τ hτ ⋯).terminalInitial (G.initial τ hτ ⋯)).value, orbit := ⋯, mean_zero := ⋯ }

theorem EulerTransversePacketProvider.HistoryData.forwardInitial_eq {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (B : HistoryData D) (G : Forcing P D raw) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) : ↑(B.forwardInitial G τ hτ hτT).value = ((B.initial τ hτ ⋯).coordinatePath (G.initial τ hτ ⋯)) ⟨τ, ⋯⟩