Classical spatial slices and true within-time derivatives of the joined recursive family.
theorem
EulerPacketCylinderField.joinedSource_high_slice
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(p : ℕ)
(t : ↑(Set.Icc 0 M.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
EulerPacketPointJets.SliceDifferentiable (Set.Icc 0 M.T) (joinedSourceProfiles P M D τ hτ hτT B primary p).high
(↑t, x, θ)
theorem
EulerPacketCylinderField.joinedSource_mean_slice
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(p : ℕ)
(t : ↑(Set.Icc 0 M.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
EulerPacketPointJets.SliceDifferentiable (Set.Icc 0 M.T) (joinedSourceProfiles P M D τ hτ hτT B primary p).mean
(↑t, x, θ)
theorem
EulerPacketCylinderField.joinedSource_corrector_slice
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(p : ℕ)
(t : ↑(Set.Icc 0 M.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
EulerPacketPointJets.SliceDifferentiable (Set.Icc 0 M.T) (joinedSourceProfiles P M D τ hτ hτT B primary p).corrector
(↑t, x, θ)
theorem
EulerPacketCylinderField.joinedSource_highPressure_smooth_all
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(hπ : ∀ (t : ↑(Set.Icc 0 M.T)), ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => primary.highPressure (↑t, y))
(p : ℕ)
(t : ↑(Set.Icc 0 M.T))
:
ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) =>
(joinedSourceProfiles P M D τ hτ hτT B primary p).highPressure (↑t, y)
theorem
EulerPacketCylinderField.joinedSource_meanPressure_smooth_all
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(hm : primary.meanPressure = 0)
(p : ℕ)
(t : ↑(Set.Icc 0 M.T))
:
ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) =>
(joinedSourceProfiles P M D τ hτ hτT B primary p).meanPressure (↑t, y)
theorem
EulerPacketCylinderField.joinedSource_meanPressure_angle_all
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(hm : primary.meanPressure = 0)
(p : ℕ)
(t : ↑(Set.Icc 0 M.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
(EulerPacketPointJets.pressureJet (joinedSourceProfiles P M D τ hτ hτT B primary p).meanPressure (↑t, x, θ)).2
EulerPacketPointJets.angleDirection = 0