Solution-side definitions for the Euler Comparator challenge

Adapted from FormalConjectures/Millenium/NavierStokes.lean at https://github.com/google-deepmind/formal-conjectures/blob/8323e878b83fcd7f4a448256069352a265460d75/FormalConjectures/Millenium/NavierStokes.lean

This is the whole-space breakdown alternative specialized to zero viscosity and zero external force. It retains the source's initial-data decay, joint smoothness, square integrability, and uniform energy conditions. Velocity and pressure take position before time. The time derivative at zero is taken within [0,∞).

These definitions reproduce the independent reference exactly. This module contains no challenge theorem or proof placeholder and does not import Euler.

noncomputable def Euler.divergence (v : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (x : EuclideanSpace ℝ (Fin 3)) : ℝ

The divergence of a vector field, computed as the trace of its derivative.

Equations

• Euler.divergence v x = (LinearMap.trace ℝ (EuclideanSpace ℝ (Fin 3))) ↑(fderiv ℝ v x)

structure Euler.InitialVelocityCondition (u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) : Prop

Smooth, divergence-free initial velocity.

• div_free (x : EuclideanSpace ℝ (Fin 3)) : divergence u₀ x = 0
• smooth : ContDiff ℝ (↑⊤) u₀

structure Euler.InitialVelocityConditionDecay (u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) extends Euler.InitialVelocityCondition u₀ : Prop

Every spatial derivative of the initial velocity decays faster than any polynomial.

• div_free (x : EuclideanSpace ℝ (Fin 3)) : divergence u₀ x = 0
• smooth : ContDiff ℝ (↑⊤) u₀
• decay (m : ℕ) (K : ℝ) : ∃ (C : ℝ), ∀ (x : EuclideanSpace ℝ (Fin 3)), ‖iteratedFDeriv ℝ m u₀ x‖ ≤ C / (1 + ‖x‖) ^ K

structure Euler.EulerExistenceAndSmoothness (u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) (p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ) : Prop

A global smooth solution of unforced incompressible Euler on ℝ³.

• euler (x : EuclideanSpace ℝ (Fin 3)) (t : ℝ) : t ≥ 0 → derivWithin (fun (x_1 : ℝ) => v x x_1) (Set.Ici 0) t + (fderiv ℝ (fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) x) (v x t) = -gradient (fun (x : EuclideanSpace ℝ (Fin 3)) => p x t) x

  ∂ₜv + (v · ∇)v = -∇p: viscosity and external force are both zero.

• div_free (x : EuclideanSpace ℝ (Fin 3)) (t : ℝ) : t ≥ 0 → divergence (fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) x = 0
• initial_condition (x : EuclideanSpace ℝ (Fin 3)) : v x 0 = u₀ x
• velocity_smooth : ContDiffOn ℝ (↑⊤) (Function.uncurry v) (Set.univ ×ˢ Set.Ici 0)
• pressure_smooth : ContDiffOn ℝ (↑⊤) (Function.uncurry p) (Set.univ ×ˢ Set.Ici 0)

structure Euler.EulerExistenceAndSmoothnessR3 (u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) (p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ) extends Euler.EulerExistenceAndSmoothness u₀ v p : Prop

The whole-space solution class, retaining the source's finite, uniformly bounded energy.

• euler (x : EuclideanSpace ℝ (Fin 3)) (t : ℝ) : t ≥ 0 → derivWithin (fun (x_1 : ℝ) => v x x_1) (Set.Ici 0) t + (fderiv ℝ (fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) x) (v x t) = -gradient (fun (x : EuclideanSpace ℝ (Fin 3)) => p x t) x
• div_free (x : EuclideanSpace ℝ (Fin 3)) (t : ℝ) : t ≥ 0 → divergence (fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) x = 0
• initial_condition (x : EuclideanSpace ℝ (Fin 3)) : v x 0 = u₀ x
• velocity_smooth : ContDiffOn ℝ (↑⊤) (Function.uncurry v) (Set.univ ×ˢ Set.Ici 0)
• pressure_smooth : ContDiffOn ℝ (↑⊤) (Function.uncurry p) (Set.univ ×ˢ Set.Ici 0)
• integrable (t : ℝ) : t ≥ 0 → MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin 3)) => ‖v x t‖) 2 MeasureTheory.volume
• globally_bounded_energy : ∃ (E : ℝ), ∀ t ≥ 0, ∫ (x : EuclideanSpace ℝ (Fin 3)), ‖v x t‖ ^ 2 < E

