Documentation

LeanPool.CaffarelliKohnNirenberg.Statements.HasSpaceTimeWeakDerivs

Has Space Time Weak Derivs #

Supporting estimates for the Navier–Stokes development.

source
def CKN.HasSpaceTimeWeakDerivs (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Dw : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (D2w : Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → Foundation.Parabolic.Vec3) (Dtw : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) :
Prop

Space-time weak derivatives on Ω × I: Dw z i j is ∂ⱼ wᵢ, D2w z i j k is ∂ₖ ∂ⱼ wᵢ, and Dtw z i is ∂ₜ wᵢ, each defined by integration by parts against smooth compactly supported scalar tests on Ω × I; all four fields are locally integrable on Ω × I (manuscript §2, space-time weak derivatives).

Equations
  • One or more equations did not get rendered due to their size.
Instances For