The independent solution to the unforced Euler Comparator challenge.
Its definitions come from SolutionDefinitions, never from the reference
module or its placeholder theorem.
Compact smooth data satisfy the independent challenge's rapid-decay condition.
theorem
Euler.initialVelocityConditionDecay_of_compact
(u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3))
(hs : ContDiff ℝ (↑⊤) u₀)
(hc : HasCompactSupport u₀)
(hd : ∀ (x : EuclideanSpace ℝ (Fin 3)), divergence u₀ x = 0)
:
theorem
Euler.euler_breakdown_R3 :
∃ (u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)),
InitialVelocityConditionDecay u₀ ∧ ¬∃ (v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) (p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ),
EulerExistenceAndSmoothnessR3 u₀ v p
Smooth, rapidly decaying, divergence-free Euler data admitting no global smooth solution with uniformly bounded kinetic energy.
theorem
Euler.exists_compact_smooth_euler_singularity :
∃ (u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (Tstar : ℝ) (v :
EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) (p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ),
InitialVelocityConditionDecay u₀ ∧ HasCompactSupport u₀ ∧ u₀ ≠ 0 ∧ 0 < Tstar ∧ Tstar ≤ 1 ∧ EulerSobolevExistenceAndSmoothnessR3On (Set.Ico 0 Tstar) u₀ v p ∧ (∃ (E : ℝ), ∀ t ∈ Set.Ico 0 Tstar, ∫ (x : EuclideanSpace ℝ (Fin 3)), ‖v x t‖ ^ 2 < E) ∧ (∀ (T : ℝ),
0 < T →
((∃ (w : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) (q :
EuclideanSpace ℝ (Fin 3) → ℝ → ℝ),
EulerSobolevExistenceAndSmoothnessR3On (Set.Icc 0 T) u₀ w q) ↔ T < Tstar)) ∧ (∀ T ∈ Set.Ioo 0 Tstar,
(⨆ t ∈ Set.Icc 0 T, velocityC1Norm fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) < ⊤ ∧ (∫⁻ (t : ℝ) in Set.Ico 0 T, vorticityNorm fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) < ⊤) ∧ Filter.limsup (fun (t : ℝ) => velocityC1Norm fun (x : EuclideanSpace ℝ (Fin 3)) => v x t)
(nhdsWithin Tstar (Set.Iio Tstar)) = ⊤ ∧ (∫⁻ (t : ℝ) in Set.Ico 0 Tstar, vorticityNorm fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) = ⊤ ∧ ¬∃ (w : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) (q :
EuclideanSpace ℝ (Fin 3) → ℝ → ℝ), EulerExistenceAndSmoothnessR3 u₀ w q
Compactly supported smooth Euler data with a finite maximal Sobolev lifespan. At the terminal time, the velocity C¹ norm has infinite left limsup and the time integral of the vorticity supremum diverges. The solution has uniformly bounded kinetic energy throughout its lifespan and admits no global smooth continuation with that energy bound.