Leray Limit Initial Tail

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.lerayLimit_initialEnergyTail_tendsto_zero (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | ↑n < Foundation.Parabolic.vec3EuclideanNorm x}, Foundation.Parabolic.vec3EuclideanNorm (a x) ^ 2) Filter.atTop (nhds 0)

The squared energy of an L² initial field vanishes outside expanding balls, as used in prop:leray-limit.