Equation

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

noncomputable def CKN.pressureTest (ψ : Foundation.Parabolic.Vec3 → ℝ) (θ : ℝ → ℝ) : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3

Space-time vector test built from a spatial gradient and a temporal scalar test.

Equations

• CKN.pressureTest ψ θ z i = θ z.2 * CKN.spatialDeriv ψ i z.1

noncomputable def CKN.pressureTestProduct (ψ : Foundation.Parabolic.Vec3 → ℝ) (θ : ℝ → ℝ) : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3

The product test field on the ordinary product carrier.

Equations

• CKN.pressureTestProduct ψ θ = CKN.pressureTest ψ θ

noncomputable def CKN.pressureTestParabolic (ψ : Foundation.Parabolic.Vec3 → ℝ) (θ : ℝ → ℝ) : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3

The product test field viewed on the parabolic-point carrier.

Equations

• CKN.pressureTestParabolic ψ θ z = CKN.pressureTest ψ θ (z.1, z.2)

theorem CKN.pressureTest_mem_spaceTimeTestFunction {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {ψ : Foundation.Parabolic.Vec3 → ℝ} {θ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψΩ : tsupport ψ ⊆ Ω) (hθ : ContDiff ℝ (↑⊤) θ) (hθc : HasCompactSupport θ) (hθI : tsupport θ ⊆ I) : pressureTestProduct ψ θ ∈ spaceTimeTestFunction Ω I

theorem CKN.pressureTest_spatialPartial {ψ : Foundation.Parabolic.Vec3 → ℝ} {θ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i j : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) : spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureTestParabolic ψ θ w i) j z = θ z.2 * mixedSecond ψ j i z.1

theorem CKN.pressureTest_timePartial {ψ : Foundation.Parabolic.Vec3 → ℝ} {θ : ℝ → ℝ} (hθ : ContDiff ℝ (↑⊤) θ) (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) : timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureTestParabolic ψ θ w i) z = (fderiv ℝ θ z.2) 1 * spatialDeriv ψ i z.1

theorem CKN.mixedSecond_swap {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i j : Fin 3) (x : Foundation.Parabolic.Vec3) : mixedSecond ψ i j x = mixedSecond ψ j i x

theorem CKN.thirdDerivative_identity {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i j : Fin 3) (x : Foundation.Parabolic.Vec3) : spatialDeriv (mixedSecond ψ j i) j x = spatialDeriv (mixedSecond ψ j j) i x

theorem CKN.pressure_time_integral_zero {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hS2 : ∀ ψ ∈ spaceTimeTestFunction Ω I, MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, u z i * spatialPartial ψ i z) (tsupport ψ) MeasureTheory.volume ∧ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, ∑ i : Fin 3, u z i * spatialPartial ψ i z = 0) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψΩ : tsupport ψ ⊆ Ω) {θ : ℝ → ℝ} (hθ : ContDiff ℝ (↑⊤) θ) (hθc : HasCompactSupport θ) (hθI : tsupport θ ⊆ I) : MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, u z i * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureTestParabolic ψ θ w i) z) (spaceTimeSet Ω I) MeasureTheory.volume ∧ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, ∑ i : Fin 3, u z i * timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureTestParabolic ψ θ w i) z = 0

theorem CKN.pressure_test_terms_integrable {Ω : 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 ψ ⊆ Ω) {θ : ℝ → ℝ} (hθ : ContDiff ℝ (↑⊤) θ) (hθc : HasCompactSupport θ) (hθI : tsupport θ ⊆ I) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureTestParabolic ψ θ w i) j z) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureTestParabolic ψ θ w i) j z) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => p z * ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureTestParabolic ψ θ w i) i z) MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, f z i * pressureTestParabolic ψ θ z i) MeasureTheory.volume

The four spatial terms generated by a separated test field are integrable.