Every positive-time slice of the Leray limit is square integrable #
The limit field of prop:leray-limit is defined at positive times by the
iterated mollified limits of eq:leray-limit-representative. At a fixed
positive time, the regularized slices are bounded in L² and converge weakly
against every L² field, so this representative agrees almost everywhere
with the weak L² limit. In particular every positive-time slice of the
limit is square integrable, as used in the proof of prop:leray-hopf-limit.
theorem
CKN.Leray.lerayHopfLimit_inner_toLp_eq
{f g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
(hg : MeasureTheory.MemLp g 2 MeasureTheory.volume)
:
inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (f x)) ⋯)
(MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (g x)) ⋯) = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, f x i * g x i
The pairing of two coordinate L² fields through their Euclidean
representatives.
theorem
CKN.Leray.lerayHopfLimit_slice_memLp_of_representative
(Useq : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3)
(σ : ℕ → ℕ)
(hσ : Filter.Tendsto σ Filter.atTop Filter.atTop)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(t : ℝ)
(hrep : ∀ (x : Foundation.Parabolic.Vec3), u (x, t) = compactnessMollifiedLimit Useq σ (x, t))
(hslice : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Useq n (x, t)) 2 MeasureTheory.volume)
(B : ℝ)
(hB : 0 ≤ B)
(hbound :
∀ (n : ℕ), ‖MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (Useq n (x, t))) ⋯‖ ≤ B)
(hweak :
∀ (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3),
MeasureTheory.MemLp w 2 MeasureTheory.volume →
Filter.Tendsto (fun (n : ℕ) => ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, Useq n (x, t) i * w x i)
Filter.atTop (nhds (∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * w x i)))
:
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume
A slice of the iterated mollified limit is square integrable when the
regularized slices at that time are uniformly bounded in L² and converge
weakly to it against every L² field.