The actual nonnegative vorticity density of a maximal Euler solution has an infinite extended integral whenever its genuine partial vorticity integrals are unbounded. The only unboundedness input is the explicit family statement used by the BKM continuation argument.

Actual vorticity supremum norms and their partial integrals on a half-open maximal Euler interval. All quantities agree exactly with the genuine smooth solutions on every shorter closed interval.

theorem EulerOrdinarySobolev.FiniteLifespan.vorticityIntegral_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).vorticityIntegral t = (L.evolution T hT hTL).vorticityIntegral ⟨↑t, ⋯⟩

theorem EulerOrdinarySobolev.FiniteLifespan.vorticityIntegral_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).vorticityIntegral ⟨t, ⋯⟩ = (L.evolution T hT hTL).vorticityIntegral ⟨t, ⋯⟩

noncomputable def EulerOrdinarySobolev.FiniteLifespan.maximalVorticityNorm {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : ℝ

Maximal vorticity norm, given by vorticityNorm (L.maximalField t).

Equations

• L.maximalVorticityNorm t = EulerOrdinarySobolev.vorticityNorm (L.maximalField t)

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityNorm_nonneg {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : 0 ≤ L.maximalVorticityNorm t

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityNorm_le_iff {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) (K : ℝ) : L.maximalVorticityNorm t ≤ K ↔ ∀ (x : EulerSmoothLimit.Space), ‖EulerMeanCutoffCurl.vectorCurl (L.maximalVelocity t) x‖ ≤ K

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityNorm_continuous {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Continuous L.maximalVorticityNorm

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityNorm_eq_evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)) : L.maximalVorticityNorm (L.shorterTime S hSL t) = (L.evolution S hS hSL).vorticityNormPath t

noncomputable def EulerOrdinarySobolev.FiniteLifespan.maximalVorticityIntegral {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : ℝ

Maximal vorticity integral as an element of ℝ.

Equations

• L.maximalVorticityIntegral t = (L.evolution (L.intermediateHorizon t) ⋯ ⋯).vorticityIntegral (L.intermediateTime t)

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityIntegral_eq_evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)) : L.maximalVorticityIntegral (L.shorterTime S hSL t) = (L.evolution S hS hSL).vorticityIntegral t

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityIntegral_nonneg {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : 0 ≤ L.maximalVorticityIntegral t

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityIntegral_initial {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : L.maximalVorticityIntegral L.initialTime = 0

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityIntegral_continuous {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Continuous L.maximalVorticityIntegral

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityIntegral_mono {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Monotone L.maximalVorticityIntegral

theorem EulerOrdinarySobolev.FiniteLifespan.vorticityIntegral_eventually_large_of_unbounded {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (hunbounded : ∀ (G : ℝ), ∃ (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)), G < (L.evolution S hS hSL).vorticityIntegral t) (G : ℝ) : ∃ (R : ℝ) (_ : 0 < R) (_ : R < L.duration), ∀ (S : ℝ) (hS : 0 < S) (hSL : S < L.duration), R ≤ S → G < (L.evolution S hS hSL).vorticityIntegral ⟨S, ⋯⟩

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityIntegral_tendsto_atTop {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (hunbounded : ∀ (G : ℝ), ∃ (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)), G < (L.evolution S hS hSL).vorticityIntegral t) : Filter.Tendsto L.maximalVorticityIntegral Filter.atTop Filter.atTop

Unbounded finite partial integrals of a nonnegative function force its extended integral on the half-open interval to be infinite. Local integrability is explicit, so no totalized real integral is used as a substitute for an improper integral.

theorem EulerNonnegativeImproperIntegral.ofReal_partial_le_lintegral (f : ℝ → ℝ) {S T : ℝ} (hS : 0 ≤ S) (hST : S < T) (hf : IntervalIntegrable f MeasureTheory.volume 0 S) (hnonneg : ∀ x ∈ Set.Ioc 0 S, 0 ≤ f x) : ENNReal.ofReal (∫ (x : ℝ) in 0..S, f x) ≤ ∫⁻ (x : ℝ) in Set.Ico 0 T, ENNReal.ofReal (f x)

theorem EulerNonnegativeImproperIntegral.lintegral_eq_top_of_unbounded_partials (f : ℝ → ℝ) (T : ℝ) (hf : ∀ (S : ℝ), 0 < S → S < T → IntervalIntegrable f MeasureTheory.volume 0 S) (hnonneg : ∀ x ∈ Set.Ico 0 T, 0 ≤ f x) (hunbounded : ∀ (K : ℝ), ∃ (S : ℝ), 0 < S ∧ S < T ∧ K < ∫ (x : ℝ) in 0..S, f x) : ∫⁻ (x : ℝ) in Set.Ico 0 T, ENNReal.ofReal (f x) = ⊤

noncomputable def EulerOrdinarySobolev.FiniteLifespan.maximalVorticityDensity {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (r : ℝ) : ℝ

The true vorticity supremum on the lifespan, extended by zero only to make the ambient real-time integral available.

Equations

• L.maximalVorticityDensity r = if hr : r ∈ Set.Ico 0 L.duration then L.maximalVorticityNorm ⟨r, hr⟩ else 0

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityDensity_nonneg {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (r : ℝ) : 0 ≤ L.maximalVorticityDensity r

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityDensity_measurable {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Measurable L.maximalVorticityDensity

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityDensity_eq {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : L.maximalVorticityDensity ↑t = L.maximalVorticityNorm t

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityDensity_le_iff {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) (K : ℝ) : L.maximalVorticityDensity ↑t ≤ K ↔ ∀ (x : EulerSmoothLimit.Space), ‖EulerMeanCutoffCurl.vectorCurl (L.maximalVelocity t) x‖ ≤ K

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityDensity_eq_evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)) : L.maximalVorticityDensity ↑t = (L.evolution S hS hSL).vorticityNormPath t

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityDensity_continuousOn {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) : ContinuousOn L.maximalVorticityDensity (Set.Icc 0 S)

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityDensity_intervalIntegrable {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) : IntervalIntegrable L.maximalVorticityDensity MeasureTheory.volume 0 S

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityDensity_integral_eq_evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)) : ∫ (r : ℝ) in 0..↑t, L.maximalVorticityDensity r = (L.evolution S hS hSL).vorticityIntegral t

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticityDensity_integral_eq {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : ∫ (r : ℝ) in 0..↑t, L.maximalVorticityDensity r = L.maximalVorticityIntegral t

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVorticity_lintegral_eq_top {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (hunbounded : ∀ (G : ℝ), ∃ (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)), G < (L.evolution S hS hSL).vorticityIntegral t) : ∫⁻ (r : ℝ) in Set.Ico 0 L.duration, ENNReal.ofReal (L.maximalVorticityDensity r) = ⊤

This is the improper integral as an extended nonnegative integral, not the totalized real Bochner integral at the singular endpoint.