The final statement for the concrete packet construction. The initial velocity is an ordinary compactly supported smooth field on Euclidean three-space. Its maximal solution has a positive finite lifespan, a divergent C¹ upper limit, and an infinite integral of the actual curl supremum. All packet, scale, local existence, continuation, and logarithmic estimate inputs have been constructed in the imported proofs.

Evolution.sobolevSolutionClass supplies one continuous strong time derivative in every spatial Sobolev order for every shorter restriction. The norm specification theorems below identify the quantities in the statement with the pointwise suprema of the actual velocity, derivative, and curl.

The genuine zero Euler solution rules out zero initial data for a positive finite maximal lifespan.

noncomputable def EulerOrdinarySobolev.zeroEvolution (T : ℝ) (hT : 0 ≤ T) : Evolution T hT

The identically zero unforced incompressible Euler solution on any nonnegative closed time interval, with identically zero pressure force.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerOrdinarySobolev.zero_has_euler (T : ℝ) (hT : 0 < T) : HasEulerEvolution EulerLpTranslation.SmoothL2Field.zeroField T

theorem EulerOrdinarySobolev.FiniteLifespan.initial_nonzero {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : A.field ≠ 0

A finite maximal lifespan cannot have identically zero initial data.

def EulerOrdinarySobolev.HasScalarEulerEvolution (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (T : ℝ) : Prop

Scalar-pressure Euler on the closed interval [0,T], with the ordinary all-order spatial and strong time regularity. No pressure-force path or pressure norm is prescribed. The maximal solution itself is on [0,T*).

Equations

• One or more equations did not get rendered due to their size.

theorem EulerOrdinarySobolev.hasScalarEulerEvolution_iff (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (T : ℝ) : HasScalarEulerEvolution A T ↔ HasEulerEvolution A T

theorem EulerOrdinarySobolev.FiniteLifespan.hasEulerEvolution_iff {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (T : ℝ) : HasEulerEvolution A T ↔ 0 < T ∧ T < L.duration

The maximal duration is exactly the upper endpoint of the positive closed intervals on which an ordinary smooth Euler evolution exists.

theorem EulerOrdinarySobolev.FiniteLifespan.hasScalarEulerEvolution_iff {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (T : ℝ) : HasScalarEulerEvolution A T ↔ 0 < T ∧ T < L.duration

noncomputable def EulerPacketInduction.maximalVorticityNorm (t : MaximalTime) : ℝ

Maximal vorticity norm, given by lifespan.maximalVorticityNorm t.

Equations

• EulerPacketInduction.maximalVorticityNorm t = EulerPacketInduction.lifespan.maximalVorticityNorm t

noncomputable def EulerPacketInduction.maximalVorticityDensity (r : ℝ) : ℝ

Maximal vorticity density, given by lifespan.maximalVorticityDensity r.

Equations

• EulerPacketInduction.maximalVorticityDensity r = EulerPacketInduction.lifespan.maximalVorticityDensity r

noncomputable def EulerPacketInduction.maximalVorticityIntegral (t : MaximalTime) : ℝ

Maximal vorticity integral, given by lifespan.maximalVorticityIntegral t.

Equations

• EulerPacketInduction.maximalVorticityIntegral t = EulerPacketInduction.lifespan.maximalVorticityIntegral t

theorem EulerPacketInduction.maximalVorticityNorm_spec (t : MaximalTime) (K : ℝ) : maximalVorticityNorm t ≤ K ↔ ∀ (x : EulerSmoothLimit.Space), ‖EulerMeanCutoffCurl.vectorCurl (maximalVelocity t) x‖ ≤ K

theorem EulerPacketInduction.maximalVorticityDensity_spec (t : MaximalTime) : maximalVorticityDensity ↑t = maximalVorticityNorm t

theorem EulerPacketInduction.maximalVorticityIntegral_spec (t : MaximalTime) : ∫ (r : ℝ) in 0..↑t, maximalVorticityDensity r = maximalVorticityIntegral t

theorem EulerPacketInduction.initialDatum_nonzero : initialDatum.field ≠ 0

theorem EulerPacketInduction.initialDatum_existence_iff (T : ℝ) : HasSmoothEulerSolution initialDatum.field T ↔ 0 < T ∧ T < lifespan.duration

theorem EulerPacketInduction.initialDatum_scalar_existence_iff (T : ℝ) : EulerOrdinarySobolev.HasScalarEulerEvolution initialDatum T ↔ 0 < T ∧ T < lifespan.duration

theorem EulerPacketInduction.maximalVorticityIntegral_tendsto : Filter.Tendsto maximalVorticityIntegral (Filter.comap (fun (t : MaximalTime) => ↑t) (nhdsWithin lifespan.duration (Set.Iio lifespan.duration))) Filter.atTop

theorem EulerPacketInduction.maximalVorticity_integral_infinite : ∫⁻ (r : ℝ) in Set.Ico 0 lifespan.duration, ENNReal.ofReal (maximalVorticityDensity r) = ⊤

theorem EulerPacketInduction.initialDatum_singularity : ContDiff ℝ (↑⊤) initialDatum.field ∧ HasCompactSupport initialDatum.field ∧ initialDatum.field ≠ 0 ∧ (∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence initialDatum.field x = 0) ∧ 0 < lifespan.duration ∧ lifespan.duration ≤ 1 ∧ (∀ (T : ℝ), HasSmoothEulerSolution initialDatum.field T ↔ 0 < T ∧ T < lifespan.duration) ∧ Filter.limsup (fun (t : MaximalTime) => ENNReal.ofReal (maximalC1Norm t)) (Filter.comap (fun (t : MaximalTime) => ↑t) (nhdsWithin lifespan.duration (Set.Iio lifespan.duration))) = ⊤ ∧ ∫⁻ (r : ℝ) in Set.Ico 0 lifespan.duration, ENNReal.ofReal (maximalVorticityDensity r) = ⊤

The two breakdown conclusions for the actual constructed datum and the actual maximal smooth solution. No unproved estimate is a premise.

theorem EulerPacketInduction.exists_compact_smooth_euler_singularity : ∃ (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (L : EulerOrdinarySobolev.FiniteLifespan A), ContDiff ℝ (↑⊤) A.field ∧ HasCompactSupport A.field ∧ A.field ≠ 0 ∧ (∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence A.field x = 0) ∧ 0 < L.duration ∧ L.duration ≤ 1 ∧ (∀ (T : ℝ), EulerOrdinarySobolev.HasScalarEulerEvolution A T ↔ 0 < T ∧ T < L.duration) ∧ L.maximalVelocity L.initialTime = A.field ∧ (∀ (S : ℝ) (hS : 0 < S) (hSL : S < L.duration), ∃ (U : EulerOrdinarySobolev.Evolution S ⋯), (U.velocity = fun (t : ↑(Set.Icc 0 S)) => L.maximalField (L.shorterTime S hSL t)) ∧ (U.pressureForce = fun (t : ↑(Set.Icc 0 S)) => L.maximalPressureField (L.shorterTime S hSL t)) ∧ U.velocity ⟨0, ⋯⟩ = A) ∧ Filter.limsup (fun (t : L.Time) => ENNReal.ofReal (L.maximalC1Norm t)) (Filter.comap (fun (t : L.Time) => ↑t) (nhdsWithin L.duration (Set.Iio L.duration))) = ⊤ ∧ ∫⁻ (r : ℝ) in Set.Ico 0 L.duration, ENNReal.ofReal (L.maximalVorticityDensity r) = ⊤

An existential form of the manuscript's claim. Every restriction of the one maximal field is an actual Euler evolution. Its time and space regularity, scalar pressure, and norm meanings are proved in the imported ordinary-Euler interfaces, rather than assumed as construction inputs.