A genuine compact scalar cylinder path supplies the actual lifted pressure-gradient Field and belongs to the closed lifted gradient space.

noncomputable def EulerPacketPressure.rawGradient (κ : ℝ) (m : EulerSmoothLimit.Space) (p : EulerPacketProfileRecursion.ScalarField) (z : EulerPacketPointJets.Domain) : EulerSmoothLimit.Space

Raw gradient, given by κ • pressureGradient p z + (pressureJet p z).2 angleDirection • m.

Equations

• EulerPacketPressure.rawGradient κ m p z = κ • EulerPacketCylinderField.pressureGradient p z + (EulerPacketPointJets.pressureJet p z).2 EulerPacketPointJets.angleDirection • m

theorem EulerPacketPressure.rawGradient_cover (P κ : ℝ) (m : EulerSmoothLimit.Space) (p : EulerPacketProfileRecursion.ScalarField) (φ : EulerLiftedGradientSpace.LiftDomain P → ℝ) (t : ℝ) (he : ∀ (x : EulerSmoothLimit.Space) (θ : ℝ), p (t, x, θ) = φ (x, ↑θ)) (x : EulerSmoothLimit.Space) (θ : ℝ) : rawGradient κ m p (t, x, θ) = EulerLiftedGradientSpace.liftedGradient P κ m φ (x, ↑θ)

noncomputable def EulerPacketPressure.angularGradientField (P : ℝ) [Fact (0 < P)] {T : ℝ} (p : EulerPacketProfileRecursion.ScalarField) (q : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), p (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P q hq t (x, ↑θ)) (m : EulerSmoothLimit.Space) : EulerPacketCylinderField.Field P T fun (z : EulerPacketPointJets.Domain) => (EulerPacketPointJets.pressureJet p z).2 EulerPacketPointJets.angleDirection • m

Angular gradient field as an element of Field P T (fun z => (pressureJet p z).2 angleDirection • m).

Equations

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

noncomputable def EulerPacketPressure.liftedGradientField (P : ℝ) [Fact (0 < P)] {T : ℝ} (p : EulerPacketProfileRecursion.ScalarField) (q : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), p (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P q hq t (x, ↑θ)) (κ : ℝ) (m : EulerSmoothLimit.Space) : EulerPacketCylinderField.Field P T (rawGradient κ m p)

Lifted gradient field, given by ((scalarGradientField p q hq he).smul κ).add (angularGradientField P p q hq he m).

Equations

• EulerPacketPressure.liftedGradientField P p q hq he κ m = ((EulerPacketCylinderField.scalarGradientField p q hq he).smul κ).add (EulerPacketPressure.angularGradientField P p q hq he m)

theorem EulerPacketPressure.scalarPointField_compact (P : ℝ) [Fact (0 < P)] {T : ℝ} (p : EulerPacketProfileRecursion.ScalarField) (q : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), p (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P q hq t (x, ↑θ)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (hz : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∉ S, ∀ (θ : ℝ), p (↑t, x, θ) = 0) (t : ↑(Set.Icc 0 T)) : HasCompactSupport (EulerCylinderScalarPrimitive.scalarPointField P q hq t)

theorem EulerPacketPressure.liftedGradientField_mem (P : ℝ) [Fact (0 < P)] {T : ℝ} (p : EulerPacketProfileRecursion.ScalarField) (q : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), p (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P q hq t (x, ↑θ)) (κ : ℝ) (m : EulerSmoothLimit.Space) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (hz : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∉ S, ∀ (θ : ℝ), p (↑t, x, θ) = 0) (t : ↑(Set.Icc 0 T)) : (liftedGradientField P p q hq he κ m).path t ∈ EulerLiftedGradientSpace.gradientSpace P κ m

noncomputable def EulerPacketCoordinates.compactPressureField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (hk : k ≠ 0) (p : EulerPacketProfileRecursion.ScalarField) (q : C(↑(Set.Icc 0 D.T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (he : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), p (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P q hq t (x, ↑θ)) : EulerPacketCylinderField.Field P D.T (coordinatePressure D k p)

Compact pressure field as an element of Field P D.T (coordinatePressure D k p).

Equations

• EulerPacketCoordinates.compactPressureField D k hk p q hq he = ((EulerPacketPressure.liftedGradientField P p q hq he k⁻¹ D.m₀).smul (k ^ 2)).congr ⋯

theorem EulerPacketCoordinates.compactPressureField_mem {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (k : ℝ) (hk : k ≠ 0) (p : EulerPacketProfileRecursion.ScalarField) (q : C(↑(Set.Icc 0 D.T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (he : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), p (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P q hq t (x, ↑θ)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (hz : ∀ (t : ↑(Set.Icc 0 D.T)), ∀ x ∉ S, ∀ (θ : ℝ), p (↑t, x, θ) = 0) (t : ↑(Set.Icc 0 D.T)) : (compactPressureField D k hk p q hq he).path t ∈ EulerLiftedGradientSpace.gradientSpace P k⁻¹ D.m₀