Theta Upper Semicontinuity #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.theta_usc_of_sws_with_alpha_bound
{Ω : 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}
{rho R : ℝ}
(hrho : 0 < rho)
(hrhoR : rho < R)
(hrect : euclideanClosedBall z₀.1 R ×ˢ Set.Icc (z₀.2 - R ^ 2) z₀.2 ⊆ spaceTimeSet Ω I)
(ht₀ : z₀.2 ∈ I)
:
Filter.limsup (fun (z : Foundation.Parabolic.ParabolicPoint) => alpha u z rho ^ 2) (nhds z₀) ≤ R / rho * alpha u z₀ R ^ 2 ∧ Filter.Tendsto (fun (z : Foundation.Parabolic.ParabolicPoint) => beta u Du z rho) (nhds z₀)
(nhds (beta u Du z₀ rho)) ∧ Filter.Tendsto (fun (z : Foundation.Parabolic.ParabolicPoint) => delta p z rho) (nhds z₀) (nhds (delta p z₀ rho)) ∧ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhds z₀) fun (z : Foundation.Parabolic.ParabolicPoint) =>
alpha u z rho ^ 2
The scale quantities have the base-point semicontinuity and continuity used in the Step 2 transfer argument.
theorem
CKN.theta_usc_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}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z₀ : Foundation.Parabolic.ParabolicPoint}
{rho R : ℝ}
(hrho : 0 < rho)
(hrhoR : rho < R)
(hrect : euclideanClosedBall z₀.1 R ×ˢ Set.Icc (z₀.2 - R ^ 2) z₀.2 ⊆ spaceTimeSet Ω I)
(ht₀ : z₀.2 ∈ I)
:
Filter.limsup (fun (z : Foundation.Parabolic.ParabolicPoint) => alpha u z rho ^ 2) (nhds z₀) ≤ R / rho * alpha u z₀ R ^ 2 ∧ Filter.Tendsto (fun (z : Foundation.Parabolic.ParabolicPoint) => beta u Du z rho) (nhds z₀)
(nhds (beta u Du z₀ rho)) ∧ Filter.Tendsto (fun (z : Foundation.Parabolic.ParabolicPoint) => delta p z rho) (nhds z₀) (nhds (delta p z₀ rho))
The paper-shaped semicontinuity and continuity statement for the scale quantities.