Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.RegularisedDuhamelPairing

Pairings for the regularized Duhamel formula #

The real mild equation is paired against complex Fourier test fields by taking the real part after complexification.

source
noncomputable def CKN.Leray.complexifyRealSchwartz (φ : SchwartzMap Foundation.Parabolic.L2Vec3 Foundation.Parabolic.L2Vec3) :
SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3

Complexify a real-valued Schwartz vector field pointwise.

Equations
Instances For
    source
    theorem CKN.Leray.complexify_toLp_realSchwartz (φ : SchwartzMap Foundation.Parabolic.L2Vec3 Foundation.Parabolic.L2Vec3) :
    complexifyVectorL2 (φ.toLp 2 MeasureTheory.volume) = complexSchwartzToL2 (complexifyRealSchwartz φ)

    Complexification of the L² class of a real Schwartz function agrees with the L² class of its pointwise complexification.