Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.RegMollifierProfileStandard

A standard mollifier profile #

The regularization of thm:regularised fixes one smooth, compactly supported, radial, nonnegative kernel of unit mass supported in the unit ball (lem:reg-mollifier-bounds). This file supplies one such kernel: the normalization of x ↦ expNegInvGlue (1 - 4‖x‖²), which is smooth, radial, nonnegative and supported in the closed ball of radius 1/2.

source
noncomputable def CKN.Leray.standardRegBump (x : Foundation.Parabolic.L2Vec3) :
ℝ

The unnormalized radial bump x ↦ expNegInvGlue (1 - 4‖x‖²).

Equations
Instances For
    source
    theorem CKN.Leray.standardRegBump_contDiff :
    ContDiff ℝ (↑⊤) standardRegBump
    source
    theorem CKN.Leray.standardRegBump_tsupport_subset :
    tsupport standardRegBump ⊆ Metric.closedBall 0 (1 / 2)
    source
    theorem CKN.Leray.standardRegBump_hasCompactSupport :
    HasCompactSupport standardRegBump
    source
    theorem CKN.Leray.standardRegBump_nonneg (x : Foundation.Parabolic.L2Vec3) :
    0 ≤ standardRegBump x
    source
    theorem CKN.Leray.standardRegBump_integral_pos :
    0 < ∫ (x : Foundation.Parabolic.L2Vec3), standardRegBump x
    source
    noncomputable def CKN.Leray.standardRegMollifierProfile :
    RegMollifierProfile

    The standard mollifier profile: the unit-mass normalization of the radial bump x ↦ expNegInvGlue (1 - 4‖x‖²), supported in the closed ball of radius 1/2.

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