Summation of the exterior source scales

The gap between the pressure Morrey exponent and the spatial critical exponent is uniform. It makes the exterior source scales summable after their spatial masses have been integrated in time.

theorem CKN.Core.Step4.pressure_time_finite_sum_bound {ι : Type u_1} (S : Finset ι) {μ : MeasureTheory.Measure ℝ} {M : ι → ℝ → ENNReal} (hM : ∀ n ∈ S, AEMeasurable (M n) μ) : (∫⁻ (s : ℝ), (∑ n ∈ S, M n s) ^ (6 / 5) ∂μ) ^ (5 / 6) ≤ ∑ n ∈ S, (∫⁻ (s : ℝ), M n s ^ (6 / 5) ∂μ) ^ (5 / 6)

Minkowski's inequality for a finite family of nonnegative temporal majorants at the pressure-gradient integrability exponent.

theorem CKN.Core.Step4.pressure_source_dyadic_ratio_bound {κ : ℝ} (hκ : 0 < κ) (hκhi : κ ≤ 25 / 9) : 2 ^ (5 / 3 - 5 / κ) ≤ 2 ^ (-2 / 15) ∧ 2 ^ (-2 / 15) < 1

The dyadic exterior ratio is bounded by one fixed ratio strictly below one throughout the pressure-gradient exponent range.

theorem CKN.Core.Step4.pressure_source_dyadic_sum_bound {κ : ℝ} (hκ : 0 < κ) (hκhi : κ ≤ 25 / 9) (N : ℕ) : ∑ n ∈ Finset.range N, (2 ^ (5 / 3 - 5 / κ)) ^ n ≤ (1 - 2 ^ (-2 / 15))⁻¹

Every finite sum of exterior dyadic ratios has one universal bound.

theorem CKN.Core.Step4.pressure_source_dyadic_constant_lt_top : (1 - 2 ^ (-2 / 15))⁻¹ < ⊤

The universal dyadic constant is finite.

theorem CKN.Core.Step4.pressure_source_spatial_mass_aemeasurable {F : Foundation.Parabolic.ParabolicPoint → ℝ} (hF : AEMeasurable F MeasureTheory.volume) (x : Foundation.Parabolic.Vec3) (ρ : ℝ) : AEMeasurable (fun (s : ℝ) => ∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x ρ, ‖F (y, s)‖ₑ) MeasureTheory.volume

The spatial source mass is a measurable function of time.

theorem CKN.Core.Step4.pressure_time_power_norm_const_mul {μ : MeasureTheory.Measure ℝ} {M : ℝ → ENNReal} (hM : AEMeasurable M μ) (c : ENNReal) : (∫⁻ (s : ℝ), (c * M s) ^ (6 / 5) ∂μ) ^ (5 / 6) = c * (∫⁻ (s : ℝ), M s ^ (6 / 5) ∂μ) ^ (5 / 6)

Pulling a nonnegative constant out of the temporal L^{6/5} norm.

theorem CKN.Core.Step4.pressure_source_exterior_scale_sum_time_bound {κ : ℝ} (hκ : 0 < κ) (hκhi : κ ≤ 25 / 9) {F : Foundation.Parabolic.ParabolicPoint → ℝ} (hF : AEMeasurable F MeasureTheory.volume) (x : Foundation.Parabolic.Vec3) (t : ℝ) {r : ℝ} (hr : 0 < r) (N : ℕ) : (∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, (∑ n ∈ Finset.range N, ENNReal.ofReal (2 ^ n * r) ^ (-3) * ∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x (2 ^ n * r), ‖F (y, s)‖ₑ) ^ (6 / 5)) ^ (5 / 6) ≤ ENNReal.ofReal (Real.pi * 4 / 3) ^ (1 / 6) * ENNReal.ofReal r ^ (5 / 3 - 5 / κ) * Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ F * (1 - 2 ^ (-2 / 15))⁻¹

Time integration and summation of finitely many exterior scales has a constant independent of both the number of scales and the exponent.