The spatial tail of the mollified initial datum

eq:forced-initial-tail in lem:forced-tails: the regularizing kernel is nonnegative, has total mass one and is supported in the ball of radius ε ≤ 1, so by the Cauchy–Schwarz inequality for the kernel measure, Tonelli and translation invariance, the exterior energy of J_ε a outside the ball of radius R is at most the exterior energy of a outside the ball of radius R - 1.

theorem CKN.Leray.forcedLerayLimit_initialTail_lintegral (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (R : ℝ) : ∫⁻ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R < Foundation.Parabolic.vec3EuclideanNorm x}, ∑ i : Fin 3, ‖regUniformMollifiedInitial ρ ε hε a x i‖ₑ ^ 2 ≤ ∫⁻ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R - 1 < Foundation.Parabolic.vec3EuclideanNorm x}, ∑ i : Fin 3, ‖a x i‖ₑ ^ 2

eq:forced-initial-tail in lower-integral form: for 0 < ε ≤ 1 and every R, the exterior energy of the mollified datum J_ε a outside the ball of radius R is at most the exterior energy of a outside the ball of radius R - 1.

theorem CKN.Leray.forcedLerayLimit_initialTail (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (R : ℝ) : ∫ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R < Foundation.Parabolic.vec3EuclideanNorm x}, Foundation.Parabolic.vec3EuclideanNorm (regUniformMollifiedInitial ρ ε hε a x) ^ 2 ≤ ∫ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R - 1 < Foundation.Parabolic.vec3EuclideanNorm x}, Foundation.Parabolic.vec3EuclideanNorm (a x) ^ 2

eq:forced-initial-tail: for 0 < ε ≤ 1 and every R, ∫_{|x|>R} |J_ε a|² ≤ ∫_{|x|>R-1} |a|².