Slice Norm Bounds

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

Slice norm bounds

This module formalizes paper equation eq:slice-norm-bounds of paper/ckn.tex. The five dimensionless scale quantities alpha, beta, gamma, delta and lambda are defined in CKN/Statements/*.lean by normalizing a nonnegative space-time integral by a power of the radius; eq:slice-norm-bounds is the inverse reading of those definitions, expressing the unnormalized slice integrals directly in terms of the scale quantities:

• the time-slice energy essential supremum of u is r * α(z,r)²,
• the Dirichlet energy ∫∫_{Q_r} |∇u|² is r * β(z,r)²,
• the pressure integral ∫∫_{Q_r} |p|^{3/2} is r² * δ(z,r)³,
• the force integral ∫∫_{Q_r} |f|^q is (r^{5/q-3} λ(z,r))^q, where σ = 3 - 5/q is the exponent of paper/ckn.tex equation eq:lambda.

The definitions pass the underlying ℝ≥0∞ integral to ℝ≥0 with ENNReal.toReal, so each identity requires the relevant integral at radius r to be finite; this is the hfin hypothesis below, discharged for suitable weak solutions by the finiteness lemmas of CKN/Setting/Finiteness.lean.

Each identity is stated twice: as an identity of ℝ≥0∞ integrals, and as an identity of Bochner set integrals for the (nonnegative) real density, using the conversion setIntegral_eq_toReal_setLIntegral_of_nonneg of CKN/Core/Caccioppoli/Conversions.lean.

Nonnegativity of the densities

The time-slice energy identity for alpha

theorem CKN.timeSliceEnergyEssSup_eq_ofReal_alpha_sq (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 < r) (hfin : (Foundation.Parabolic.Integration.timeSliceEnergyEssSup z.1 z.2 r fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w)) ≠ ⊤) : (Foundation.Parabolic.Integration.timeSliceEnergyEssSup z.1 z.2 r fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w)) = ENNReal.ofReal (r * alpha u z r ^ 2)

Paper equation eq:slice-norm-bounds, velocity line: the essential supremum of the time-slice energy of u over the cylinder is r * α(z,r)².

The Dirichlet energy identity for beta

theorem CKN.lintegral_spatialGradientSq_eq_ofReal_beta_sq (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 < r) (hfin : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal (spatialGradientSq u Du w) ≠ ⊤) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal (spatialGradientSq u Du w) = ENNReal.ofReal (r * beta u Du z r ^ 2)

Paper equation eq:slice-norm-bounds, gradient line: the Dirichlet energy of u over the cylinder is r * β(z,r)².

theorem CKN.integral_spatialGradientSq_eq_beta_sq (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 < r) (hint : MeasureTheory.IntegrableOn (fun (w : Foundation.Parabolic.ParabolicPoint) => spatialGradientSq u Du w) (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) MeasureTheory.volume) : ∫ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, spatialGradientSq u Du w = r * beta u Du z r ^ 2

The real Bochner form of the gradient line of eq:slice-norm-bounds: the Dirichlet energy of u over the cylinder is r * β(z,r)².

The pressure integral identity for delta

theorem CKN.lintegral_abs_pow_eq_ofReal_delta_cube (p : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 < r) (hfin : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal |p w| ^ (3 / 2) ≠ ⊤) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal |p w| ^ (3 / 2) = ENNReal.ofReal (r ^ 2 * delta p z r ^ 3)

Paper equation eq:slice-norm-bounds, pressure line: the pressure integral ∫∫_{Q_r} |p|^{3/2} is r² * δ(z,r)³.

theorem CKN.integral_abs_pow_eq_delta_cube (p : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 < r) (hint : MeasureTheory.IntegrableOn (fun (w : Foundation.Parabolic.ParabolicPoint) => |p w| ^ (3 / 2)) (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) MeasureTheory.volume) : ∫ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, |p w| ^ (3 / 2) = r ^ 2 * delta p z r ^ 3

The real Bochner form of the pressure line of eq:slice-norm-bounds: the pressure integral ∫∫_{Q_r} |p|^{3/2} is r² * δ(z,r)³.

The force integral identity for lambda

theorem CKN.lintegral_vec3EuclideanNorm_pow_eq_ofReal_lambda_pow (q : ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 < r) (hq : 0 < q) (hfin : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q ≠ ⊤) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q = ENNReal.ofReal ((r ^ (5 / q - 3) * lambda q f z r) ^ q)

Paper equation eq:slice-norm-bounds, force line: with σ = 3 - 5/q, the force integral ∫∫_{Q_r} |f|^q is (r^{-σ} λ(z,r))^q.

The identities for suitable weak solutions

theorem CKN.sws_timeSliceEnergyEssSup_eq_ofReal_alpha_sq {Ω : 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)) = ENNReal.ofReal (r * alpha u z r ^ 2)

Paper equation eq:slice-norm-bounds, velocity line, for a suitable weak solution whose cylinder has closure in the carrier: the essential supremum of the time-slice energy of u is r * α(z,r)².

theorem CKN.sws_lintegral_spatialGradientSq_eq_ofReal_beta_sq {Ω : 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) = ENNReal.ofReal (r * beta u Du z r ^ 2)

Paper equation eq:slice-norm-bounds, gradient line, for a suitable weak solution whose cylinder has closure in the carrier: the Dirichlet energy of u is r * β(z,r)².

theorem CKN.sws_lintegral_abs_pow_eq_ofReal_delta_cube {Ω : 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) = ENNReal.ofReal (r ^ 2 * delta p z r ^ 3)

Paper equation eq:slice-norm-bounds, pressure line, for a suitable weak solution whose cylinder has closure in the carrier: the pressure integral ∫∫_{Q_r} |p|^{3/2} is r² * δ(z,r)³.

theorem CKN.sws_lintegral_vec3EuclideanNorm_pow_eq_ofReal_lambda_pow {Ω : 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 = ENNReal.ofReal ((r ^ (5 / q - 3) * lambda q f z r) ^ q)

Paper equation eq:slice-norm-bounds, force line, for a suitable weak solution whose cylinder has closure in the carrier: with σ = 3 - 5/q, the force integral ∫∫_{Q_r} |f|^q is (r^{-σ} λ(z,r))^q.

The real Bochner identities for suitable weak solutions

theorem CKN.sws_integral_abs_pow_eq_delta_cube {Ω : 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, |p w| ^ (3 / 2) = r ^ 2 * delta p z r ^ 3

Paper equation eq:slice-norm-bounds, pressure line, in real Bochner form for a suitable weak solution: the pressure integral ∫∫_{Q_r} |p|^{3/2} is r² * δ(z,r)³.