Temporal Hölder estimates for the pressure source

The products in the slice estimate eq:pressure-gradient-morrey are integrated at exponent 6/5. Velocity cubes and gradient squares enter with powers 2/5 and 3/5; quadratic velocity and tensor-energy terms use the remaining 1/5 power of the time-window measure.

theorem CKN.Core.Step4.origin_time_velocity_gradient_product_bound {μ : MeasureTheory.Measure ℝ} {U D : ℝ → ENNReal} (hU : AEMeasurable U μ) (hD : AEMeasurable D μ) : ∫⁻ (s : ℝ), (U s * D s) ^ (6 / 5) ∂μ ≤ (∫⁻ (s : ℝ), U s ^ 3 ∂μ) ^ (2 / 5) * (∫⁻ (s : ℝ), D s ^ 2 ∂μ) ^ (3 / 5)

Temporal Hölder for the velocity-gradient product in the source.

theorem CKN.Core.Step4.origin_time_energy_four_fifths_bound {μ : MeasureTheory.Measure ℝ} {E : ℝ → ENNReal} (hE : AEMeasurable E μ) : ∫⁻ (s : ℝ), E s ^ (4 / 5) ∂μ ≤ (∫⁻ (s : ℝ), E s ∂μ) ^ (4 / 5) * μ Set.univ ^ (1 / 5)

Temporal Hölder for the four-fifths power of the tensor energy.

theorem CKN.Core.Step4.origin_time_velocity_square_bound {μ : MeasureTheory.Measure ℝ} {U : ℝ → ENNReal} (hU : AEMeasurable U μ) : ∫⁻ (s : ℝ), (U s * U s) ^ (6 / 5) ∂μ ≤ (∫⁻ (s : ℝ), U s ^ 3 ∂μ) ^ (4 / 5) * μ Set.univ ^ (1 / 5)

The cutoff's quadratic velocity term is controlled by the velocity cube integral and the one-fifth power of the time-window measure.

theorem CKN.Core.Step4.origin_time_two_product_majorant_bound {μ : MeasureTheory.Measure ℝ} {U D N : ℝ → ENNReal} (c d : ENNReal) (hU : AEMeasurable U μ) (hD : AEMeasurable D μ) (hN : ∀ᵐ (s : ℝ) ∂μ, N s ≤ c * (D s * U s + d * (U s * U s))) : ∫⁻ (s : ℝ), N s ^ (6 / 5) ∂μ ≤ c ^ (6 / 5) * 2 ^ (1 / 5) * ((∫⁻ (s : ℝ), U s ^ 3 ∂μ) ^ (2 / 5) * (∫⁻ (s : ℝ), D s ^ 2 ∂μ) ^ (3 / 5) + d ^ (6 / 5) * ((∫⁻ (s : ℝ), U s ^ 3 ∂μ) ^ (4 / 5) * μ Set.univ ^ (1 / 5)))

A two-term centered-source majorant integrates using only the velocity cube, gradient square, and the measure of the time window.