Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.AssocPressureTestOperators

Assoc Pressure Test Operators #

Supporting estimates for the Navier–Stokes development.

source
noncomputable def CKN.Leray.associatedPressureTestPartial (f : Foundation.Parabolic.Vec3 × ℝ → ℝ) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) :
ℝ

The spatial coordinate derivative of a scalar field in product space-time coordinates.

Equations
Instances For
    source
    noncomputable def CKN.Leray.associatedPressureTestCurl (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) :
    Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3

    The three-dimensional curl of a vector test field in product space-time coordinates.

    Equations
    Instances For
      source
      @[simp]
      theorem CKN.Leray.associatedPressureTestCurl_zero (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.Vec3 × ℝ) :
      associatedPressureTestCurl φ z 0 = associatedPressureTestPartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => φ w 2) 1 z - associatedPressureTestPartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => φ w 1) 2 z
      source
      @[simp]
      theorem CKN.Leray.associatedPressureTestCurl_one (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.Vec3 × ℝ) :
      associatedPressureTestCurl φ z 1 = associatedPressureTestPartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => φ w 0) 2 z - associatedPressureTestPartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => φ w 2) 0 z
      source
      @[simp]
      theorem CKN.Leray.associatedPressureTestCurl_two (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.Vec3 × ℝ) :
      associatedPressureTestCurl φ z 2 = associatedPressureTestPartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => φ w 1) 0 z - associatedPressureTestPartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => φ w 0) 1 z
      source
      theorem CKN.Leray.associatedPressureTestPartial_eq_spatialPartial (f : Foundation.Parabolic.Vec3 × ℝ → ℝ) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) :
      associatedPressureTestPartial f i z = spatialPartial f i z
      source
      theorem CKN.Leray.associatedPressureTestCurl_mem_spaceTimeTestFunction {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Ω I) :
      associatedPressureTestCurl φ ∈ spaceTimeTestFunction Ω I

      The curl of a compact smooth vector test remains in the same compact test class.

      source
      theorem CKN.Leray.associatedPressureTestCurl_contDiff {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) :
      ContDiff ℝ (↑⊤) (associatedPressureTestCurl φ)

      The curl of a smooth vector field is smooth.

      source
      theorem CKN.Leray.associatedPressureTestPartial_spatialPartial_commute {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) :
      associatedPressureTestPartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureTestPartial f i w) j z = associatedPressureTestPartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureTestPartial f j w) i z

      Mixed spatial derivatives of a smooth scalar field commute in product space-time coordinates.

      source
      theorem CKN.Leray.associatedPressureTestPartial_sub_smooth {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) :
      associatedPressureTestPartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => f w - g w) i z = associatedPressureTestPartial f i z - associatedPressureTestPartial g i z

      Spatial differentiation distributes over subtraction of smooth scalar fields.

      source
      theorem CKN.Leray.associatedPressureTestCurl_divergence {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (z : Foundation.Parabolic.Vec3 × ℝ) :
      ∑ i : Fin 3, associatedPressureTestPartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureTestCurl φ w i) i z = 0

      The curl of a smooth test field has zero spatial divergence.

      source
      noncomputable def CKN.Leray.associatedPressureTestTimePartial (f : Foundation.Parabolic.Vec3 × ℝ → ℝ) :
      Foundation.Parabolic.Vec3 × ℝ → ℝ

      The componentwise time derivative of a scalar test in product space-time coordinates.

      Equations
      Instances For
        source
        theorem CKN.Leray.associatedPressureTestPartial_timePartial_commute {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) :
        associatedPressureTestTimePartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureTestPartial f i w) z = associatedPressureTestPartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureTestTimePartial f w) i z
        source
        theorem CKN.Leray.associatedPressureTestCurl_timePartial {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) :
        associatedPressureTestTimePartial (fun (w : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureTestCurl φ w i) z = associatedPressureTestCurl (fun (w : Foundation.Parabolic.Vec3 × ℝ) (k : Fin 3) => associatedPressureTestTimePartial (fun (y : Foundation.Parabolic.Vec3 × ℝ) => φ y k) w) z i

        Time differentiation commutes with the curl on smooth product-space tests.