Localized Equation Tested #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.Core.Step3.localized_divergence_tested_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)
{φ : Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hφ : φ ∈ spaceTimeTestFunction Ω I)
{Ω' : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hbox : localBox Ω I Ω' J)
(hφbox : tsupport φ ⊆ Ω' ×ˢ J)
{ψ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3}
(hψ : ψ ∈ spaceTimeTestFunction Set.univ Set.univ)
:
∫ (z : Foundation.Parabolic.ParabolicPoint), ∑ i : Fin 3,
localizedVelocity
(have this := φ;
this)
u z i * (-timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => ψ w i) z - ∑ j : Fin 3, spatialSecondPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => ψ w i) j j z) = (∫ (z : Foundation.Parabolic.ParabolicPoint), ∑ i : Fin 3, localizedDivergenceG φ u Du p f z i * ψ z i) + ∑ i : Fin 3,
∑ j : Fin 3,
∫ (z : Foundation.Parabolic.ParabolicPoint), localizedDivergenceH φ u p j z i * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => ψ w i) j z