Tsai excess quantities

The four quantities in this file use genuine averages on the one-sided parabolic cylinder. The velocity norm is transported to L² before applying the convexity estimate, so it is the Euclidean norm used by the scale quantities.

noncomputable def CKN.tsaiVelocityExcess (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) : ℝ

Tsai's velocity excess C_tilde on the one-sided parabolic cylinder.

Equations

• One or more equations did not get rendered due to their size.

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

Tsai's pressure excess D_tilde on the one-sided parabolic cylinder.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.tsaiPhi (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) : ℝ

Tsai's combined excess φ.

Equations

• CKN.tsaiPhi u p z r = CKN.tsaiVelocityExcess u z r ^ (1 / 3) + CKN.tsaiPressureExcess p z r ^ (2 / 3)

noncomputable def CKN.tsaiPsi (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) : ℝ

Tsai's drift functional Ψ.

Equations

• CKN.tsaiPsi u z r = r * CKN.Foundation.Parabolic.vec3EuclideanNorm (⨍ (w : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.parabolicCylinder z.1 z.2 r, u w)

theorem CKN.tsaiVelocityExcess_le_eight_gamma_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} (hsol : 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) : tsaiVelocityExcess u z r ≤ 8 * gamma u z r ^ 3

theorem CKN.meanFreeVec_eq_sub_spatialAverage {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {x : Foundation.Parabolic.Vec3} {r s : ℝ} (hu : MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (Foundation.Parabolic.vec3Ball x r) MeasureTheory.volume) : (fun (y : Foundation.Parabolic.Vec3) => meanFreeVec u x r s y) = fun (y : Foundation.Parabolic.Vec3) => u (y, s) - ⨍ (z : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x r, u (z, s)

theorem CKN.meanFreeVec_aemeasurable {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {x : Foundation.Parabolic.Vec3} {r : ℝ} {T : Set ℝ} (hU : MeasureTheory.AEStronglyMeasurable u ((MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)).prod (MeasureTheory.volume.restrict T))) : MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.Vec3 × ℝ) => meanFreeVec u x r w.2 w.1) ((MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)).prod (MeasureTheory.volume.restrict T))

theorem CKN.pressureChat_le_eight_of_integrability {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (hu : MeasureTheory.IntegrableOn u (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) MeasureTheory.volume) (hu3 : MeasureTheory.IntegrableOn (fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w) ^ 3) (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) MeasureTheory.volume) : pressureChat u z r ≤ 8 * gamma u z r ^ 3

theorem CKN.pressureChat_le_eight_gamma_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} (hsol : 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) : pressureChat u z r ≤ 8 * gamma u z r ^ 3

theorem CKN.tsai_integrable_velocity_on_cylinder {Ω : 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 : ℝ} (hr : 0 < r) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ spaceTimeSet Ω I) : MeasureTheory.IntegrableOn u (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) MeasureTheory.volume

Integrability of the velocity on a contained parabolic cylinder.

theorem CKN.tsai_integrable_velocity_cube_on_cylinder {Ω : 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 : ℝ} (hr : 0 < r) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ spaceTimeSet Ω I) : MeasureTheory.IntegrableOn (fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w) ^ 3) (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) MeasureTheory.volume

Cubic velocity integrability on a contained parabolic cylinder.