The energy inequality for the Leray–Hopf limit #

This is the energy clause (LH4) of def:leray-hopf in the proof of prop:leray-hopf-limit. The regularized energy equality of thm:regularised bounds the slice energy plus twice the dissipation by the energy of the mollified data, hence by the energy of the data. The weak convergence of the slices and of the gradients then passes this bound to the limit by weak lower semicontinuity of the two Hilbert norms, in the form of the elementary inequality 2ab - b² ≤ a².

source

theorem CKN.Leray.lerayHopfLimit_lintegral_euclidean_sq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {g : α → Foundation.Parabolic.Vec3} (hg : MeasureTheory.MemLp g 2 μ) :

∫⁻ (x : α), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (g x)) ^ 2 ∂μ = ENNReal.ofReal (∑ i : Fin 3, ∫ (x : α), g x i ^ 2 ∂μ)

The squared Euclidean energy of a square-integrable coordinate field.

source

theorem CKN.Leray.lerayHopfLimit_eLpNorm_toLp_sq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {g : α → Foundation.Parabolic.Vec3} (hg : MeasureTheory.MemLp g 2 μ) :

MeasureTheory.eLpNorm (fun (x : α) => WithLp.toLp 2 (g x)) 2 μ ^ 2 = ENNReal.ofReal (∑ i : Fin 3, ∫ (x : α), g x i ^ 2 ∂μ)

The squared L² norm of the Euclidean representative of a coordinate field.

source

theorem CKN.Leray.lerayHopfLimit_eLpNorm_spatialField {f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) :

MeasureTheory.eLpNorm (regUniformSpatialField f) 2 MeasureTheory.volume = MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (f x)) 2 MeasureTheory.volume

The Euclidean L² norm of a coordinate field is unchanged by passing to the Euclidean carrier of the spatial variable.

source

theorem CKN.Leray.lerayHopfLimit_dissipation_eq_setLIntegral (U : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (t₀ : ℝ) :

regUniformDissipation U D t₀ = ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), ENNReal.ofReal (spatialGradientSq U D z)

The regularized dissipation up to time t₀ is the dissipation integral over the slab ℝ³ × (0,t₀).

source

theorem CKN.Leray.lerayHopfLimit_aestronglyMeasurable_of_slabs {f : Foundation.Parabolic.ParabolicPoint → ℝ} {t₀ : ℝ} (ht₀ : 0 < t₀) (h : ∀ (δ : ℝ), 0 < δ → δ < t₀ → MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ t₀)))) :

MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 t₀)))

Measurability on every positive-time slab gives measurability on the slab reaching the initial time.

source

theorem CKN.Leray.lerayHopfLimit_two_mul_integral_sub_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) :

MeasureTheory.Integrable (fun (x : α) => f x * g x) μ ∧ 2 * ∫ (x : α), f x * g x ∂μ - ∫ (x : α), g x ^ 2 ∂μ ≤ ∫ (x : α), f x ^ 2 ∂μ

The elementary weak lower semicontinuity inequality 2 ∫ f g - ∫ g² ≤ ∫ f², together with the integrability of f g.

source

(∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), u (x, t₀) i ^ 2) + 2 * ∑ i : Fin 3, ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), Du z i j ^ 2 ≤ ∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), a x i ^ 2

The energy inequality of the limit at a positive time, in real form: the slice energy plus twice the dissipation up to that time is bounded by the energy of the data.

source

(ENNReal.ofReal (1 / 2) * ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, t₀))) ^ 2) + ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 t₀), ENNReal.ofReal (spatialGradientSq u Du z) ≤ ENNReal.ofReal (1 / 2) * ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (a x)) ^ 2

The real energy inequality gives the energy clause (LH4) at a positive time.

source

Filter.Tendsto (fun (t : ℝ) => ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, t) - a x)) ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The initial trace clause (LH5): the energy bound and weak continuity at the initial time give strong L² convergence to the data.

Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.LerayHopfLimitPropEnergyIneq

The energy inequality for the Leray–Hopf limit #