The regularized transport velocity on one time slice

On each time slice the transport velocity J_ε u of thm:regularised is the spatial convolution of the velocity slice with the smooth compactly supported profile. It is therefore smooth, pointwise divergence-free when the slice is weakly divergence-free, and bounded in L² by the slice. These are the properties of J_ε u used in the proof of lem:reg-equicontinuity.

theorem CKN.Leray.lerayHopfLimit_integral_sq_eq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {h : α → ℝ} (hh : MeasureTheory.MemLp h 2 μ) : ∫ (x : α), h x ^ 2 ∂μ = (MeasureTheory.eLpNorm h 2 μ).toReal ^ 2

The square integral of a real L² function is its squared L² norm.

theorem CKN.Leray.lerayHopfLimit_integral_component_sq_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {g : α → Foundation.Parabolic.L2Vec3} (hg : MeasureTheory.MemLp g 2 μ) (j : Fin 3) : MeasureTheory.MemLp (fun (x : α) => (g x).ofLp j) 2 μ ∧ ∫ (x : α), (g x).ofLp j ^ 2 ∂μ ≤ (MeasureTheory.eLpNorm g 2 μ).toReal ^ 2

A coordinate of a square-integrable Euclidean field has square integral at most the squared L² norm of the field.

theorem CKN.Leray.lerayHopfLimit_toLp_memLp {f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (f x)) 2 MeasureTheory.volume

The Euclidean representative of a coordinate field in L².

theorem CKN.Leray.lerayHopfLimit_mollifiedInitial_contDiff (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedInitial ρ ε hε f x i

Each coordinate of the mollified field is smooth.

theorem CKN.Leray.lerayHopfLimit_divergence_eq_zero_of_weak (F : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hF : ∀ (i : Fin 3), ContDiff ℝ 1 fun (x : Foundation.Parabolic.Vec3) => F x i) (hweak : ∀ (ψ : WeakTestFunction Set.univ), ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, F x i * ψ.partialDeriv i x = 0) (x : Foundation.Parabolic.Vec3) : ∑ i : Fin 3, (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => F y i) x) (basisVec i) = 0

A continuously differentiable field whose weak divergence vanishes against every smooth compactly supported test is pointwise divergence-free.

theorem CKN.Leray.lerayHopfLimit_mollifiedInitial_divergence_eq_zero (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hf : IsWeakDivFreeL2 f) (x : Foundation.Parabolic.Vec3) : ∑ j : Fin 3, (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => regUniformMollifiedInitial ρ ε hε f y j) x) (basisVec j) = 0

The mollification of a weakly divergence-free L² field is pointwise divergence-free.

theorem CKN.Leray.lerayHopfLimit_mollifiedInitial_component_sq_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (j : Fin 3) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedInitial ρ ε hε f x j) 2 MeasureTheory.volume ∧ ∫ (x : Foundation.Parabolic.Vec3), regUniformMollifiedInitial ρ ε hε f x j ^ 2 ≤ (MeasureTheory.eLpNorm (regUniformSpatialField f) 2 MeasureTheory.volume).toReal ^ 2

The coordinates of the mollified field are square integrable, with square integral bounded by the squared L² norm of the field.