Leray Limit Assembly Support

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.lerayLimit_lintegral_slice_bound_of_energy (F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (A : ENNReal) (hSlice : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => F (x, t)) 2 MeasureTheory.volume) (hEnergy : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.eLpNorm (regUniformVelocitySlice F t) 2 MeasureTheory.volume ^ 2 ≤ A ^ 2) (t : ℝ) : 0 ≤ t → ∫⁻ (x : Foundation.Parabolic.Vec3), ‖WithLp.toLp 2 (F (x, t))‖ₑ ^ 2 ≤ A ^ 2

A uniform slice energy identity bounds the squared spatial integral on each nonnegative time slice.

theorem CKN.Leray.lerayLimit_lintegral_spatial_tail_of_real_bound (F : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (E : Set Foundation.Parabolic.Vec3) (b : ℝ) (hF : MeasureTheory.MemLp F 2 MeasureTheory.volume) (hbound : ∫ (x : Foundation.Parabolic.Vec3) in E, Foundation.Parabolic.vec3EuclideanNorm (F x) ^ 2 ≤ b) : ∫⁻ (x : Foundation.Parabolic.Vec3) in E, ‖WithLp.toLp 2 (F x)‖ₑ ^ 2 ≤ ENNReal.ofReal b

A real exterior energy estimate controls the corresponding squared integral of the Euclidean L² representative.