noncomputable def Euler.toL2 {V : Type u_1} [NormedAddCommGroup V] (f : EuclideanSpace ℝ (Fin 3) → V) : ↥(MeasureTheory.Lp V 2 MeasureTheory.volume)

The L² equivalence class of a square-integrable function. The fallback makes this a total function; the solution conditions require square integrability wherever it is used.

Equations

• Euler.toL2 f = if h : MeasureTheory.MemLp f 2 MeasureTheory.volume then MeasureTheory.MemLp.toLp f h else 0

structure Euler.SobolevSmoothOn (I : Set ℝ) (v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) : Prop

A spatially smooth path whose actual spatial derivative tensors belong to L² and depend continuously on time in L², at every finite order.

• spatial_smooth (t : ℝ) : t ∈ I → ContDiff ℝ ↑⊤ fun (x : EuclideanSpace ℝ (Fin 3)) => v x t
• integrable (t : ℝ) : t ∈ I → MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) 2 MeasureTheory.volume
• jets_integrable (m : ℕ) (t : ℝ) : t ∈ I → MeasureTheory.MemLp (iteratedFDeriv ℝ m fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) 2 MeasureTheory.volume
• continuous : ContinuousOn (fun (t : ℝ) => toL2 fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) I
• jets_continuous (m : ℕ) : ContinuousOn (fun (t : ℝ) => toL2 (iteratedFDeriv ℝ m fun (x : EuclideanSpace ℝ (Fin 3)) => v x t)) I

structure Euler.EulerSobolevExistenceAndSmoothnessR3On (I : Set ℝ) (u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) (p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ) : Prop

Scalar-pressure Euler on a time set I in the original theorem's smooth Sobolev class. The velocity and its strong time derivative have continuous L² spatial jets of every order. The Euler equation uses this derivative witness.

As in IsSmoothScalarEuler, the time law and scalar-pressure equation are required at interior times. There is no endpoint derivative condition. We use Ico 0 T for a maximal lifespan and Icc 0 T for a closed interval.

• div_free (x : EuclideanSpace ℝ (Fin 3)) (t : ℝ) : t ∈ I → divergence (fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) x = 0
• initial_condition (x : EuclideanSpace ℝ (Fin 3)) : v x 0 = u₀ x
• velocity_smooth : SobolevSmoothOn I v
• pressure_differentiable (t : ℝ) : t ∈ interior I → Differentiable ℝ fun (x : EuclideanSpace ℝ (Fin 3)) => p x t
• euler : ∃ (w : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)), SobolevSmoothOn I w ∧ (∀ t ∈ interior I, HasDerivAt (fun (s : ℝ) => toL2 fun (x : EuclideanSpace ℝ (Fin 3)) => v x s) (toL2 fun (x : EuclideanSpace ℝ (Fin 3)) => w x t) t) ∧ ∀ (x : EuclideanSpace ℝ (Fin 3)), ∀ t ∈ interior I, w x t + (fderiv ℝ (fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) x) (v x t) = -gradient (fun (x : EuclideanSpace ℝ (Fin 3)) => p x t) x

noncomputable def Euler.vorticity (v : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (x : EuclideanSpace ℝ (Fin 3)) : EuclideanSpace ℝ (Fin 3)

The ordinary curl of a velocity field, expressed through its spatial derivative. Indices in Fin 3 are cyclic.

Equations

• Euler.vorticity v x = WithLp.toLp 2 fun (i : Fin 3) => ((fderiv ℝ v x) (EuclideanSpace.single (i + 1) 1)).ofLp (i + 2) - ((fderiv ℝ v x) (EuclideanSpace.single (i + 2) 1)).ofLp (i + 1)

noncomputable def Euler.velocityC1Norm (v : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) : ENNReal

The sum of the spatial suprema of the velocity norm and derivative operator norm.

Equations

• Euler.velocityC1Norm v = (⨆ (x : EuclideanSpace ℝ (Fin 3)), ENNReal.ofReal ‖v x‖) + ⨆ (x : EuclideanSpace ℝ (Fin 3)), ENNReal.ofReal ‖fderiv ℝ v x‖

noncomputable def Euler.vorticityNorm (v : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) : ENNReal

The spatial supremum of the Euclidean norm of the actual vorticity.

Equations

• Euler.vorticityNorm v = ⨆ (x : EuclideanSpace ℝ (Fin 3)), ENNReal.ofReal ‖Euler.vorticity v x‖