Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.Support.CarlemanCoreProduct

Ordinary product calculus on space-time #

The Carleman calculations use the ordinary normed product structure on space-time. These explicit structures keep that choice consistent across the linear estimates.

source
@[reducible, inline]
abbrev CKN.carlemanProductNormedAddCommGroup :
NormedAddCommGroup Foundation.Parabolic.ParabolicPoint

The ordinary product normed additive group on space-time.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[instance_reducible]
    def CKN.carlemanCoreProductNormedAddCommGroup :
    NormedAddCommGroup Foundation.Parabolic.ParabolicPoint

    The product normed additive group structure on the spatial-time carrier.

    Equations
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev CKN.carlemanProductNormedSpace :
      NormedSpace ℝ Foundation.Parabolic.ParabolicPoint

      The ordinary product normed real vector space on space-time.

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