The actual inverse-frame mean profiles satisfy the closed lifted divergence constraint.
theorem
EulerPacketCylinderField.Field.mem_divergenceFree_of_angleIndependent
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(t : ↑(Set.Icc 0 T))
(ha : ∀ (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = raw (↑t, x, 0))
(hd :
∀ (x : EulerSmoothLimit.Space),
EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => raw (↑t, y, 0)) x = 0)
:
noncomputable def
EulerPacketCylinderField.sourceMeanPullbackField
(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)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(p : ℕ)
:
Field P M.T fun (z : EulerPacketPointJets.Domain) =>
((sourceOperators P M D I).inverseFrame z) ((sourceProfiles P M D I Iprimary p).mean z)
Source mean pullback field, given by (sourceCoefficientData P M D I hT).inverse.multiply (sourceProfileWitness P M D hT I Iprimary p).mean.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketCylinderField.sourceMeanPullback_divergence
(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)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(A : SourceCoefficientAgreement M D)
(p : ℕ)
(t : ↑(Set.Icc 0 M.T))
(x : EulerSmoothLimit.Space)
:
EulerSmoothLimit.divergence
(fun (y : EulerSmoothLimit.Space) =>
((sourceOperators P M D I).inverseFrame (↑t, y, 0)) ((sourceProfiles P M D I Iprimary p).mean (↑t, y, 0)))
x = 0
theorem
EulerPacketCylinderField.sourceMeanPullbackField_mem
(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)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(A : SourceCoefficientAgreement M D)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(p : ℕ)
(t : ↑(Set.Icc 0 M.T))
:
(sourceMeanPullbackField P M D hT I Iprimary p).path t ∈ EulerLiftedGradientSpace.divergenceFreeSpace P κ m