The transport velocity J_ε u of a continuous field #
The transport velocity of thm:regularised is the spatial convolution of the
velocity with a smooth compactly supported kernel. When the velocity is
continuous on ℝ³ × (0,∞) and has square-integrable slices, the transport
velocity is continuous there, and it is bounded by the integral of the kernel
times any bound of the velocity slice.
theorem
CKN.Leray.regR12_convolution_continuousOn
{κ : Foundation.Parabolic.Vec3 → ℝ}
{S : Set (Foundation.Parabolic.Vec3 × ℝ)}
{F : Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hκ : Continuous κ)
(hκc : HasCompactSupport κ)
(hF : ContinuousOn F S)
(hSshift : ∀ z ∈ S, ∀ (y : Foundation.Parabolic.Vec3), (z.1 - y, z.2) ∈ S)
:
ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => ∫ (y : Foundation.Parabolic.Vec3), F (z.1 - y, z.2) * κ y) S
A spatial convolution in a space-time field with a continuous compactly supported kernel is continuous on every translation-invariant set.
theorem
CKN.Leray.regR12Kernel_mollifier_continuous
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
:
Continuous fun (y : Foundation.Parabolic.Vec3) => regMollifierKernel ρ ε hε (WithLp.toLp 2 y)
theorem
CKN.Leray.regR12Kernel_mollifier_compact
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
:
HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => regMollifierKernel ρ ε hε (WithLp.toLp 2 y)
theorem
CKN.Leray.regR12_mollifiedVelocity_eq_integral
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(t : ℝ)
(hSlice : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume)
(x : Foundation.Parabolic.Vec3)
(i : Fin 3)
:
regUniformMollifiedVelocity ρ ε hε u (x, t) i = ∫ (y : Foundation.Parabolic.Vec3), u (x - y, t) i * regMollifierKernel ρ ε hε (WithLp.toLp 2 y)
The transport velocity as a spatial convolution.
theorem
CKN.Leray.regR12_mollifiedVelocity_continuousOn
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(hSlice :
∀ (t : ℝ), 0 < t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume)
(hU : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => u z i) (Set.univ ×ˢ Set.Ioi 0))
(i : Fin 3)
:
ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => regUniformMollifiedVelocity ρ ε hε u z i)
(Set.univ ×ˢ Set.Ioi 0)
The transport velocity of a velocity continuous on ℝ³ × (0,∞) with
square-integrable slices is continuous there.
theorem
CKN.Leray.regR12_mollifiedVelocity_abs_le
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(t : ℝ)
(hSlice : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume)
(B : ℝ)
(hB : ∀ (x : Foundation.Parabolic.Vec3) (i : Fin 3), |u (x, t) i| ≤ B)
(x : Foundation.Parabolic.Vec3)
(i : Fin 3)
:
|regUniformMollifiedVelocity ρ ε hε u (x, t) i| ≤ B * ∫ (y : Foundation.Parabolic.Vec3), |regMollifierKernel ρ ε hε (WithLp.toLp 2 y)|
The transport velocity is bounded by the integral of the kernel times a bound of the velocity slice.