Genuine continuation of every closed smooth Euler evolution, and the resulting gradient blowup criterion at a finite maximal horizon.

theorem EulerOrdinarySobolev.Evolution.exists_extension {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (hTpos : 0 < T) : ∃ (S : ℝ) (hS : 0 < S) (hTS : T < S) (V : Evolution S ⋯), V.velocity ⟨0, ⋯⟩ = U.velocity ⟨0, ⋯⟩ ∧ ∀ (t : ↑(Set.Icc 0 T)), V.velocity ⟨↑t, ⋯⟩ = U.velocity t

theorem EulerOrdinarySobolev.Evolution.gradientIntegral_mono {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (s t : ↑(Set.Icc 0 T)) (hst : ↑s ≤ ↑t) : U.gradientIntegral s ≤ U.gradientIntegral t

theorem EulerOrdinarySobolev.HasEulerEvolution.extend {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} {T : ℝ} (h : HasEulerEvolution A T) : ∃ (S : ℝ), T < S ∧ HasEulerEvolution A S

theorem EulerOrdinarySobolev.FiniteLifespan.no_endpoint {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : ¬HasEulerEvolution A L.duration

theorem EulerOrdinarySobolev.FiniteLifespan.gradientIntegral_unbounded {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (G : ℝ) : ∃ (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)), G < (L.evolution S hS hSL).gradientIntegral t

theorem EulerOrdinarySobolev.FiniteLifespan.gradient_unbounded {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (K : ℝ) : ∃ (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)) (x : EulerSmoothLimit.Space), K < ‖fderiv ℝ ((L.evolution S hS hSL).velocity t).field x‖

theorem EulerOrdinarySobolev.FiniteLifespan.evolution_agrees_at {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S T : ℝ) (hS : 0 < S) (hT : 0 < T) (hSL : S < L.duration) (hTL : T < L.duration) (t : ℝ) (ht0 : 0 ≤ t) (htS : t ≤ S) (htT : t ≤ T) : (L.evolution S hS hSL).velocity ⟨t, ⋯⟩ = (L.evolution T hT hTL).velocity ⟨t, ⋯⟩

theorem EulerOrdinarySobolev.FiniteLifespan.gradient_unbounded_near_endpoint {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (τ K : ℝ) (hτ : τ < L.duration) : ∃ (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)) (x : EulerSmoothLimit.Space), τ < ↑t ∧ K < ‖fderiv ℝ ((L.evolution S hS hSL).velocity t).field x‖

theorem EulerOrdinarySobolev.FiniteLifespan.gradientIntegral_agrees {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S T : ℝ) (hS : 0 < S) (hT : 0 < T) (hSL : S < L.duration) (hTL : T < L.duration) (hST : S ≤ T) (t : ↑(Set.Icc 0 S)) : (L.evolution S hS hSL).gradientIntegral t = (L.evolution T hT hTL).gradientIntegral ⟨↑t, ⋯⟩

theorem EulerOrdinarySobolev.FiniteLifespan.gradientIntegral_eventually_large {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (G : ℝ) : ∃ (R : ℝ) (_ : 0 < R) (_ : R < L.duration), ∀ (S : ℝ) (hS : 0 < S) (hSL : S < L.duration), R ≤ S → G < (L.evolution S hS hSL).gradientIntegral ⟨S, ⋯⟩