The actual time derivative and normalized pressure also match at the history/forward junction.

The history trace matches the actual forward transverse solve

The forward datum is the constructed history coordinate velocity. Both physical velocities therefore agree at the source time τ, with the same deformation frame on the two intervals.

The joined inverse uses coercivity only on the actual history interval. Its source Hessian need not satisfy a smallness condition on the full history-plus-forward time interval.

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

The terminal coordinate of the actual local history, used as forward data.

Equations

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

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

noncomputable def EulerTransversePacketJoin.pastVelocity {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : C(↑(Set.Icc 0 τ), ↥(EulerLiftedGradientSpace.LiftL2 P))

Past velocity, given by B.velocityPath (G.initial τ hτ hτT.le).

Equations

• EulerTransversePacketJoin.pastVelocity τ hτ hτT B G = B.velocityPath (G.initial τ hτ ⋯)

noncomputable def EulerTransversePacketJoin.futureVelocity {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : C(↑(Set.Icc 0 (D.T - τ)), ↥(EulerLiftedGradientSpace.LiftL2 P))

Future velocity, given by includePath P D.support D.support_measurable ((G.tail τ hτ.le hτT).velocityPath (forwardInitial τ hτ hτT B G)).

Equations

• EulerTransversePacketJoin.futureVelocity τ hτ hτT B G = (EulerLpCylinderPaths.includePath P D.support ⋯) ((G.tail τ ⋯ hτT).velocityPath (EulerTransversePacketJoin.forwardInitial τ hτ hτT B G))

noncomputable def EulerTransversePacketJoin.pastDerivative {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : C(↑(Set.Icc 0 τ), ↥(EulerLiftedGradientSpace.LiftL2 P))

Past derivative, given by B.derivativePath (G.initial τ hτ hτT.le).

Equations

• EulerTransversePacketJoin.pastDerivative τ hτ hτT B G = B.derivativePath (G.initial τ hτ ⋯)

noncomputable def EulerTransversePacketJoin.futureDerivative {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : C(↑(Set.Icc 0 (D.T - τ)), ↥(EulerLiftedGradientSpace.LiftL2 P))

Future derivative, given by includePath P D.support D.support_measurable ((G.tail τ hτ.le hτT).derivativePath (forwardInitial τ hτ hτT B G)).

Equations

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

noncomputable def EulerTransversePacketJoin.pastPressure {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : C(↑(Set.Icc 0 τ), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))

Past pressure, given by B.pressurePath (G.initial τ hτ hτT.le).

Equations

• EulerTransversePacketJoin.pastPressure τ hτ hτT B G = B.pressurePath (G.initial τ hτ ⋯)

noncomputable def EulerTransversePacketJoin.futurePressure {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : C(↑(Set.Icc 0 (D.T - τ)), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))

Future pressure, given by (G.tail τ hτ.le hτT).pressurePath (forwardInitial τ hτ hτT B G).

Equations

• EulerTransversePacketJoin.futurePressure τ hτ hτT B G = (G.tail τ ⋯ hτT).pressurePath (EulerTransversePacketJoin.forwardInitial τ hτ hτT B G)

theorem EulerTransversePacketJoin.pastVelocity_orbit {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (pastVelocity τ hτ hτT B G)

theorem EulerTransversePacketJoin.futureVelocity_orbit {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (futureVelocity τ hτ hτT B G)

theorem EulerTransversePacketJoin.pastDerivative_orbit {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (pastDerivative τ hτ hτT B G)

theorem EulerTransversePacketJoin.futureDerivative_orbit {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (futureDerivative τ hτ hτT B G)

theorem EulerTransversePacketJoin.pastPressure_orbit {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (pastPressure τ hτ hτT B G)

theorem EulerTransversePacketJoin.futurePressure_orbit {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (futurePressure τ hτ hτT B G)

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

The actual forward velocity starts from the actual history velocity.

theorem EulerTransversePacketJoin.source_coefficient_match {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 D.T)) V) : (A.comp (EulerTimeIntervalRestriction.initialInclusion D.T τ ⋯)).field ⟨τ, ⋯⟩ = (A.comp (EulerTimeIntervalRestriction.tailInclusion D.T τ ⋯)).field ⟨0, ⋯⟩

theorem EulerTransversePacketJoin.normal_match {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) : (D.initial τ hτ ⋯).normal.field ⟨τ, ⋯⟩ = (D.tail τ ⋯ hτT).normal.field ⟨0, ⋯⟩

theorem EulerTransversePacketJoin.forcing_match {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) : ↑((G.initial τ hτ ⋯).path ⟨τ, ⋯⟩) = ↑((G.tail τ ⋯ hτT).path ⟨0, ⋯⟩)

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

The same physical first-order equation determines the same derivative from the matching velocity and forcing.

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

The normalized pressure integral has the same input scalar L² class on both sides of the junction.