Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.Support.CarlemanCoreLocalDerivs

Local smoothness of space-time coordinate derivatives #

The phase in prop:carleman-halfspace of the Escauriaza–Seregin–Šverák manuscript is smooth only on its open cylinder. These facts keep its coordinate derivatives smooth on that same cylinder.

source
@[instance_reducible]
def CKN.carlemanCoreLocalDerivsNormedAddCommGroup :
NormedAddCommGroup Foundation.Parabolic.ParabolicPoint

The product normed additive group structure used for local derivative estimates.

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable def CKN.carlemanCoreLocalDerivsNormedSpace :
    NormedSpace ℝ Foundation.Parabolic.ParabolicPoint

    The real product normed-space structure used for local derivative estimates.

    Equations
    Instances For
      source
      theorem CKN.contDiffOn_spatialPartial {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {φ : Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) (i : Fin 3) :
      ContDiffOn ℝ (↑⊤) (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial φ i z) U

      Spatial differentiation preserves smoothness on an open set.

      source
      theorem CKN.contDiffOn_timePartial {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {φ : Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) :
      ContDiffOn ℝ (↑⊤) (fun (z : Foundation.Parabolic.ParabolicPoint) => timePartial φ z) U

      Time differentiation preserves smoothness on an open set.

      source
      theorem CKN.contDiff_mul_of_tsupport {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {f w : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) (hw : ContDiff ℝ (↑⊤) w) (hwU : tsupport w ⊆ U) :
      ContDiff ℝ ↑⊤ fun (z : Foundation.Parabolic.ParabolicPoint) => f z * w z

      A local smooth coefficient times a smooth field supported in its domain extends smoothly by zero to the whole ordinary space-time product.

      source
      theorem CKN.integrable_mul_of_tsupport {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {f w : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) (hw : ContDiff ℝ (↑⊤) w) (hwc : HasCompactSupport w) (hwU : tsupport w ⊆ U) :
      MeasureTheory.Integrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => f z * w z) MeasureTheory.volume

      A compactly supported product of a local smooth coefficient and a smooth field is integrable on space-time.

      source
      theorem CKN.contDiffOn_scalarGradSq {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) :
      ContDiffOn ℝ (↑⊤) (scalarGradSq f) U

      The scalar squared gradient of a smooth phase is smooth on its domain.

      source
      theorem CKN.contDiffOn_scalarLaplacian {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) :
      ContDiffOn ℝ (↑⊤) (scalarLaplacian f) U

      The scalar spatial Laplacian of a smooth phase is smooth on its domain.

      source
      theorem CKN.contDiffOn_carlemanConj {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {φ v : Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) (hv : ContDiff ℝ (↑⊤) v) :
      ContDiffOn ℝ (↑⊤) (carlemanConj φ v) U

      The expanded conjugated heat operator is smooth where the phase is smooth.