Finiteness

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

Finiteness of the scale quantities on suitable weak solutions

The quantities α, β, γ, δ, λ of paper/ckn.tex are real-valued, so the lemmas lem:monotonicity and lem:scaling-quantities for them carry side conditions saying that the underlying nonnegative integrals are finite (a necessary input when passing an ℝ≥0∞ integral to ℝ≥0). The class def:sws of suitable weak solutions supplies exactly these finiteness properties on every local box, and this file transfers them to the parabolic cylinders Q_r(z) of the monotonicity and scaling statements.

The main transfer fact is that a cylinder whose closure lies in the open carrier Ω × I is contained in a local box: the spatial slice is enclosed in a metric thickening of its closed ball, and the time slice in a thickening of its closed interval, both chosen small enough to stay inside Ω and I.

Elementary comparisons of the two norms on Vec3

Cylinders inside local boxes

theorem CKN.exists_localBox_of_closure_subset {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) {x : Foundation.Parabolic.Vec3} {t r : ℝ} (hr : 0 < r) (hsub : closure (Foundation.Parabolic.parabolicCylinder x t r) ⊆ spaceTimeSet Ω I) : ∃ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I Ω' J ∧ Foundation.Parabolic.parabolicCylinder x t r ⊆ spaceTimeSet Ω' J

A parabolic cylinder whose closure lies in the open carrier Ω × I is contained in a local box Ω' × J. The box is obtained by thickening the compact closed slices of the cylinder; the carrier is open, so a positive thickening radius keeps it inside.

The finiteness data on a local box

Finiteness of the time-slice energy (α)

theorem CKN.sws_timeSliceEnergyEssSup_lt_top {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (h : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ spaceTimeSet Ω I) : (Foundation.Parabolic.Integration.timeSliceEnergyEssSup z.1 z.2 r fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w)) < ⊤

On a cylinder whose closure lies in the carrier, the def:sws time-slice energy estimate bounds the essential supremum of the Euclidean time-slice energy occurring in lem:monotonicity for α.

theorem CKN.sws_timeSliceEnergyEssSup_ne_top {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (h : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ spaceTimeSet Ω I) : (Foundation.Parabolic.Integration.timeSliceEnergyEssSup z.1 z.2 r fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w)) ≠ ⊤

Restatement of sws_timeSliceEnergyEssSup_lt_top in the ≠ ⊤ form in which the hypothesis appears in lem:monotonicity.

Finiteness of the gradient, pressure and force integrals

theorem CKN.sws_gradient_integral_lt_top {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (h : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ spaceTimeSet Ω I) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal (spatialGradientSq u Du w) < ⊤

The Dirichlet-energy integral of lem:monotonicity for β is finite on a cylinder whose closure lies in the carrier.

theorem CKN.sws_pressure_integral_lt_top {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (h : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ spaceTimeSet Ω I) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal |p w| ^ (3 / 2) < ⊤

The pressure integral of lem:monotonicity for δ is finite on a cylinder whose closure lies in the carrier.

theorem CKN.sws_force_integral_lt_top {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (h : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ spaceTimeSet Ω I) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q < ⊤

The force integral of lem:monotonicity for λ is finite on a cylinder whose closure lies in the carrier, for the exponent q > 0 of def:sws.

Hypothesis-free monotonicity for suitable weak solutions

theorem CKN.alpha_mono_radius_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (h : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (z : Foundation.Parabolic.ParabolicPoint) {r₁ r₂ : ℝ} (hr₁ : 0 < r₁) (hrr : r₁ ≤ r₂) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r₂) ⊆ spaceTimeSet Ω I) : alpha u z r₁ ≤ (r₂ / r₁) ^ (1 / 2) * alpha u z r₂

lem:monotonicity for the velocity energy α, with the finiteness hypothesis supplied by def:sws.

theorem CKN.beta_mono_radius_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (h : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (z : Foundation.Parabolic.ParabolicPoint) {r₁ r₂ : ℝ} (hr₁ : 0 < r₁) (hrr : r₁ ≤ r₂) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r₂) ⊆ spaceTimeSet Ω I) : beta u Du z r₁ ≤ (r₂ / r₁) ^ (1 / 2) * beta u Du z r₂

lem:monotonicity for the gradient quantity β, with the finiteness hypothesis supplied by def:sws.

theorem CKN.delta_sq_mono_radius_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (h : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (z : Foundation.Parabolic.ParabolicPoint) {r₁ r₂ : ℝ} (hr₁ : 0 < r₁) (hrr : r₁ ≤ r₂) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r₂) ⊆ spaceTimeSet Ω I) : delta p z r₁ ^ 2 ≤ (r₂ / r₁) ^ (4 / 3) * delta p z r₂ ^ 2

lem:monotonicity for the pressure quantity δ in squared form, with the finiteness hypothesis supplied by def:sws.

theorem CKN.lambda_mono_radius_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (h : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (z : Foundation.Parabolic.ParabolicPoint) {r₁ r₂ : ℝ} (hr₁ : 0 < r₁) (hrr : r₁ ≤ r₂) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r₂) ⊆ spaceTimeSet Ω I) : lambda q f z r₁ ≤ (r₁ / r₂) ^ (3 - 5 / q) * lambda q f z r₂

lem:monotonicity for the force quantity λ, with the finiteness hypothesis supplied by def:sws.

theorem CKN.alpha_rescale_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} : IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ (μ : ℝ) (hμ : 0 < μ) (z₀ : Foundation.Parabolic.ParabolicPoint) (r : ℝ), alpha (rescaleVelocity μ z₀ u) (0, 0) r = alpha u z₀ (μ * r)

lem:scaling-quantities for the velocity energy α, with the two boundedness hypotheses supplied by def:sws (they hold for every nonnegative energy profile, so no assumption on the solution is needed).

theorem CKN.theta_rescale_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} : IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ (κ μ : ℝ) (hμ : 0 < μ) (z₀ : Foundation.Parabolic.ParabolicPoint) (r : ℝ) (hr : 0 < r), theta κ (rescaleVelocity μ z₀ u) (rescaleGradient μ z₀ Du) (rescalePressure μ z₀ p) (0, 0) r = theta κ u Du p z₀ (μ * r)

lem:scaling-quantities for the iteration quantity θ, with the two boundedness hypotheses of α supplied as in alpha_rescale_of_sws.