The genuine endpoint primary supplies all qualitative inputs to the joined recursion.
noncomputable def
EulerPacketCylinderField.joinedTerminalPrimary
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{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τ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
:
Joined terminal primary, constructed using primaryProfile.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketCylinderField.joinedTerminalPrimaryWitness
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
:
ProfileRegularity P M.T ⋯ D.support (joinedTerminalPrimary P M D τ hτ hτT B Y)
Joined terminal primary witness as an element of ProfileRegularity P M.T M.T_pos.le D.support (joinedTerminalPrimary P M D τ hτ hτT B Y).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketCylinderField.joinedTerminalPrimary_mean
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{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τ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
:
theorem
EulerPacketCylinderField.joinedTerminalPrimary_tangent
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 M.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
theorem
EulerPacketCylinderField.joinedTerminalPrimary_pressure_smooth
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{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τ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ℝ)
:
ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => (joinedTerminalPrimary P M D τ hτ hτT B Y).highPressure (t, y)
theorem
EulerPacketCylinderField.joinedTerminalPrimary_equation
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 M.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
(EulerPacketPointJets.linearPart (D.strain (↑t, x, θ)))
(EulerPacketPointJets.slicedJet (Set.Icc 0 M.T) (joinedTerminalPrimary P M D τ hτ hτT B Y).high (↑t, x, θ)) + (EulerPacketPointJets.fastPressure (D.normalField (↑t, x, θ)))
(EulerPacketPointJets.pressureJet (joinedTerminalPrimary P M D τ hτ hτT B Y).highPressure (↑t, x, θ)) = 0