Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.Support.CarlemanCoreCalculus

First derivatives of conjugated scalar fields #

Local product and chain rules for the ordinary space-time coordinates in prop:carleman-gauss of the Escauriaza–Seregin–Šverák manuscript.

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

The product normed additive group structure required for space-time differentiation.

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

    The real product normed-space structure required for space-time differentiation.

    Equations
    Instances For
      source
      theorem CKN.spatialPartial_mul_at {a b : Foundation.Parabolic.ParabolicPoint → ℝ} {z : Foundation.Parabolic.ParabolicPoint} (ha : DifferentiableAt ℝ a z) (hb : DifferentiableAt ℝ b z) (i : Fin 3) :
      spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => a y * b y) i z = spatialPartial a i z * b z + a z * spatialPartial b i z

      Spatial product rule at a point of differentiability.

      source
      theorem CKN.timePartial_mul_at {a b : Foundation.Parabolic.ParabolicPoint → ℝ} {z : Foundation.Parabolic.ParabolicPoint} (ha : DifferentiableAt ℝ a z) (hb : DifferentiableAt ℝ b z) :
      timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => a y * b y) z = timePartial a z * b z + a z * timePartial b z

      Time product rule at a point of differentiability.

      source
      theorem CKN.spatialPartial_exp_at {φ : Foundation.Parabolic.ParabolicPoint → ℝ} {z : Foundation.Parabolic.ParabolicPoint} (hφ : DifferentiableAt ℝ φ z) (i : Fin 3) :
      spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => Real.exp (φ y)) i z = Real.exp (φ z) * spatialPartial φ i z

      Spatial derivative of the exponential of a differentiable phase.

      source
      theorem CKN.timePartial_exp_at {φ : Foundation.Parabolic.ParabolicPoint → ℝ} {z : Foundation.Parabolic.ParabolicPoint} (hφ : DifferentiableAt ℝ φ z) :
      timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => Real.exp (φ y)) z = Real.exp (φ z) * timePartial φ z

      Time derivative of the exponential of a differentiable phase.

      source
      theorem CKN.spatialPartial_exp_mul_at {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {φ w : Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) (hw : ContDiff ℝ (↑⊤) w) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) (i : Fin 3) :
      spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => Real.exp (φ y) * w y) i z = Real.exp (φ z) * (spatialPartial w i z + w z * spatialPartial φ i z)

      The first spatial derivative under exponential conjugation.

      source
      theorem CKN.timePartial_exp_mul_at {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {φ w : Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) (hw : ContDiff ℝ (↑⊤) w) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) :
      timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => Real.exp (φ y) * w y) z = Real.exp (φ z) * (timePartial w z + w z * timePartial φ z)

      The first time derivative under exponential conjugation.

      source
      theorem CKN.exp_sq_scalarGradSq_le {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {φ w : Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) (hw : ContDiff ℝ (↑⊤) w) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) :
      Real.exp (φ z) ^ 2 * scalarGradSq w z ≤ 2 * (scalarGradSq (fun (y : Foundation.Parabolic.ParabolicPoint) => Real.exp (φ y) * w y) z + (Real.exp (φ z) * w z) ^ 2 * scalarGradSq φ z)

      The spatial gradient of a field before conjugation is controlled by its conjugated gradient and the phase gradient (eq:carleman-half-gradient-estimate of the Escauriaza–Seregin–Šverák manuscript).