Calculus

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

theorem CKN.spaceTimeTestFunction_mul_smooth {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {ψ χ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ψ ∈ spaceTimeTestFunction Ω I) (hχ : ContDiff ℝ (↑⊤) χ) : (fun (z : Foundation.Parabolic.Vec3 × ℝ) => ψ z * χ z) ∈ spaceTimeTestFunction Ω I

theorem CKN.spatialPartial_contDiff {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial ψ i z

theorem CKN.spatialPartial_mul_time {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {χ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => ψ w * χ w.2) i z = spatialPartial ψ i z * χ z.2

theorem CKN.timePartial_mul_time {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {χ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hχ : ContDiff ℝ (↑⊤) χ) (z : Foundation.Parabolic.Vec3 × ℝ) : timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => ψ w * χ w.2) z = timePartial ψ z * χ z.2 + ψ z * deriv χ z.2

theorem CKN.spatialSecondPartial_mul_time {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {χ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialSecondPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => ψ w * χ w.2) i j z = spatialSecondPartial ψ i j z * χ z.2

theorem CKN.localEnergyRhs_mul_time {u : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.Vec3 × ℝ → ℝ} {f : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} {χ : ℝ → ℝ} {z : Foundation.Parabolic.Vec3 × ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hχ : ContDiff ℝ (↑⊤) χ) : localEnergyRhs u p f (fun (w : Foundation.Parabolic.Vec3 × ℝ) => ψ w * χ w.2) z = localEnergyRhs u p f ψ z * χ z.2 + Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * ψ z * deriv χ z.2