Actual defining equations of the generated mean and high profiles.

structure EulerPacketCylinderField.SourceCoefficientAgreement {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (M : EulerMeanPacketProvider.Data) (D : EulerTransversePacketProvider.Data U) : Prop

The two source inverses use the same prescribed inverse deformation and strain.

• inverse (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) : (M.FInv t) x = (D.FInv.field (D.clamp ↑t)) x
• strain (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) : (M.M.field t) x = (D.M.field (D.clamp ↑t)) x

theorem EulerPacketCylinderField.sourceInverse_eq_mean {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) (D : EulerTransversePacketProvider.Data U) (I : EulerTransversePacketProvider.InitialData P D) (A : SourceCoefficientAgreement M D) (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (sourceOperators P M D I).inverseFrame (↑t, x, θ) = M.inverseFrame (↑t, x, θ)

theorem EulerPacketCylinderField.sourceStrain_eq_mean {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) (D : EulerTransversePacketProvider.Data U) (I : EulerTransversePacketProvider.InitialData P D) (A : SourceCoefficientAgreement M D) (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (sourceOperators P M D I).strain (↑t, x, θ) = M.strain (↑t, x, θ)

theorem EulerPacketCylinderField.source_mean_equation {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (A : SourceCoefficientAgreement M D) (p : ℕ) (hp : 2 ≤ p) (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.linearPart ((sourceOperators P M D I).strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 M.T) (sourceProfiles P M D I Iprimary p).mean (↑t, x, θ)) + (EulerPacketPointJets.slowPressure ((sourceOperators P M D I).inverseFrame (↑t, x, θ))) (EulerPacketPointJets.pressureJet (sourceProfiles P M D I Iprimary p).meanPressure (↑t, x, θ)) = EulerPacketProfileRecursion.meanForce (sourceOperators P M D I) p (sourceProfiles P M D I Iprimary) (↑t, x, θ)

theorem EulerPacketCylinderField.source_high_equation {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (p : ℕ) (hp : 2 ≤ p) (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.linearPart ((sourceOperators P M D I).strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 M.T) (sourceProfiles P M D I Iprimary p).high (↑t, x, θ)) + (EulerPacketPointJets.fastPressure ((sourceOperators P M D I).normal (↑t, x, θ))) (EulerPacketPointJets.pressureJet (sourceProfiles P M D I Iprimary p).highPressure (↑t, x, θ)) = EulerPacketProfileRecursion.highForce (sourceOperators P M D I) p (sourceProfiles P M D I Iprimary) (↑t, x, θ)

theorem EulerPacketCylinderField.source_primary_equation {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.linearPart ((sourceOperators P M D I).strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 M.T) ((homogeneousForcing D).vector Iprimary) (↑t, x, θ)) + (EulerPacketPointJets.fastPressure ((sourceOperators P M D I).normal (↑t, x, θ))) (EulerPacketPointJets.pressureJet ((homogeneousForcing D).scalar Iprimary) (↑t, x, θ)) = 0