Decomposition #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
def
CKN.pressureUTensor
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(c : ℝ → Foundation.Parabolic.Vec3)
(z : Foundation.Parabolic.ParabolicPoint)
(i j : Fin 3)
:
Partially centered velocity tensor with the sign convention for the pressure decomposition.
Equations
- CKN.pressureUTensor u c z i j = -u z i * (u z j - c z.2 j)
Instances For
theorem
CKN.decomposition_slice_integrability
{Ω : 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)
{η ψ : Foundation.Parabolic.Vec3 → ℝ}
(hηc : HasCompactSupport η)
(hηΩ : tsupport η ⊆ Ω)
(hψc : HasCompactSupport ψ)
(hψΩ : tsupport ψ ⊆ Ω)
:
∃ (Ω' : Set Foundation.Parabolic.Vec3),
IsOpen Ω' ∧ tsupport η ⊆ Ω' ∧ tsupport ψ ⊆ Ω' ∧ IsCompact (closure Ω') ∧ closure Ω' ⊆ Ω ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, s)) 2
(MeasureTheory.volume.restrict Ω') ∧ MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => p (x, s))
(MeasureTheory.volume.restrict Ω') ∧ MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => f (x, s))
(MeasureTheory.volume.restrict Ω')
Slice integrability of a compactly supported test pair on a slightly larger set.
theorem
CKN.pressure_laplace_cutoff_identity_ae
{Ω : 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)
{η : Foundation.Parabolic.Vec3 → ℝ}
(hη : ContDiff ℝ (↑⊤) η)
(hηc : HasCompactSupport η)
(hηΩ : tsupport η ⊆ Ω)
{c : ℝ → Foundation.Parabolic.Vec3}
{ψ : Foundation.Parabolic.Vec3 → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψc : HasCompactSupport ψ)
(hψΩ : tsupport ψ ⊆ Ω)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∫ (x : Foundation.Parabolic.Vec3) in Ω, p (x, s) * (η x * spatialLaplacian ψ x) = (((((((∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, ∑ j : Fin 3, pressureUTensor u c (x, s) i j * (η x * mixedSecond ψ i j x)) + ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, ∑ j : Fin 3, pressureUTensor u c (x, s) i j * (mixedSecond η i j x * ψ x)) + ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3,
∑ j : Fin 3, pressureUTensor u c (x, s) i j * (spatialDeriv η i x * spatialDeriv ψ j x)) + ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, ∑ j : Fin 3, pressureUTensor u c (x, s) i j * (spatialDeriv η j x * spatialDeriv ψ i x)) - ∫ (x : Foundation.Parabolic.Vec3) in Ω, p (x, s) * (ψ x * spatialLaplacian η x)) - 2 * ∫ (x : Foundation.Parabolic.Vec3) in Ω, spatialGradDot η ψ x * p (x, s)) - ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, f (x, s) i * (η x * spatialDeriv ψ i x)) - ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, f (x, s) i * (ψ x * spatialDeriv η i x)