The actual spatial derivatives and nonlinear jet terms preserve joint odd velocity parity.

@[reducible, inline]

abbrev EulerPacketCylinderField.JointOdd (T : ℝ) (raw : EulerPacketProfileRecursion.VectorField) : Prop

Joint odd: an abbreviation for ∀ (t : Icc (0 : ℝ) T) x θ, raw (t,(-x,-θ)) = -raw (t,(x,θ)).

Equations

• EulerPacketCylinderField.JointOdd T raw = ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)

theorem EulerPacketCylinderField.JointOdd.zero (T : ℝ) : JointOdd T 0

theorem EulerPacketCylinderField.JointOdd.add {T : ℝ} {f g : EulerPacketProfileRecursion.VectorField} (hf : JointOdd T f) (hg : JointOdd T g) : JointOdd T (f + g)

theorem EulerPacketCylinderField.JointOdd.neg {T : ℝ} {f : EulerPacketProfileRecursion.VectorField} (hf : JointOdd T f) : JointOdd T (-f)

theorem EulerPacketCylinderField.JointOdd.sub {T : ℝ} {f g : EulerPacketProfileRecursion.VectorField} (hf : JointOdd T f) (hg : JointOdd T g) : JointOdd T (f - g)

theorem EulerPacketCylinderField.JointOdd.congr {T : ℝ} {f g : EulerPacketProfileRecursion.VectorField} (hf : JointOdd T f) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), g (↑t, x, θ) = f (↑t, x, θ)) : JointOdd T g

theorem EulerPacketCylinderField.Field.raw_fderiv_even_of_odd {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hodd : JointOdd T raw) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : fderiv ℝ (fun (y : EulerLiftedGradientSpace.LiftTangent) => raw (↑t, y)) (-x, -θ) = fderiv ℝ (fun (y : EulerLiftedGradientSpace.LiftTangent) => raw (↑t, y)) (x, θ)

theorem EulerPacketCylinderField.SpatialJetField.spatial_even_of_value_odd {P T : ℝ} [Fact (0 < P)] {K : EulerPacketPointJets.Domain → EulerPacketPointJets.VectorJet} (H : SpatialJetField P T K) (hK : JointOdd T fun (z : EulerPacketPointJets.Domain) => (K z).1) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) (v : EulerPacketPointJets.SpatialDomain) : (K (↑t, -x, -θ)).2 (0, v) = (K (↑t, x, θ)).2 (0, v)

theorem EulerPacketCylinderField.SpatialJetField.slowAdvection_odd {P T : ℝ} [Fact (0 < P)] {J K : EulerPacketPointJets.Domain → EulerPacketPointJets.VectorJet} (H : SpatialJetField P T K) (inverse : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hI : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inverse (↑t, -x, -θ) = inverse (↑t, x, θ)) (hJ : JointOdd T fun (z : EulerPacketPointJets.Domain) => (J z).1) (hK : JointOdd T fun (z : EulerPacketPointJets.Domain) => (K z).1) : JointOdd T fun (z : EulerPacketPointJets.Domain) => ((EulerPacketPointJets.slowAdvection (inverse z)) (J z)) (K z)

theorem EulerPacketCylinderField.SpatialJetField.fastAdvection_odd {P T : ℝ} [Fact (0 < P)] {J K : EulerPacketPointJets.Domain → EulerPacketPointJets.VectorJet} (H : SpatialJetField P T K) (normal : EulerPacketProfileRecursion.VectorField) (hN : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), normal (↑t, -x, -θ) = normal (↑t, x, θ)) (hJ : JointOdd T fun (z : EulerPacketPointJets.Domain) => (J z).1) (hK : JointOdd T fun (z : EulerPacketPointJets.Domain) => (K z).1) : JointOdd T fun (z : EulerPacketPointJets.Domain) => ((EulerPacketPointJets.fastAdvection (normal z)) (J z)) (K z)