The genuine physical pressure gradient has a finite covector expansion. The angular factor k shifts only the high-pressure series.

noncomputable def EulerPacketPressure.angularPressure (m : EulerSmoothLimit.Space) (p : EulerPacketProfileRecursion.ScalarField) : EulerPacketProfileRecursion.VectorField

Angular pressure, defined pointwise by (pressureJet p z).2 angleDirection • m.

Equations

• EulerPacketPressure.angularPressure m p z = (EulerPacketPointJets.pressureJet p z).2 EulerPacketPointJets.angleDirection • m

noncomputable def EulerPacketPressure.covector (k : ℝ) (m : EulerSmoothLimit.Space) (p : EulerPacketProfileRecursion.ScalarField) : EulerPacketProfileRecursion.VectorField

Covector, given by pressureGradient p + k • angularPressure m p.

Equations

• EulerPacketPressure.covector k m p = EulerPacketCylinderField.pressureGradient p + k • EulerPacketPressure.angularPressure m p

noncomputable def EulerPacketPressure.covectorGrades (N : ℕ) (m : EulerSmoothLimit.Space) (a : ℕ → EulerPacketProfileRecursion.Profile) : ℕ → EulerPacketProfileRecursion.VectorField

Covector grades, constructed using assemble.

Equations

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

noncomputable def EulerPacketPressure.gradientLinear : EulerPacketPointJets.ScalarJet →ₗ[ℝ] EulerSmoothLimit.Space

Gradient linear, bundling toFun, map_add, map_smul.

Equations

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

theorem EulerPacketPressure.gradientLinear_jet (p : EulerPacketProfileRecursion.ScalarField) (z : EulerPacketPointJets.Domain) : gradientLinear (EulerPacketPointJets.pressureJet p z) = EulerPacketCylinderField.pressureGradient p z

theorem EulerPacketPressure.fieldSum_assemble {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (N : ℕ) (κ : ℝ) (u c : ℕ → EulerPacketPointJets.Domain → E) (z : EulerPacketPointJets.Domain) : EulerPacketPointJets.fieldSum (N + 1) κ (EulerFiniteGrades.assemble N u c) z = EulerPacketPointJets.fieldSum N κ u z + κ • EulerPacketPointJets.fieldSum N κ c z

theorem EulerPacketPressure.pressureJet_finite (N : ℕ) (κ : ℝ) (a : ℕ → EulerPacketProfileRecursion.Profile) (z : EulerPacketPointJets.Domain) (hm : ∀ i ≤ N, DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => (a i).meanPressure (z.1, y)) z.2) (hh : ∀ i ≤ N, DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => (a i).highPressure (z.1, y)) z.2) : EulerPacketPointJets.pressureJet (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledPressure N a)) z = (EulerFiniteGrades.evaluate N κ fun (i : ℕ) => EulerPacketPointJets.pressureJet (a i).meanPressure z) + κ • EulerFiniteGrades.evaluate N κ fun (i : ℕ) => EulerPacketPointJets.pressureJet (a i).highPressure z

theorem EulerPacketPressure.covector_finite (N : ℕ) (κ : ℝ) (hκ : κ ≠ 0) (m : EulerSmoothLimit.Space) (a : ℕ → EulerPacketProfileRecursion.Profile) (z : EulerPacketPointJets.Domain) (hm : ∀ i ≤ N, DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => (a i).meanPressure (z.1, y)) z.2) (hh : ∀ i ≤ N, DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => (a i).highPressure (z.1, y)) z.2) (hangle : ∀ i ≤ N, (EulerPacketPointJets.pressureJet (a i).meanPressure z).2 EulerPacketPointJets.angleDirection = 0) : covector κ⁻¹ m (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledPressure N a)) z = EulerPacketPointJets.fieldSum (N + 1) κ (covectorGrades N m a) z

theorem EulerPacketPressure.gradient_graph_covector (k : ℝ) (m : EulerSmoothLimit.Space) (p : EulerPacketProfileRecursion.ScalarField) (t : ℝ) (x : EulerSmoothLimit.Space) (hp : DifferentiableAt ℝ (fun (z : EulerSmoothLimit.Space × ℝ) => p (t, z)) ((EulerGraphPullback.graphMap k m) x)) : gradient (fun (y : EulerSmoothLimit.Space) => p (t, y, k * inner ℝ m y)) x = covector k m p (t, x, k * inner ℝ m x)

theorem EulerPacketPressure.gradient_physical_covector (k : ℝ) (m : EulerSmoothLimit.Space) (p : EulerPacketProfileRecursion.ScalarField) (t : ℝ) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (J : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hY : HasFDerivAt Y J x) (hp : DifferentiableAt ℝ (fun (z : EulerSmoothLimit.Space × ℝ) => p (t, z)) ((EulerGraphPullback.graphMap k m) (Y x))) : gradient (fun (y : EulerSmoothLimit.Space) => p (t, Y y, k * inner ℝ m (Y y))) x = (ContinuousLinearMap.adjoint J) (covector k m p (t, Y x, k * inner ℝ m (Y x)))