Oddness of actual cylinder paths is preserved by scalar multiplication, time identification, and multiplication by an even matrix coefficient.

@[reducible, inline]

abbrev EulerPacketCylinderField.Field.ReflectionOdd {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) : Prop

Reflection odd: an abbreviation for ∀ t : Icc (0 : ℝ) T, reflection P (G.path t) = -G.path t.

Equations

• G.ReflectionOdd = ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderFieldReflection.reflection P) (G.path t) = -G.path t

theorem EulerPacketCylinderField.Field.reflectionOdd_of_raw {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (h : JointOdd T raw) : G.ReflectionOdd

theorem EulerPacketCylinderField.Field.ReflectionOdd.raw_odd {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} (h : G.ReflectionOdd) : JointOdd T raw

theorem EulerPacketCylinderField.Field.ReflectionOdd.smul {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} (h : G.ReflectionOdd) (c : ℝ) : (G.smul c).ReflectionOdd

theorem EulerPacketCylinderField.Field.ReflectionOdd.changeTime {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} (h : G.ReflectionOdd) {T' : ℝ} (he : T = T') : (G.changeTime he).ReflectionOdd

theorem EulerPacketCylinderField.Field.ReflectionOdd.multiply {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} (h : G.ReflectionOdd) {a : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T a) (ha : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), a (↑t, -x, -θ) = a (↑t, x, θ)) : (A.multiply G).ReflectionOdd