Odd prescribed velocity gives an odd actual Picard flow and inverse. The symmetry is proved by uniqueness of the genuine ODE solution.

theorem EulerBoundedLipschitzFlow.Data.flow_odd {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (ho : ∀ (t : ℝ), Function.Odd (V.velocity t)) (s t : ℝ) : Function.Odd (V.flow s t)

theorem EulerBoundedLipschitzFlow.Data.forward_odd {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (ho : ∀ (t : ℝ), Function.Odd (V.velocity t)) (t : ℝ) : Function.Odd (V.forward t)

theorem EulerBoundedLipschitzFlow.Data.backward_odd {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (ho : ∀ (t : ℝ), Function.Odd (V.velocity t)) (t : ℝ) : Function.Odd (V.backward t)

theorem EulerSmoothBanachFlow.forward_odd {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (ho : ∀ (t : ↑(Set.Icc 0 T)), Function.Odd ⇑(A.field t)) (t : ℝ) : Function.Odd ((flowData T hT A).forward t)

theorem EulerSmoothBanachFlow.backward_odd {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (ho : ∀ (t : ↑(Set.Icc 0 T)), Function.Odd ⇑(A.field t)) (t : ℝ) : Function.Odd ((flowData T hT A).backward t)