A uniform bound for the regularized pairing derivative #
After the spatial integrations by parts, the time derivative of the pairing
of a regularized velocity with a fixed smooth solenoidal test involves only
the velocity and the transport velocity, without derivatives. Their L²
bounds therefore control it uniformly, as in the proof of
lem:reg-equicontinuity.
theorem
CKN.Leray.lerayHopfLimit_abs_integral_mul_le_half_sq
{f g : Foundation.Parabolic.Vec3 → ℝ}
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
(hg : MeasureTheory.MemLp g 2 MeasureTheory.volume)
:
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => f x * g x) MeasureTheory.volume ∧ |∫ (x : Foundation.Parabolic.Vec3), f x * g x| ≤ ((∫ (x : Foundation.Parabolic.Vec3), f x ^ 2) + ∫ (x : Foundation.Parabolic.Vec3), g x ^ 2) / 2
The elementary estimate |∫ f g| ≤ (∫ f² + ∫ g²) / 2.
theorem
CKN.Leray.lerayHopfLimit_memLp_two_of_compact
{c : Foundation.Parabolic.Vec3 → ℝ}
(hc : Continuous c)
(hcc : HasCompactSupport c)
:
A continuous compactly supported field is square integrable.
theorem
CKN.Leray.lerayHopfLimit_pairing_rhs_bound
(w : Fin 3 → Foundation.Parabolic.Vec3 → ℝ)
(hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (w i))
(hwc : ∀ (i : Fin 3), HasCompactSupport (w i))
(B : ℝ)
:
∃ (K : ℝ),
0 ≤ K ∧ ∀ (f J : Fin 3 → Foundation.Parabolic.Vec3 → ℝ),
(∀ (i : Fin 3), MeasureTheory.MemLp (f i) 2 MeasureTheory.volume) →
(∀ (j : Fin 3), MeasureTheory.MemLp (J j) 2 MeasureTheory.volume) →
(∀ (i : Fin 3), ∫ (x : Foundation.Parabolic.Vec3), f i x ^ 2 ≤ B ^ 2) →
(∀ (j : Fin 3), ∫ (x : Foundation.Parabolic.Vec3), J j x ^ 2 ≤ B ^ 2) →
|∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3,
∑ j : Fin 3,
(f i x * spatialDeriv (spatialDeriv (w i) j) j x + f i x * J j x * spatialDeriv (w i) j x)| ≤ K
The pairing derivative after the spatial integrations by parts is bounded
by a constant depending only on the test and on the L² bounds of the
velocity and the transport velocity.