Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.Support.CarlemanCoreSupport

Support of conjugated test functions #

The exponential change of variables in prop:carleman-gauss of the Escauriaza–Seregin–Šverák manuscript preserves smooth compact support when the phase is smooth near that support.

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

The product normed additive group structure used in support arguments.

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

    The real product normed-space structure used in support arguments.

    Equations
    Instances For
      source
      theorem CKN.tsupport_exp_mul_subset (φ w : Foundation.Parabolic.ParabolicPoint → ℝ) :
      (tsupport fun (z : Foundation.Parabolic.ParabolicPoint) => Real.exp (φ z) * w z) ⊆ tsupport w

      Multiplication by a scalar exponential does not enlarge topological support.

      source
      theorem CKN.hasCompactSupport_exp_mul (φ w : Foundation.Parabolic.ParabolicPoint → ℝ) (hw : HasCompactSupport w) :
      HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => Real.exp (φ z) * w z

      Exponential conjugation preserves compact support.

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

      Exponential conjugation is globally smooth when the phase is smooth on an open neighborhood of the support; this is used by eq:carleman-commutator of the Escauriaza–Seregin–Šverák manuscript.