Actual equations, tangency and pressure regularity at every solved joined grade.

theorem EulerPacketCylinderField.joinedInverse_eq_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τ ⋯)) (A : SourceCoefficientAgreement M D) (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (joinedSourceOperators P M D τ hτ hτT B).inverseFrame (↑t, x, θ) = M.inverseFrame (↑t, x, θ)

theorem EulerPacketCylinderField.joinedStrain_eq_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τ ⋯)) (A : SourceCoefficientAgreement M D) (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (joinedSourceOperators P M D τ hτ hτT B).strain (↑t, x, θ) = M.strain (↑t, x, θ)

theorem EulerPacketCylinderField.joinedSource_mean_equation (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) (A : SourceCoefficientAgreement M D) (p : ℕ) (hp : 2 ≤ p) (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.linearPart ((joinedSourceOperators P M D τ hτ hτT B).strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 M.T) (joinedSourceProfiles P M D τ hτ hτT B primary p).mean (↑t, x, θ)) + (EulerPacketPointJets.slowPressure ((joinedSourceOperators P M D τ hτ hτT B).inverseFrame (↑t, x, θ))) (EulerPacketPointJets.pressureJet (joinedSourceProfiles P M D τ hτ hτT B primary p).meanPressure (↑t, x, θ)) = EulerPacketProfileRecursion.meanForce (joinedSourceOperators P M D τ hτ hτT B) p (joinedSourceProfiles P M D τ hτ hτT B primary) (↑t, x, θ)

theorem EulerPacketCylinderField.joinedSource_high_equation (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 : ℕ) (hp : 2 ≤ p) (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.linearPart ((joinedSourceOperators P M D τ hτ hτT B).strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 M.T) (joinedSourceProfiles P M D τ hτ hτT B primary p).high (↑t, x, θ)) + (EulerPacketPointJets.fastPressure ((joinedSourceOperators P M D τ hτ hτT B).normal (↑t, x, θ))) (EulerPacketPointJets.pressureJet (joinedSourceProfiles P M D τ hτ hτT B primary p).highPressure (↑t, x, θ)) = EulerPacketProfileRecursion.highForce (joinedSourceOperators P M D τ hτ hτT B) p (joinedSourceProfiles P M D τ hτ hτT B primary) (↑t, x, θ)

theorem EulerPacketCylinderField.joinedSource_high_tangent (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 : ℕ) (hp : 2 ≤ p) (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : inner ℝ (D.normalField (↑t, x, θ)) ((joinedSourceProfiles P M D τ hτ hτT B primary p).high (↑t, x, θ)) = 0

theorem EulerPacketCylinderField.joinedSource_highPressure_smooth (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 : ℕ) (hp : 2 ≤ p) (t : ℝ) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => (joinedSourceProfiles P M D τ hτ hτT B primary p).highPressure (t, y)

theorem EulerPacketCylinderField.joinedSource_meanPressure_smooth (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 : ℕ) (hp : 2 ≤ p) (t : ℝ) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => (joinedSourceProfiles P M D τ hτ hτT B primary p).meanPressure (t, y)

theorem EulerPacketCylinderField.joinedSource_meanPressure_angle (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 : ℕ) (hp : 2 ≤ p) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.pressureJet (joinedSourceProfiles P M D τ hτ hτT B primary p).meanPressure (t, x, θ)).2 EulerPacketPointJets.angleDirection = 0