Spatial interpolation for the strong-solution estimate

The finite-exponent H¹ estimate uses interpolation between L² and the whole-space L⁶ Sobolev bound (lem:lps-H1-estimate).

theorem ESS.lps_h1_vector_interpolation {s : ℝ} (hs : 3 < s) {u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hu2 : MeasureTheory.MemLp u 2 MeasureTheory.volume) (hDu2 : MeasureTheory.MemLp Du 2 MeasureTheory.volume) (hgrad : ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => u x i) fun (x : CKN.Vec 3) => Du x i) : MeasureTheory.eLpNorm u (ENNReal.ofReal (2 * s / (s - 2))) MeasureTheory.volume ≤ 3 * CKN.gagliardoNirenbergSobolevConstant ^ (3 / s) * 2 ^ (3 / s) * MeasureTheory.eLpNorm u 2 MeasureTheory.volume ^ ((s - 3) / s) * MeasureTheory.eLpNorm Du 2 MeasureTheory.volume ^ (3 / s)

Whole-space interpolation of a vector field with componentwise H¹ data, used for the gradient in lem:lps-H1-estimate.

theorem ESS.lps_h1_gradient_interpolation {s : ℝ} (hs : 3 < s) {Du : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2u : CKN.Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hDu2 : MeasureTheory.MemLp Du 2 MeasureTheory.volume) (hD2u2 : MeasureTheory.MemLp D2u 2 MeasureTheory.volume) (hgrad : ∀ (i j : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => Du x i j) fun (x : CKN.Vec 3) => D2u x i j) : MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ‖Du x i‖) (ENNReal.ofReal (2 * s / (s - 2))) MeasureTheory.volume ≤ 9 * CKN.gagliardoNirenbergSobolevConstant ^ (3 / s) * 2 ^ (3 / s) * MeasureTheory.eLpNorm Du 2 MeasureTheory.volume ^ ((s - 3) / s) * MeasureTheory.eLpNorm D2u 2 MeasureTheory.volume ^ (3 / s)

Interpolation of the full first spatial derivative using componentwise weak second derivatives, in the finite-exponent form of lem:lps-H1-estimate.

theorem ESS.lps_h1_finite_absorption {s : ℝ} (hs : 3 < s) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {A B D : ℝ}, 0 ≤ A → 0 ≤ B → 0 ≤ D → A * B ^ (1 - 3 / s) * D ^ (1 + 3 / s) ≤ 1 / 2 * D ^ 2 + C * A ^ (2 * s / (s - 3)) * B ^ 2

The finite-exponent Young absorption used after the spatial interpolation in lem:lps-H1-estimate.

theorem ESS.lps_h1_infinite_absorption {A B D : ℝ} : A * B * D ≤ 1 / 2 * D ^ 2 + 1 / 2 * A ^ 2 * B ^ 2

The separate L^2_t L^∞_x Young absorption in lem:lps-H1-estimate.

theorem ESS.lps_h1_finite_differential_absorption {s : ℝ} (hs : 3 < s) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {dy d A B D f : ℝ}, 0 ≤ A → 0 ≤ B → 0 ≤ D → B ^ 2 = f → D ^ 2 = d → dy + 2 * d ≤ 2 * (A * B ^ (1 - 3 / s) * D ^ (1 + 3 / s)) → dy + d ≤ 2 * C * A ^ (2 * s / (s - 3)) * f

The finite Serrin absorption turns the strong-equation pairing estimate into the differential inequality used by Grönwall (lem:lps-H1-estimate).

theorem ESS.lps_h1_infinite_differential_absorption {dy d A B D f : ℝ} (hBsq : B ^ 2 = f) (hDsq : D ^ 2 = d) (hBalance : dy + 2 * d ≤ 2 * (A * B * D)) : dy + d ≤ A ^ 2 * f

The endpoint Serrin absorption turns the strong-equation pairing estimate into its separate L²_t L∞_x differential inequality (lem:lps-H1-estimate).

theorem ESS.lps_h1_function_interpolation {q : ℝ} (hq2 : 2 < q) (hq6 : q < 6) (h : CKN.H1Function Set.univ) : MeasureTheory.eLpNorm h.toFun (ENNReal.ofReal q) MeasureTheory.volume ≤ MeasureTheory.eLpNorm h.toFun 2 MeasureTheory.volume ^ (1 - 3 * (1 / 2 - 1 / q)) * (CKN.gagliardoNirenbergSobolevConstant * MeasureTheory.eLpNorm (fun (x : CKN.Vec 3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (h.grad x)) 2 MeasureTheory.volume) ^ (3 * (1 / 2 - 1 / q))

Interpolation of an H¹ function between its L² norm and the whole-space L⁶ Sobolev estimate, in the exponents used by lem:lps-H1-estimate.

theorem ESS.lps_h1_finite_time_moment_integrable {t₀ t₁ s : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁)))) (hs : 3 < s) (hmix : ∫⁻ (t : ℝ) in Set.Ioo t₀ t₁, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ s) ^ (2 * s / (s - 3) / s) < ⊤) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) (ENNReal.ofReal s) MeasureTheory.volume).toReal ^ (2 * s / (s - 3))) (Set.Ioo t₀ t₁) MeasureTheory.volume

The finite branch of the mixed Serrin integral makes its spatial norm integrable to the critical time power on any open time interval. This moment is the coefficient used in the Gronwall estimate of lem:lps-H1-estimate.

theorem ESS.lps_h1_finite_time_moment_integrable_closed {t₀ t₁ s : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁)))) (hs : 3 < s) (hmix : ∫⁻ (t : ℝ) in Set.Ioo t₀ t₁, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ s) ^ (2 * s / (s - 3) / s) < ⊤) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) (ENNReal.ofReal s) MeasureTheory.volume).toReal ^ (2 * s / (s - 3))) (Set.Icc t₀ t₁) MeasureTheory.volume

The finite Serrin coefficient is integrable on the closed interval as well, since its endpoints have measure zero (lem:lps-H1-estimate).