Actual finite packet velocities and residual tails preserve the joint odd parity of the constructed profiles.
theorem
EulerPacketCylinderField.JointOdd.smul
{T : ℝ}
{f : EulerPacketProfileRecursion.VectorField}
(hf : JointOdd T f)
(c : ℝ)
:
theorem
EulerPacketCylinderField.JointOdd.sum
{T : ℝ}
{ι : Type u_1}
(s : Finset ι)
(f : ι → EulerPacketProfileRecursion.VectorField)
(hf : ∀ i ∈ s, JointOdd T (f i))
:
JointOdd T fun (z : EulerPacketPointJets.Domain) => ∑ i ∈ s, f i z
theorem
EulerPacketCylinderField.JointOdd.matrix_apply
{T : ℝ}
{f : EulerPacketProfileRecursion.VectorField}
(hf : JointOdd T f)
(A : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(hA : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), A (↑t, -x, -θ) = A (↑t, x, θ))
:
JointOdd T fun (z : EulerPacketPointJets.Domain) => (A z) (f z)
theorem
EulerPacketCylinderField.JointOdd.truncate
{T : ℝ}
(N : ℕ)
(f : ℕ → EulerPacketProfileRecursion.VectorField)
(hf : ∀ i ≤ N, JointOdd T (f i))
(i : ℕ)
:
JointOdd T (EulerFiniteGrades.truncate N f i)
theorem
EulerPacketCylinderField.JointOdd.assemble
{T : ℝ}
(N : ℕ)
(f c : ℕ → EulerPacketProfileRecursion.VectorField)
(hf : ∀ i ≤ N, JointOdd T (f i))
(hc : ∀ i ≤ N, JointOdd T (c i))
(i : ℕ)
:
JointOdd T (EulerFiniteGrades.assemble N f c i)
theorem
EulerPacketCylinderField.JointOdd.fieldSum
{T : ℝ}
(N : ℕ)
(κ : ℝ)
(f : ℕ → EulerPacketProfileRecursion.VectorField)
(hf : ∀ i ≤ N, JointOdd T (f i))
:
JointOdd T (EulerPacketPointJets.fieldSum N κ f)
theorem
EulerPacketCylinderField.Field.linearPart_odd
{P T : ℝ}
[Fact (0 < P)]
{f ft : EulerPacketProfileRecursion.VectorField}
(G : Field P T f)
(Gt : Field P T ft)
(hT : 0 < T)
(hdt : TimeDerivative ⋯ G Gt)
(hf : JointOdd T f)
(M : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(hM : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), M (↑t, -x, -θ) = M (↑t, x, θ))
:
JointOdd T fun (z : EulerPacketPointJets.Domain) =>
(EulerPacketPointJets.linearPart (M z)) (EulerPacketPointJets.slicedJet (Set.Icc 0 T) f z)
theorem
EulerPacketCylinderField.slowPressure_odd
{T : ℝ}
(f : EulerPacketProfileRecursion.ScalarField)
(I : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(hf : JointOdd T (pressureGradient f))
(hI : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), I (↑t, -x, -θ) = I (↑t, x, θ))
:
JointOdd T fun (z : EulerPacketPointJets.Domain) =>
(EulerPacketPointJets.slowPressure (I z)) (EulerPacketPointJets.pressureJet f z)
theorem
EulerPacketCylinderField.PrefixFields.nonlinearGrade_odd
{P T : ℝ}
[Fact (0 < P)]
{O : EulerPacketProfileRecursion.Operators}
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(F : PrefixFields P T p a)
(H : PrefixOdd T p a)
(hp : 1 ≤ p)
(E : CoefficientEven T O)
(M n : ℕ)
:
JointOdd T fun (z : EulerPacketPointJets.Domain) =>
EulerPacketPointJets.nonlinearGrade M n (O.inverseFrame z) (O.normal z)
(EulerPacketProfileRecursion.knownJets O p a z)
theorem
EulerPacketCylinderField.ProfileParity.assembledVelocity_odd
{T : ℝ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{N : ℕ}
(H : ∀ i ≤ N, ProfileParity T (a i))
(i : ℕ)
:
theorem
EulerPacketCylinderField.ProfileParity.velocity_odd
{T : ℝ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{N : ℕ}
(H : ∀ i ≤ N, ProfileParity T (a i))
(κ : ℝ)
:
JointOdd T (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledVelocity N a))
theorem
EulerPacketCylinderField.ProfileRegularity.recursiveTail_odd
{P T : ℝ}
[Fact (0 < P)]
{O : EulerPacketProfileRecursion.Operators}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{N : ℕ}
{S : Set EulerSmoothLimit.Space}
(hT : 0 < T)
(G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ S (a i))
(H : ∀ i ≤ N, ProfileParity T (a i))
(C : CoefficientData P T O)
(E : CoefficientEven T O)
(ha : a 0 = 0)
(n : ℕ)
(hn : N + 1 ≤ n)
:
JointOdd T fun (z : EulerPacketPointJets.Domain) => EulerPacketProfileRecursion.recursiveGrade O N a z n
theorem
EulerPacketCylinderField.ProfileRegularity.residualTail_odd
{P T : ℝ}
[Fact (0 < P)]
{O : EulerPacketProfileRecursion.Operators}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{N : ℕ}
{S : Set EulerSmoothLimit.Space}
(hT : 0 < T)
(G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ S (a i))
(H : ∀ i ≤ N, ProfileParity T (a i))
(C : CoefficientData P T O)
(E : CoefficientEven T O)
(ha : a 0 = 0)
(κ : ℝ)
:
JointOdd T fun (z : EulerPacketPointJets.Domain) =>
∑ n ∈ Finset.Ico (N + 1) (2 * N + 3), κ ^ n • EulerPacketProfileRecursion.recursiveGrade O N a z n