Lin34 Slice Quantities

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

The four time-slice quantities of prop:lin34

The integrated estimate eq:lin35-force of paper/ckn.tex is obtained by integrating eq:lin34-pointwise over J_ρ = (t₀ - ρ², t₀). This file names the four functions of time that appear in that integration, proves that they are integrable on J_ρ, and identifies their integrals with the cylinder quantities D(z₀, r) and D(z₀, ρ) of eq:ABCDE, and C_hat(z₀, ρ) of eq:Chat.

noncomputable def CKN.lin34VelocitySlice (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (ρ s : ℝ) : ℝ

The spatial L³ mass of the mean-free velocity on B_ρ at time s, the slice integrand of C_hat(z₀,ρ) in eq:Chat.

Equations

• CKN.lin34VelocitySlice u z ρ s = ∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball z.1 ρ, CKN.Foundation.Parabolic.vec3EuclideanNorm (CKN.meanFreeVec u z.1 ρ s y) ^ 3

noncomputable def CKN.lin34PressureSlice (p : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ρ s : ℝ) : ℝ

The spatial L^{3/2} mass of the pressure on B_ρ at time s, the slice integrand of D(z₀,ρ).

Equations

• CKN.lin34PressureSlice p z ρ s = ∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball z.1 ρ, |p (y, s)| ^ (3 / 2)

noncomputable def CKN.lin34ForceSliceIntegral (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (ρ r : ℝ) (hρ : 0 < ρ) (s : ℝ) : ℝ

The spatial L^{3/2} mass of the force group p₇ + p₈ on B_r at time s.

Equations

• CKN.lin34ForceSliceIntegral f z ρ r hρ s = ∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball z.1 r, |CKN.lin34ForcePart f z.1 ρ hρ s x| ^ (3 / 2)

noncomputable def CKN.lin34F (p : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) : ℝ → ℝ

The left-hand side of eq:lin34-pointwise, extended by zero outside J_r = (t₀ - r², t₀).

Equations

• CKN.lin34F p z r = (Set.Ioc (z.2 - r ^ 2) z.2).indicator fun (s : ℝ) => r⁻¹ ^ 2 * CKN.lin34PressureSlice p z r s

noncomputable def CKN.lin34G (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (ρ : ℝ) : ℝ → ℝ

The velocity term of eq:lin34-pointwise.

Equations

• CKN.lin34G u z ρ s = ρ⁻¹ ^ 2 * CKN.lin34VelocitySlice u z ρ s

noncomputable def CKN.lin34H (p : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ρ : ℝ) : ℝ → ℝ

The pressure term of eq:lin34-pointwise.

Equations

• CKN.lin34H p z ρ s = ρ⁻¹ ^ 2 * CKN.lin34PressureSlice p z ρ s

noncomputable def CKN.lin34J (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (ρ r : ℝ) (hρ : 0 < ρ) : ℝ → ℝ

The force term of eq:lin34-pointwise, extended by zero outside J_r.

Equations

• CKN.lin34J f z ρ r hρ = (Set.Ioc (z.2 - r ^ 2) z.2).indicator fun (s : ℝ) => r⁻¹ ^ 2 * CKN.lin34ForceSliceIntegral f z ρ r hρ s

theorem CKN.lin34_time_subset {z : Foundation.Parabolic.ParabolicPoint} {ρ r : ℝ} (hr : 0 < r) (hrρ : r ≤ ρ) : z.2 - ρ ^ 2 ≤ z.2 - r ^ 2

J_r ⊆ J_ρ at the level of the left endpoints.

theorem CKN.lin34_integral_indicator_subinterval {a b c : ℝ} (hab : a ≤ b) (g : ℝ → ℝ) : ∫ (t : ℝ) in Set.Ioc a c, (Set.Ioc b c).indicator g t = ∫ (t : ℝ) in Set.Ioc b c, g t

Integrating a function extended by zero over the larger time interval is integrating it over the smaller one.

theorem CKN.lin34G_integrable {Ω : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) : MeasureTheory.Integrable (lin34G u z ρ) (MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2))

The velocity slice quantity is integrable in time on J_ρ.

theorem CKN.lin34H_integrable {Ω : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) : MeasureTheory.Integrable (lin34H p z ρ) (MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2))

The pressure slice quantity is integrable in time on J_ρ.

theorem CKN.lin34F_integrable {Ω : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {ρ r : ℝ} : 0 < ρ → ∀ (hr : 0 < r) (hrρ : r ≤ ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I), MeasureTheory.Integrable (lin34F p z r) (MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2))

The inner pressure quantity, extended by zero, is integrable on J_ρ.

theorem CKN.lin34J_integrable {Ω : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {ρ r : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hhalf : r ≤ ρ / 2) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) : MeasureTheory.Integrable (lin34J f z ρ r hρ) (MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2))

The force quantity, extended by zero, is integrable on J_ρ.

theorem CKN.lin34_pressureChat_eq_integral {Ω : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) : pressureChat u z ρ = ∫ (t : ℝ) in Set.Ioc (z.2 - ρ ^ 2) z.2, lin34G u z ρ t

C_hat(z₀,ρ) of eq:Chat is the time integral of the velocity slice quantity.

theorem CKN.lin34_pressureD_eq_integral {Ω : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) : pressureD p z ρ = ∫ (t : ℝ) in Set.Ioc (z.2 - ρ ^ 2) z.2, lin34H p z ρ t

D(z₀,ρ) is the time integral of the pressure slice quantity.

theorem CKN.lin34_pressureD_inner_eq_integral {Ω : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {ρ r : ℝ} : 0 < ρ → ∀ (hr : 0 < r) (hrρ : r ≤ ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I), pressureD p z r = ∫ (t : ℝ) in Set.Ioc (z.2 - ρ ^ 2) z.2, lin34F p z r t

D(z₀,r) is the time integral over J_ρ of the extended inner pressure quantity.