Oscillation Lin34 Solution #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.pressure_harmonic_potential_data_ae_of_sws_inner
{Ω : 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)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), PressureHarmonicPotentialData (euclideanBall z.1 (13 * ρ / 20)) (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p
s
theorem
CKN.pressureD_eq_time_slice_integral
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{z : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
(hint :
MeasureTheory.IntegrableOn (fun (w : Foundation.Parabolic.ParabolicPoint) => |p w| ^ (3 / 2))
(Foundation.Parabolic.parabolicCylinder z.1 z.2 r) MeasureTheory.volume)
:
theorem
CKN.pressureChat_eq_time_slice_integral
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{z : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
(hint :
MeasureTheory.IntegrableOn
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u z.1 r w.2 w.1) ^ 3)
(Foundation.Parabolic.parabolicCylinder z.1 z.2 r) MeasureTheory.volume)
:
pressureChat u z r = ∫ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2, r⁻¹ ^ 2 * ∫ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 r, Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u z.1 r s x) ^ 3