Genuine ordinary vorticity fields, their continuous supremum norms, and actual time integrals. These are literal curls of the velocity.

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

Vorticity field, given by mapField curlOperator A.derivative.

Equations

• EulerOrdinarySobolev.vorticityField A = EulerLpTranslation.SmoothL2Field.mapField EulerPacketPiola.curlOperator A.derivative

theorem EulerOrdinarySobolev.vorticityField_apply (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : (vorticityField A).field x = EulerMeanCutoffCurl.vectorCurl A.field x

theorem EulerOrdinarySobolev.vorticityField_continuous {K : Type u_1} [TopologicalSpace K] (A : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (n : ℕ) : Continuous fun (t : K) => (vorticityField (A t)).jetLp n

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

Vorticity norm, given by ‖finiteField (vorticityField A)‖.

Equations

• EulerOrdinarySobolev.vorticityNorm A = ‖EulerMeanSobolevBoundedField.finiteField (EulerOrdinarySobolev.vorticityField A)‖

theorem EulerOrdinarySobolev.vorticityNorm_nonneg (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : 0 ≤ vorticityNorm A

theorem EulerOrdinarySobolev.vorticityNorm_le_iff (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K : ℝ) : vorticityNorm A ≤ K ↔ ∀ (x : EulerSmoothLimit.Space), ‖EulerMeanCutoffCurl.vectorCurl A.field x‖ ≤ K

theorem EulerOrdinarySobolev.vorticityNorm_continuous {K : Type u_1} [TopologicalSpace K] (A : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) : Continuous fun (t : K) => vorticityNorm (A t)

noncomputable def EulerOrdinarySobolev.Evolution.vorticityNormPath {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) : C(↑(Set.Icc 0 T), ℝ)

Vorticity norm path, given by ⟨fun t => vorticityNorm (U.velocity t),vorticityNorm_continuous U.velocity U.velocity_continuous⟩.

Equations

• U.vorticityNormPath = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerOrdinarySobolev.vorticityNorm (U.velocity t), continuous_toFun := ⋯ }

theorem EulerOrdinarySobolev.Evolution.vorticityNormPath_nonneg {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : 0 ≤ U.vorticityNormPath t

theorem EulerOrdinarySobolev.Evolution.vorticityNormPath_le_iff {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) (K : ℝ) : U.vorticityNormPath t ≤ K ↔ ∀ (x : EulerSmoothLimit.Space), ‖EulerMeanCutoffCurl.vectorCurl (U.velocity t).field x‖ ≤ K

theorem EulerOrdinarySobolev.Evolution.pointwise_vorticity_le {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ‖EulerMeanCutoffCurl.vectorCurl (U.velocity t).field x‖ ≤ U.vorticityNormPath t

noncomputable def EulerOrdinarySobolev.Evolution.vorticityIntegral {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : ℝ

Vorticity integral, given by realIntegral T hT U.vorticityNormPath t.

Equations

• U.vorticityIntegral t = EulerContinuousTimeIntegral.realIntegral T hT U.vorticityNormPath ↑t

theorem EulerOrdinarySobolev.Evolution.vorticityIntegral_nonneg {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : 0 ≤ U.vorticityIntegral t

theorem EulerOrdinarySobolev.Evolution.vorticityIntegral_initial {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) : U.vorticityIntegral ⟨0, ⋯⟩ = 0

theorem EulerOrdinarySobolev.Evolution.vorticityIntegral_continuous {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) : Continuous U.vorticityIntegral

theorem EulerOrdinarySobolev.Evolution.vorticityIntegral_mono {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (s t : ↑(Set.Icc 0 T)) (hst : ↑s ≤ ↑t) : U.vorticityIntegral s ≤ U.vorticityIntegral t

theorem EulerOrdinarySobolev.Evolution.vorticityIntegral_le_const {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (K : ℝ) (hK : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖EulerMeanCutoffCurl.vectorCurl (U.velocity t).field x‖ ≤ K) (t : ↑(Set.Icc 0 T)) : U.vorticityIntegral t ≤ K * ↑t

theorem EulerOrdinarySobolev.Evolution.vorticityNormPath_le_gradient {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : U.vorticityNormPath t ≤ ‖EulerPacketPiola.curlOperator‖ * U.gradientNormPath t