Reg Tails Time Bounds

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.regTails_time_integral_le_of_sq_integral {T E : ℝ} (hT : 0 < T) (hE : 0 ≤ E) (g : ℝ → ℝ) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ioo 0 T))) (hg0 : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), 0 ≤ g t) (henergy : ∫ (t : ℝ) in Set.Ioo 0 T, g t ^ 2 ≤ E ^ 2 / 2) : ∫ (t : ℝ) in Set.Ioo 0 T, g t ≤ E * T ^ (1 / 2)

The time integral of a nonnegative L² quantity is controlled by its space-time energy and the square root of the slab length.

theorem CKN.Leray.regTails_time_rpow_three_halves_le_of_sq_integral {T E : ℝ} (hT : 0 < T) (hE : 0 ≤ E) (g : ℝ → ℝ) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ioo 0 T))) (hg0 : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), 0 ≤ g t) (henergy : ∫ (t : ℝ) in Set.Ioo 0 T, g t ^ 2 ≤ E ^ 2 / 2) : ∫ (t : ℝ) in Set.Ioo 0 T, g t ^ (3 / 2) ≤ E ^ (3 / 2) * T ^ (1 / 4)

The 3/2 time moment is controlled by the same L² energy and the quarter power of the slab length.