Decomposition Identity #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.pressureP1_distributional_identity_of_cutoff
{Ω : Set Foundation.Parabolic.Vec3}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{c : ℝ → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{s : ℝ}
{η ψ : Foundation.Parabolic.Vec3 → ℝ}
(hcut :
∫ (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))
(hA :
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => η x * p (x, s) * spatialLaplacian ψ x)
MeasureTheory.volume)
(hAΩ : (tsupport fun (x : Foundation.Parabolic.Vec3) => η x * p (x, s) * spatialLaplacian ψ x) ⊆ Ω)
(hB0 :
MeasureTheory.Integrable
(fun (x : Foundation.Parabolic.Vec3) =>
∑ i : Fin 3, ∑ j : Fin 3, pressureUTensor u c (x, s) i j * (η x * mixedSecond ψ i j x))
MeasureTheory.volume)
(hB0Ω :
(tsupport fun (x : Foundation.Parabolic.Vec3) =>
∑ i : Fin 3, ∑ j : Fin 3, pressureUTensor u c (x, s) i j * (η x * mixedSecond ψ i j x)) ⊆
Ω)
(hB1 :
MeasureTheory.Integrable
(fun (x : Foundation.Parabolic.Vec3) =>
∑ i : Fin 3, ∑ j : Fin 3, pressureUTensor u c (x, s) i j * (mixedSecond η i j x * ψ x))
MeasureTheory.volume)
(hB1Ω :
(tsupport fun (x : Foundation.Parabolic.Vec3) =>
∑ i : Fin 3, ∑ j : Fin 3, pressureUTensor u c (x, s) i j * (mixedSecond η i j x * ψ x)) ⊆
Ω)
(hB2 :
MeasureTheory.Integrable
(fun (x : Foundation.Parabolic.Vec3) =>
∑ i : Fin 3, ∑ j : Fin 3, pressureUTensor u c (x, s) i j * (spatialDeriv η i x * spatialDeriv ψ j x))
MeasureTheory.volume)
(hB2Ω :
(tsupport fun (x : Foundation.Parabolic.Vec3) =>
∑ i : Fin 3, ∑ j : Fin 3, pressureUTensor u c (x, s) i j * (spatialDeriv η i x * spatialDeriv ψ j x)) ⊆
Ω)
(hB3 :
MeasureTheory.Integrable
(fun (x : Foundation.Parabolic.Vec3) =>
∑ i : Fin 3, ∑ j : Fin 3, pressureUTensor u c (x, s) i j * (spatialDeriv η j x * spatialDeriv ψ i x))
MeasureTheory.volume)
(hB3Ω :
(tsupport fun (x : Foundation.Parabolic.Vec3) =>
∑ i : Fin 3, ∑ j : Fin 3, pressureUTensor u c (x, s) i j * (spatialDeriv η j x * spatialDeriv ψ i x)) ⊆
Ω)
(hC5 :
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => p (x, s) * (ψ x * spatialLaplacian η x))
MeasureTheory.volume)
(hC5Ω : (tsupport fun (x : Foundation.Parabolic.Vec3) => p (x, s) * (ψ x * spatialLaplacian η x)) ⊆ Ω)
(hC6 :
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => spatialGradDot η ψ x * p (x, s))
MeasureTheory.volume)
(hC6Ω : (tsupport fun (x : Foundation.Parabolic.Vec3) => spatialGradDot η ψ x * p (x, s)) ⊆ Ω)
(hF7 :
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, f (x, s) i * (η x * spatialDeriv ψ i x))
MeasureTheory.volume)
(hF7Ω : (tsupport fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, f (x, s) i * (η x * spatialDeriv ψ i x)) ⊆ Ω)
(hF8 :
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, f (x, s) i * (ψ x * spatialDeriv η i x))
MeasureTheory.volume)
(hF8Ω : (tsupport fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, f (x, s) i * (ψ x * spatialDeriv η i x)) ⊆ Ω)
(hQ :
MeasureTheory.Integrable
(fun (x : Foundation.Parabolic.Vec3) =>
(pressureP2 η u c s x + pressureP3 η u c s x + pressureP4 η u c s x + pressureP5 η p s x + pressureP6 η p s x + pressureP7 η f s x + pressureP8 η f s x) * spatialLaplacian ψ x)
MeasureTheory.volume)
(hP2 :
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => pressureP2 η u c s x * spatialLaplacian ψ x)
MeasureTheory.volume)
(hP3 :
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => pressureP3 η u c s x * spatialLaplacian ψ x)
MeasureTheory.volume)
(hP4 :
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => pressureP4 η u c s x * spatialLaplacian ψ x)
MeasureTheory.volume)
(hP5 :
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => pressureP5 η p s x * spatialLaplacian ψ x)
MeasureTheory.volume)
(hP6 :
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => pressureP6 η p s x * spatialLaplacian ψ x)
MeasureTheory.volume)
(hP7 :
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => pressureP7 η f s x * spatialLaplacian ψ x)
MeasureTheory.volume)
(hP8 :
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => pressureP8 η f s x * spatialLaplacian ψ x)
MeasureTheory.volume)
(hPair2 :
∫ (x : Foundation.Parabolic.Vec3), pressureP2 η u c s x * spatialLaplacian ψ x = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, pressureUTensor u c (x, s) i j * (mixedSecond η i j x * ψ x))
(hPair3 :
∫ (x : Foundation.Parabolic.Vec3), pressureP3 η u c s x * spatialLaplacian ψ x = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, pressureUTensor u c (x, s) i j * (spatialDeriv η i x * spatialDeriv ψ j x))
(hPair4 :
∫ (x : Foundation.Parabolic.Vec3), pressureP4 η u c s x * spatialLaplacian ψ x = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, pressureUTensor u c (x, s) i j * (spatialDeriv η j x * spatialDeriv ψ i x))
(hPair5 :
∫ (x : Foundation.Parabolic.Vec3), pressureP5 η p s x * spatialLaplacian ψ x = -∫ (x : Foundation.Parabolic.Vec3), p (x, s) * (ψ x * spatialLaplacian η x))
(hPair6 :
∫ (x : Foundation.Parabolic.Vec3), pressureP6 η p s x * spatialLaplacian ψ x = -2 * ∫ (x : Foundation.Parabolic.Vec3), spatialGradDot η ψ x * p (x, s))
(hPair7 :
∫ (x : Foundation.Parabolic.Vec3), pressureP7 η f s x * spatialLaplacian ψ x = -∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, f (x, s) i * (η x * spatialDeriv ψ i x))
(hPair8 :
∫ (x : Foundation.Parabolic.Vec3), pressureP8 η f s x * spatialLaplacian ψ x = -∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, f (x, s) i * (ψ x * spatialDeriv η i x))
:
∫ (x : Foundation.Parabolic.Vec3), pressureP1 η u c p f s x * spatialLaplacian ψ x = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, η x * pressureUTensor u c (x, s) i j * mixedSecond ψ i j x