A genuine L² evolution lifts to every ordinary Sobolev order when the proposed derivative has continuous actual spatial jets. Bounded Sobolev evaluation then supplies the classical pointwise time law.

theorem EulerOrdinarySobolev.instOrdinaryStrongTime1 : Fact (0 < 1)

theorem EulerOrdinarySobolev.sobolev_derivative_of_l2 (T : ℝ) (hT : 0 ≤ T) (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hB : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (B t).jetLp n) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => (A (Set.projIcc 0 T hT r)).toLp) (B ⟨t, ⋯⟩).toLp t) (q : ℕ) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerSmoothFieldSobolevTime.sobolevPath A hA q)) ((EulerSmoothFieldSobolevTime.sobolevPath B hB q) t) (Set.Icc 0 T) ↑t

theorem EulerOrdinarySobolev.pointwise_derivative_of_l2 (T : ℝ) (hT : 0 ≤ T) (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hB : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (B t).jetLp n) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => (A (Set.projIcc 0 T hT r)).toLp) (B ⟨t, ⋯⟩).toLp t) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (r : ℝ) => (A (Set.projIcc 0 T hT r)).field x) ((B t).field x) (Set.Icc 0 T) ↑t