Localized Equation Gradient Transfers #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Localized Equation Gradient Transfer #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
A spacetime version of the slice weak-gradient integration-by-parts rule.
theorem
CKN.Core.Step3.spacetime_weak_partial_transfer
{Ω' : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
{a d : Foundation.Parabolic.ParabolicPoint → ℝ}
{b : Foundation.Parabolic.Vec3 × ℝ → ℝ}
{j : Fin 3}
(hJ : MeasurableSet J)
(hleft : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => d z * b z) MeasureTheory.volume)
(hright :
MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => a z * spatialPartial b j z)
MeasureTheory.volume)
(hzero_left : ∀ z ∉ spaceTimeSet Ω' J, d z * b z = 0)
(hzero_right : ∀ z ∉ spaceTimeSet Ω' J, a z * spatialPartial b j z = 0)
(hgrad :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, HasWeakPartialDerivOn Ω' j (fun (x : Vec 3) => a (x, t)) fun (x : Vec 3) => d (x, t))
(hb : ∀ (t : ℝ), ContDiff ℝ ↑⊤ fun (x : Foundation.Parabolic.Vec3) => b (x, t))
(hbc : ∀ (t : ℝ), HasCompactSupport fun (x : Foundation.Parabolic.Vec3) => b (x, t))
(hbΩ : ∀ (t : ℝ), (tsupport fun (x : Foundation.Parabolic.Vec3) => b (x, t)) ⊆ Ω')
:
∫ (z : Foundation.Parabolic.ParabolicPoint), d z * b z = -∫ (z : Foundation.Parabolic.ParabolicPoint), a z * spatialPartial b j z
theorem
CKN.Core.Step3.localized_convection_transfer_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)
(i j : Fin 3)
:
∫ (z : Foundation.Parabolic.ParabolicPoint), u z i * u z j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w * ψ w i) j z = -∫ (z : Foundation.Parabolic.ParabolicPoint), (Du z i j * u z j + u z i * Du z j j) * (φ z * ψ z i)
theorem
CKN.Core.Step3.localized_diffusion_transfer_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)
(i j : Fin 3)
:
(-∫ (z : Foundation.Parabolic.ParabolicPoint), Du z i j * spatialPartial φ j z * ψ z i) + ∫ (z : Foundation.Parabolic.ParabolicPoint), u z i * (spatialPartial φ j z * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => ψ w i) j z) = (∫ (z : Foundation.Parabolic.ParabolicPoint), u z i * (spatialSecondPartial
(have this := φ;
this)
j j z * ψ z i)) + 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint), u z i * (spatialPartial φ j z * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => ψ w i) j z)