Uniform energy bounds for regularized solutions

The energy equality in thm:regularised controls every time slice and the full positive-time dissipation, uniformly in the regularization parameter.

def CKN.Leray.regUniformSpatialField (f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3

The spatial L² field represented by a CKN vector-valued function.

Equations

• CKN.Leray.regUniformSpatialField f x = WithLp.toLp 2 (f x.ofLp)

def CKN.Leray.regUniformVelocitySlice (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (t : ℝ) : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3

A time slice of the velocity, represented on the Euclidean spatial carrier.

Equations

• CKN.Leray.regUniformVelocitySlice u t x = WithLp.toLp 2 (u (x.ofLp, t))

noncomputable def CKN.Leray.regUniformMollifiedInitial (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The mollified initial velocity as a pointwise CKN vector field.

Equations

• CKN.Leray.regUniformMollifiedInitial ρ ε hε a x = (CKN.Leray.regMollifyVector ρ ε hε (CKN.Leray.regUniformSpatialField a) (WithLp.toLp 2 x)).ofLp

noncomputable def CKN.Leray.regUniformMollifiedVelocity (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3

The regularized transport velocity J_ε u on positive-time slices.

Equations

• CKN.Leray.regUniformMollifiedVelocity ρ ε hε u z = (CKN.Leray.regMollifyVector ρ ε hε (CKN.Leray.regUniformVelocitySlice u z.2) (WithLp.toLp 2 z.1)).ofLp

noncomputable def CKN.Leray.regUniformPositiveTimeMeasure : MeasureTheory.Measure Foundation.Parabolic.ParabolicPoint

Lebesgue measure on all positive space-time, used for global energy bounds.

Equations

• CKN.Leray.regUniformPositiveTimeMeasure = MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioi 0))

noncomputable def CKN.Leray.regUniformDissipation (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (T : ℝ) : ENNReal

Dissipation up to time T, measured on the positive-time carrier.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.regUniform_energy_bounds (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (ha : MeasureTheory.MemLp (regUniformSpatialField a) 2 MeasureTheory.volume) (hR5 : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.eLpNorm (regUniformVelocitySlice u t) 2 MeasureTheory.volume ^ 2 + 2 * regUniformDissipation u Du t = MeasureTheory.eLpNorm (regMollifyVector ρ ε hε (regUniformSpatialField a)) 2 MeasureTheory.volume ^ 2) (hDuMeasurable : Measurable Du) : (∀ (t : ℝ), 0 ≤ t → MeasureTheory.eLpNorm (regUniformVelocitySlice u t) 2 MeasureTheory.volume ^ 2 ≤ MeasureTheory.eLpNorm (regUniformSpatialField a) 2 MeasureTheory.volume ^ 2) ∧ 2 * ∫⁻ (z : Foundation.Parabolic.ParabolicPoint), ENNReal.ofReal (spatialGradientSq u Du z) ∂regUniformPositiveTimeMeasure ≤ MeasureTheory.eLpNorm (regUniformSpatialField a) 2 MeasureTheory.volume ^ 2

The energy equality in thm:regularised implies the uniform slice-energy bound and the full positive-time dissipation bound.

theorem CKN.Leray.regUniform_mollified_velocity_L2_bound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (t : ℝ) (hu : MeasureTheory.MemLp (regUniformVelocitySlice u t) 2 MeasureTheory.volume) : MeasureTheory.eLpNorm (regMollifyVector ρ ε hε (regUniformVelocitySlice u t)) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (regUniformVelocitySlice u t) 2 MeasureTheory.volume

The regularized transport field has no larger slice L² norm than the velocity, by the convolution contraction in lem:reg-mollifier-bounds.