The actual finite source packet satisfies the lifted L² constraint #
The terminal corrector is retained in the finite assembly. Each genuine Piola pair and every inverse-frame mean belongs to the same closed constraint space.
noncomputable def
EulerPacketCylinderField.sourcePacketPullbackField
(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)
(N : ℕ)
(κ : ℝ)
:
Field P M.T fun (z : EulerPacketPointJets.Domain) =>
((sourceOperators P M D I).inverseFrame z)
(EulerPacketPointJets.fieldSum (N + 1) κ
(EulerPacketProfileRecursion.assembledVelocity N (sourceProfiles P M D I Iprimary)) z)
Source packet pullback field as an element of Field P M.T (fun z => (sourceOperators P M D I).inverseFrame z (fieldSum (N+1) κ (assembledVelocity N (sourceProfiles P M D I Iprimary)) z)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketCylinderField.sourcePacketPullbackField_path
(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)
(N : ℕ)
(κ : ℝ)
:
(sourcePacketPullbackField P M D hT I Iprimary N κ).path = ∑ i ∈ Finset.range N,
((sourcePairField P M D hT I Iprimary κ (i + 1)).path + κ ^ (i + 1) • (sourceMeanPullbackField P M D hT I Iprimary (i + 1)).path)
theorem
EulerPacketCylinderField.sourcePacketPullbackField_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)
(N : ℕ)
(κ : ℝ)
(t : ↑(Set.Icc 0 M.T))
(Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hΞ : ContDiff ℝ (↑⊤) Ξ)
(hF : ∀ (x : EulerSmoothLimit.Space), fderiv ℝ Ξ x = (D.F.field (sourceTime M D hT t)) x)
(hdet :
∀ (x : EulerSmoothLimit.Space),
Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field (sourceTime M D hT t)) x)) = 1)
:
(sourcePacketPullbackField P M D hT I Iprimary N κ).path t ∈ EulerLiftedGradientSpace.divergenceFreeSpace P κ D.m₀