Ordinary spatial smoothness, finite energy, and the pointwise time equation follow from the independent Comparator solution class.

theorem Euler.EulerExistenceAndSmoothnessR3.velocity_contDiff {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (t : ℝ) (ht : 0 ≤ t) : ContDiff ℝ ↑⊤ fun (x : EuclideanSpace ℝ (Fin 3)) => v x t

theorem Euler.EulerExistenceAndSmoothnessR3.pressure_contDiff {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (t : ℝ) (ht : 0 ≤ t) : ContDiff ℝ ↑⊤ fun (x : EuclideanSpace ℝ (Fin 3)) => p x t

theorem Euler.EulerExistenceAndSmoothnessR3.velocity_memLp {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (t : ℝ) (ht : 0 ≤ t) : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) 2 MeasureTheory.volume

theorem Euler.EulerExistenceAndSmoothnessR3.pointwise_euler {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (x : EuclideanSpace ℝ (Fin 3)) (t : ℝ) (ht : 0 < t) : HasDerivAt (fun (x_1 : ℝ) => v x x_1) (-(fderiv ℝ (fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) x) (v x t) - gradient (fun (x : EuclideanSpace ℝ (Fin 3)) => p x t) x) t