The canonical maximal solution in the reference's ordinary-function Sobolev class. All regularity is inherited from its existing shorter evolutions.

The canonical maximal fields in the challenge's position-first, real-time convention. Extension by zero outside the lifespan has no role in the equation.

The extended spatial suprema in the independent challenge agree with the ordinary development's bounded-function norms on every smooth Sobolev slice.

theorem Euler.ComparatorBridge.vorticity_eq_vectorCurl (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hu : ContDiff ℝ (↑⊤) u) : vorticity u = EulerMeanCutoffCurl.vectorCurl u

theorem Euler.ComparatorBridge.iSup_ofReal_norm_boundedContinuousFunction {X : Type u_1} {V : Type u_2} [TopologicalSpace X] [NormedAddCommGroup V] (f : BoundedContinuousFunction X V) : ⨆ (x : X), ENNReal.ofReal ‖f x‖ = ENNReal.ofReal ‖f‖

theorem Euler.ComparatorBridge.velocityC1Norm_eq (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : velocityC1Norm A.field = ENNReal.ofReal (‖EulerMeanSobolevBoundedField.finiteField A‖ + ‖EulerMeanSobolevBoundedField.finiteField A.derivative‖)

theorem Euler.ComparatorBridge.vorticityNorm_eq (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : vorticityNorm A.field = ENNReal.ofReal (EulerOrdinarySobolev.vorticityNorm A)

noncomputable def Euler.ComparatorBridge.maximalVelocityExtension {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (x : EulerSmoothLimit.Space) (t : ℝ) : EulerSmoothLimit.Space

Maximal velocity extension, with branches according to ht : t ∈ Ico (0 : ℝ) L.duration.

Equations

• Euler.ComparatorBridge.maximalVelocityExtension L x t = if ht : t ∈ Set.Ico 0 L.duration then L.maximalVelocity ⟨t, ht⟩ x else 0

noncomputable def Euler.ComparatorBridge.maximalPressureExtension {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (x : EulerSmoothLimit.Space) (t : ℝ) : ℝ

Maximal pressure extension, with branches according to ht : t ∈ Ico (0 : ℝ) L.duration.

Equations

• Euler.ComparatorBridge.maximalPressureExtension L x t = if ht : t ∈ Set.Ico 0 L.duration then L.maximalPressure ⟨t, ht⟩ x else 0

theorem Euler.ComparatorBridge.maximalVelocityExtension_eq {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (t : L.Time) : (fun (x : EulerSmoothLimit.Space) => maximalVelocityExtension L x ↑t) = L.maximalVelocity t

theorem Euler.ComparatorBridge.maximalPressureExtension_eq {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (t : L.Time) : (fun (x : EulerSmoothLimit.Space) => maximalPressureExtension L x ↑t) = L.maximalPressure t

theorem Euler.ComparatorBridge.maximalVelocityExtension_initial {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) : (fun (x : EulerSmoothLimit.Space) => maximalVelocityExtension L x 0) = A.field

theorem Euler.ComparatorBridge.maximalVelocityExtension_memLp {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (t : ℝ) (ht : t ∈ Set.Ico 0 L.duration) : MeasureTheory.MemLp (fun (x : EulerSmoothLimit.Space) => maximalVelocityExtension L x t) 2 MeasureTheory.volume

theorem Euler.ComparatorBridge.maximalVelocityExtension_divergence {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (t : ℝ) (ht : t ∈ Set.Ico 0 L.duration) (x : EulerSmoothLimit.Space) : divergence (fun (x : EuclideanSpace ℝ (Fin 3)) => maximalVelocityExtension L x t) x = 0

theorem Euler.ComparatorBridge.velocityC1Norm_maximal {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (t : L.Time) : (velocityC1Norm fun (x : EuclideanSpace ℝ (Fin 3)) => maximalVelocityExtension L x ↑t) = ENNReal.ofReal (L.maximalC1Norm t)

theorem Euler.ComparatorBridge.vorticityNorm_maximal {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (t : L.Time) : (vorticityNorm fun (x : EuclideanSpace ℝ (Fin 3)) => maximalVelocityExtension L x ↑t) = ENNReal.ofReal (L.maximalVorticityNorm t)

theorem Euler.ComparatorBridge.vorticityNorm_maximal_density {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (t : ℝ) (ht : t ∈ Set.Ico 0 L.duration) : (vorticityNorm fun (x : EuclideanSpace ℝ (Fin 3)) => maximalVelocityExtension L x t) = ENNReal.ofReal (L.maximalVorticityDensity t)

theorem Euler.ComparatorBridge.maximalField_kineticEnergy {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (t : L.Time) : ‖(L.maximalField t).toLp‖ ^ 2 = ‖A.toLp‖ ^ 2

theorem Euler.ComparatorBridge.maximalVelocityExtension_energy {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (t : ℝ) (ht : t ∈ Set.Ico 0 L.duration) : ∫ (x : EulerSmoothLimit.Space), ‖maximalVelocityExtension L x t‖ ^ 2 = ‖A.toLp‖ ^ 2

theorem Euler.ComparatorBridge.maximalVelocityExtension_bounded_energy {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) : ∃ (E : ℝ), ∀ t ∈ Set.Ico 0 L.duration, ∫ (x : EulerSmoothLimit.Space), ‖maximalVelocityExtension L x t‖ ^ 2 < E

theorem Euler.ComparatorBridge.maximalVelocityExtension_c1_locally_bounded {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (S : ℝ) (_hS : 0 < S) (hSL : S < L.duration) : (⨆ t ∈ Set.Icc 0 S, velocityC1Norm fun (x : EuclideanSpace ℝ (Fin 3)) => maximalVelocityExtension L x t) < ⊤

theorem Euler.ComparatorBridge.maximalVelocityExtension_vorticity_locally_integrable {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) : (∫⁻ (t : ℝ) in Set.Ico 0 S, vorticityNorm fun (x : EuclideanSpace ℝ (Fin 3)) => maximalVelocityExtension L x t) < ⊤

theorem Euler.ComparatorBridge.maximalVelocityExtension_c1_limsup {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) : Filter.limsup (fun (t : ℝ) => velocityC1Norm fun (x : EuclideanSpace ℝ (Fin 3)) => maximalVelocityExtension L x t) (nhdsWithin L.duration (Set.Iio L.duration)) = ⊤

theorem Euler.ComparatorBridge.maximalVelocityExtension_vorticity_integral {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) : (∫⁻ (t : ℝ) in Set.Ico 0 L.duration, vorticityNorm fun (x : EuclideanSpace ℝ (Fin 3)) => maximalVelocityExtension L x t) = ⊤

noncomputable def Euler.ComparatorBridge.maximalDerivativeField {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (t : L.Time) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Maximal derivative field, given by eulerRhs (L.maximalField t) (L.maximalPressureField t).

Equations

• Euler.ComparatorBridge.maximalDerivativeField L t = EulerOrdinarySobolev.eulerRhs (L.maximalField t) (L.maximalPressureField t)

theorem Euler.ComparatorBridge.maximalDerivativeField_eq_evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)) : maximalDerivativeField L (L.shorterTime S hSL t) = (L.evolution S hS hSL).derivative t

theorem Euler.ComparatorBridge.maximalDerivativeField_jet_continuous {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (n : ℕ) : Continuous fun (t : L.Time) => (maximalDerivativeField L t).jetLp n

noncomputable def Euler.ComparatorBridge.maximalDerivativeExtension {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (x : EulerSmoothLimit.Space) (t : ℝ) : EulerSmoothLimit.Space

Maximal derivative extension, with branches according to ht : t ∈ Ico (0 : ℝ) L.duration.

Equations

• Euler.ComparatorBridge.maximalDerivativeExtension L x t = if ht : t ∈ Set.Ico 0 L.duration then (Euler.ComparatorBridge.maximalDerivativeField L ⟨t, ht⟩).field x else 0

theorem Euler.ComparatorBridge.maximalDerivativeExtension_eq {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (t : L.Time) : (fun (x : EulerSmoothLimit.Space) => maximalDerivativeExtension L x ↑t) = (maximalDerivativeField L t).field

theorem Euler.ComparatorBridge.maximalVelocityExtension_eq_evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)) : (fun (x : EulerSmoothLimit.Space) => maximalVelocityExtension L x ↑t) = ((L.evolution S hS hSL).velocity t).field

theorem Euler.ComparatorBridge.maximalVelocityExtension_sobolevSmooth {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) : SobolevSmoothOn (Set.Ico 0 L.duration) (maximalVelocityExtension L)

theorem Euler.ComparatorBridge.maximalDerivativeExtension_sobolevSmooth {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) : SobolevSmoothOn (Set.Ico 0 L.duration) (maximalDerivativeExtension L)

theorem Euler.ComparatorBridge.maximalVelocityExtension_hasDerivAt {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (t : ℝ) (ht : t ∈ Set.Ioo 0 L.duration) : HasDerivAt (fun (s : ℝ) => toL2 fun (x : EuclideanSpace ℝ (Fin 3)) => maximalVelocityExtension L x s) (toL2 fun (x : EuclideanSpace ℝ (Fin 3)) => maximalDerivativeExtension L x t) t

theorem Euler.ComparatorBridge.maximal_sobolevSolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) : EulerSobolevExistenceAndSmoothnessR3On (Set.Ico 0 L.duration) A.field (maximalVelocityExtension L) (maximalPressureExtension L)

theorem Euler.ComparatorBridge.maximal_sobolev_existence_iff {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) (T : ℝ) (hT : 0 < T) : (∃ (v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) (p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ), EulerSobolevExistenceAndSmoothnessR3On (Set.Icc 0 T) A.field v p) ↔ T < L.duration