The actual normalized transverse pressure supplies the literal next-grade pressure gradient.
The literal pressure integral is the genuine jointly continuous scalar path representative.
theorem
EulerSourceCylinderClassical.pressureField_eq_pointField
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(S : Set EulerSmoothLimit.Space)
(hS : MeasurableSet S)
(hSc : IsCompact S)
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS)))
(a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS))
(hf :
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f))
(ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀)
(M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space)
(cm : ℝ)
(hcm : 0 < cm)
(hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2)
(hf₀ : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0)
(ha₀zero : (EulerCylinderAngleAverage.average P) ↑a₀ = 0)
(t : ↑(Set.Icc 0 T))
:
pressureField P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m cm hcm hm hf₀ ha₀zero t = EulerCylinderScalarPrimitive.scalarPointField P
(EulerSourceCylinderEquation.pressurePath P S hS T hT Q Q₁ c hc hQ f a₀ M m cm hcm hm) ⋯ t
theorem
EulerSourceCylinderClassical.pressureField_joint_continuous
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(S : Set EulerSmoothLimit.Space)
(hS : MeasurableSet S)
(hSc : IsCompact S)
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS)))
(a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS))
(hf :
ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f))
(ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀)
(M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space)
(cm : ℝ)
(hcm : 0 < cm)
(hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2)
(hf₀ : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0)
(ha₀zero : (EulerCylinderAngleAverage.average P) ↑a₀ = 0)
:
Continuous fun (z : ↑(Set.Icc 0 T) × EulerLiftedGradientSpace.LiftDomain P) =>
pressureField P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m cm hcm hm hf₀ ha₀zero z.1 z.2
theorem
EulerTransversePacketProvider.Forcing.scalar_eq_pointField
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(I : InitialData P D)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
noncomputable def
EulerTransversePacketProvider.Forcing.scalarGradientField
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
(I : InitialData P D)
:
The next known-force pressure term comes from the constructed scalar pressure itself.
Equations
- G.scalarGradientField I = EulerPacketCylinderField.scalarGradientField (G.scalar I) (G.pressurePath I) ⋯ ⋯
Instances For
noncomputable def
EulerTransversePacketProvider.highSolvePressureGradientField
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : Data U)
(I : InitialData P D)
(raw : EulerPacketProfileRecursion.VectorField)
(h : Nonempty (Forcing P D raw))
:
EulerPacketCylinderField.Field P D.T (EulerPacketCylinderField.pressureGradient (highSolve P D I raw).2)
The total high operator has the required pressure-gradient witness on admissible forcing.
Equations
- EulerTransversePacketProvider.highSolvePressureGradientField P D I raw h = ((Classical.choice h).scalarGradientField I).congr ⋯