The ordinary Euler vorticity blowup criterion, with the whole-space logarithmic estimate proved and instantiated. No spatial estimate or unboundedness assumption remains in these conclusions.

Reduction of the vorticity blowup criterion to the whole-space logarithmic gradient inequality. The geometric inequality remains an explicit hypothesis here and is discharged by the kernel argument.

The scalar part of the vorticity continuation argument. A genuine logarithmic gradient estimate bounds the gradient integral using only the time integral of its continuous vorticity coefficient.

noncomputable def EulerOrdinarySobolev.logEnergyBase (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ℝ

Log energy base, given by exp 1+wordCount 3*sqrt (wordEnergy 3 A).

Equations

• EulerOrdinarySobolev.logEnergyBase A = Real.exp 1 + EulerOrdinarySobolev.wordCount 3 * √(EulerOrdinarySobolev.wordEnergy 3 A)

theorem EulerOrdinarySobolev.logEnergyBase_pos (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : 0 < logEnergyBase A

noncomputable def EulerOrdinarySobolev.logarithmicGronwallConstant (C : ℝ) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ℝ

Logarithmic gronwall constant, given by C*(1+‖A.toLp‖+logEnergyBase A+gradientEnergyConstant).

Equations

• EulerOrdinarySobolev.logarithmicGronwallConstant C A = C * (1 + ‖A.toLp‖ + EulerOrdinarySobolev.logEnergyBase A + EulerOrdinarySobolev.gradientEnergyConstant)

theorem EulerOrdinarySobolev.logarithmicGronwallConstant_nonneg (C : ℝ) (hC : 0 ≤ C) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : 0 ≤ logarithmicGronwallConstant C A

theorem EulerOrdinarySobolev.Evolution.logarithmic_h3_bound {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : Real.log (Real.exp 1 + tensorNorm 3 (U.velocity t)) ≤ logEnergyBase (U.velocity ⟨0, ⋯⟩) + gradientEnergyConstant * U.gradientIntegral t

theorem EulerOrdinarySobolev.Evolution.gradient_logarithmic_envelope {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (C : ℝ) (hC : 0 ≤ C) (W : C(↑(Set.Icc 0 T), ℝ)) (hW : ∀ (t : ↑(Set.Icc 0 T)), 0 ≤ W t) (hlog : ∀ (t : ↑(Set.Icc 0 T)), U.gradientNormPath t ≤ C * (1 + ‖(U.velocity t).toLp‖ + W t * Real.log (Real.exp 1 + tensorNorm 3 (U.velocity t)))) (t : ↑(Set.Icc 0 T)) : U.gradientNormPath t ≤ logarithmicGronwallConstant C (U.velocity ⟨0, ⋯⟩) * (1 + W t) * (1 + U.gradientIntegral t)

theorem EulerOrdinarySobolev.Evolution.gradientIntegral_logarithmic_bound {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (C : ℝ) (hC : 0 ≤ C) (W : C(↑(Set.Icc 0 T), ℝ)) (hW : ∀ (t : ↑(Set.Icc 0 T)), 0 ≤ W t) (hlog : ∀ (t : ↑(Set.Icc 0 T)), U.gradientNormPath t ≤ C * (1 + ‖(U.velocity t).toLp‖ + W t * Real.log (Real.exp 1 + tensorNorm 3 (U.velocity t)))) (t : ↑(Set.Icc 0 T)) : 1 + U.gradientIntegral t ≤ Real.exp (logarithmicGronwallConstant C (U.velocity ⟨0, ⋯⟩) * (↑t + EulerContinuousTimeIntegral.realIntegral T hT W ↑t))

theorem EulerOrdinarySobolev.Evolution.gradientIntegral_logarithmic_uniform {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (C : ℝ) (hC : 0 ≤ C) (W : C(↑(Set.Icc 0 T), ℝ)) (hW : ∀ (t : ↑(Set.Icc 0 T)), 0 ≤ W t) (hlog : ∀ (t : ↑(Set.Icc 0 T)), U.gradientNormPath t ≤ C * (1 + ‖(U.velocity t).toLp‖ + W t * Real.log (Real.exp 1 + tensorNorm 3 (U.velocity t)))) (Tmax G : ℝ) (hTmax : T ≤ Tmax) (hG : ∀ (t : ↑(Set.Icc 0 T)), EulerContinuousTimeIntegral.realIntegral T hT W ↑t ≤ G) (t : ↑(Set.Icc 0 T)) : U.gradientIntegral t ≤ Real.exp (logarithmicGronwallConstant C (U.velocity ⟨0, ⋯⟩) * (Tmax + G))

theorem EulerOrdinarySobolev.Evolution.gradientIntegral_of_vorticity_bound (C : ℝ) (hC : 0 ≤ C) (hlog : ∀ (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (W : ℝ), A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace → (∀ (x : EulerSmoothLimit.Space), ‖EulerMeanCutoffCurl.vectorCurl A.field x‖ ≤ W) → ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ C * (1 + ‖A.toLp‖ + W * Real.log (Real.exp 1 + tensorNorm 3 A))) {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (Tmax G : ℝ) (hTmax : T ≤ Tmax) (hG : ∀ (t : ↑(Set.Icc 0 T)), U.vorticityIntegral t ≤ G) (t : ↑(Set.Icc 0 T)) : U.gradientIntegral t ≤ Real.exp (logarithmicGronwallConstant C (U.velocity ⟨0, ⋯⟩) * (Tmax + G))

theorem EulerOrdinarySobolev.FiniteLifespan.vorticity_unbounded_of_logarithmic (C : ℝ) (hC : 0 ≤ C) (hlog : ∀ (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (W : ℝ), A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace → (∀ (x : EulerSmoothLimit.Space), ‖EulerMeanCutoffCurl.vectorCurl A.field x‖ ≤ W) → ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ C * (1 + ‖A.toLp‖ + W * Real.log (Real.exp 1 + tensorNorm 3 A))) {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).vorticityIntegral t

theorem EulerOrdinarySobolev.FiniteLifespan.vorticityIntegral_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).vorticityIntegral t

Genuine partial vorticity integrals exceed every finite bound.

theorem EulerOrdinarySobolev.FiniteLifespan.vorticityIntegral_tendsto_atTop {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Filter.Tendsto L.maximalVorticityIntegral Filter.atTop Filter.atTop

The actual partial integrals tend to infinity as time approaches the maximal lifespan from below.

theorem EulerOrdinarySobolev.FiniteLifespan.vorticity_lintegral_eq_top {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : ∫⁻ (r : ℝ) in Set.Ico 0 L.duration, ENNReal.ofReal (L.maximalVorticityDensity r) = ⊤

The true nonnegative vorticity supremum has infinite integral on the half-open maximal lifespan. This is an extended integral, so divergence is not obscured by the convention for nonintegrable real integrals.