Documentation

LeanPool.EscauriazaSereginSverak.Linear.BUShortEnergyCompare

Energy comparison in the short-time cylinder #

The half-space Carleman mass and gradient terms dominate the quadratic cutoff energy needed to absorb the scaled differential inequality.

theorem ESS.bu_short_carleman_mass_gradient_lower (a s X G : ℝ) (ha : 1 ≤ a) (hs : 0 < s) (hs1 : s ≤ 1) (hG : 0 ≤ G) :
s ^ 2 * (X ^ 2 + G) ≤ s ^ 2 * (a * X ^ 2 / s ^ 2 + G / s)

At times below one, the Carleman left integrand dominates the weighted quadratic cutoff energy for parameters at least one.