Reg Uniform Momentum

Supporting estimates for the Navier–Stokes development.

@[instance_reducible]

def CKN.Leray.instNormedAddCommGroupParabolicPoint : NormedAddCommGroup Foundation.Parabolic.ParabolicPoint

The product normed additive group structure on the parabolic space-time carrier.

Equations

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

@[instance_reducible]

noncomputable def CKN.Leray.instNormedSpaceRealParabolicPoint : NormedSpace ℝ Foundation.Parabolic.ParabolicPoint

The real normed-space structure on the parabolic space-time carrier.

Equations

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

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

The physical-space kernel for the uniform regularized convolution estimate.

Equations

• CKN.Leray.regUniformPhysicalKernel ρ ε hε x = CKN.Leray.regMollifierKernel ρ ε hε (WithLp.toLp 2 x)

theorem CKN.Leray.regUniform_mollified_velocity_continuousOn (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {S : Set (Foundation.Parabolic.Vec3 × ℝ)} (hSlice : ∀ (t : ℝ), 0 < t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hU : ∀ (i : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) S) (hSpositive : ∀ z ∈ S, 0 < z.2) (hSshift : ∀ z ∈ S, ∀ (y : Foundation.Parabolic.Vec3), (z.1 - y, z.2) ∈ S) (i : Fin 3) : ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => regUniformMollifiedVelocity ρ ε hε u z i) S

Spatial convolution of a regularized velocity is continuous on positive time.

theorem CKN.Leray.regUniform_mollified_velocity_spatialPartial_continuousOn (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {S : Set (Foundation.Parabolic.Vec3 × ℝ)} (hSlice : ∀ (t : ℝ), 0 < t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hU : ∀ (i : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) S) (hSpositive : ∀ z ∈ S, 0 < z.2) (hSshift : ∀ z ∈ S, ∀ (y : Foundation.Parabolic.Vec3), (z.1 - y, z.2) ∈ S) (i j : Fin 3) : ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regUniformMollifiedVelocity ρ ε hε u y i) j z) S

Spatial derivatives of the regularized transport velocity are continuous on positive time.

theorem CKN.Leray.regUniform_weakDivFree_contDiff_divergence_eq_zero {f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hC1 : ∀ (i : Fin 3), ContDiff ℝ 1 fun (x : Foundation.Parabolic.Vec3) => f x i) (hdiv : IsWeakDivFreeL2 f) (x : Foundation.Parabolic.Vec3) : ∑ i : Fin 3, (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => f y i) x) (basisVec i) = 0

A continuously differentiable weakly divergence-free field has zero classical divergence at every point.

theorem CKN.Leray.regUniform_mollified_velocity_divergence_eq_zero (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (t : ℝ) (hdiv : IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => u (x, t)) (x : Foundation.Parabolic.Vec3) : ∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regUniformMollifiedVelocity ρ ε hε u y j) j (x, t) = 0

The regularized transport velocity is classically divergence free on each positive-time slice.