Bounded-support Morrey inclusions #
This module records the change of Morrey exponent available for functions supported in one parabolic cylinder.
theorem
CKN.Foundation.Parabolic.Morrey.morreyNorm_bounded_support
{p q q' : ℝ}
(hp : 1 ≤ p)
(hpq : p ≤ q)
(hpq' : p ≤ q')
(hq'q : q' ≤ q)
{f : ParabolicPoint → ℝ}
{z₀ : ParabolicPoint}
{R : ℝ}
(hR : 0 < R)
(hsupp : ∀ w ∉ parabolicCylinder z₀.1 z₀.2 R, f w = 0)
:
A bounded-support function has the lower Morrey exponent at an explicit scale cost.