One-sided transfer of scalar Morrey estimates

This is Step 2 of the proof of thm:A, isolated as a statement about one scalar function. The manuscript's Step 2 replaces the centre shift of lem:step2-morrey-balls, which moves a centre forward in time by the square of the radius, by a truncated shift that stops at the top face t = 0; see truncatedCylinderCenter. Small cylinders are then covered by a cylinder of twice the radius about an admissible centre, and the decay hypothesis eq:thmA-morrey applies there. Large cylinders are paid for by the total integral on the fixed intermediate cylinder, which is the manuscript's unchanged large-radius case.

oneSidedMorreyBound P τ ρ₀ A B is the resulting constant. A is the small-cell growth coefficient and B the total integral; the two enter through the two regimes just described.

theorem CKN.Core.Endgame.cylinder_morrey_cell_le {P τ : ℝ} {K : ENNReal} {g : Foundation.Parabolic.ParabolicPoint → ℝ} {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hP : 0 < P) (hr : 0 < r) (hI : Foundation.Parabolic.Morrey.cylinderPowerIntegral P g z r ≤ K * ENNReal.ofReal (r ^ (5 * (1 - P / τ)))) : Foundation.Parabolic.Morrey.morreyCell P τ g z r ≤ K ^ (1 / P)

noncomputable def CKN.Core.Endgame.oneSidedMorreyBound (P τ ρ₀ : ℝ) (A B : ENNReal) : ENNReal

The explicit small-scale plus large-scale constant for the one-sided Morrey transfer.

Equations

• CKN.Core.Endgame.oneSidedMorreyBound P τ ρ₀ A B = (A * ENNReal.ofReal (2 ^ (5 * (1 - P / τ)))) ^ (1 / P) + ENNReal.ofReal ((ρ₀ / 2) ^ (-(5 * (1 - P / τ) / P))) * B ^ (1 / P)

theorem CKN.Core.Endgame.oneSidedMorreyBound_lt_top {P τ ρ₀ : ℝ} {A B : ENNReal} (hP : 0 < P) (hA : A < ⊤) (hB : B < ⊤) : oneSidedMorreyBound P τ ρ₀ A B < ⊤

Finite integral constants give a finite transfer constant.

theorem CKN.Core.Endgame.morreyNorm_one_sided_indicator_le_on_cylinder (a P τ ρ₀ : ℝ) (A B : ENNReal) (ha : 0 < a) (ha34 : a < 3 / 4) (hP : 1 ≤ P) (hPτ : P ≤ τ) (hρ₀ : 0 < ρ₀) (g : Foundation.Parabolic.ParabolicPoint → ℝ) (hsmall : ∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4), ∀ (r : ℝ), 0 < r → r ≤ ρ₀ → Foundation.Parabolic.Morrey.cylinderPowerIntegral P g z r ≤ A * ENNReal.ofReal (r ^ (5 * (1 - P / τ)))) (hglobal : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 a, ENNReal.ofReal |g w| ^ P ≤ B) : Foundation.Parabolic.Morrey.morreyNorm P τ ((Foundation.Parabolic.parabolicCylinder 0 0 a).indicator g) ≤ oneSidedMorreyBound P τ ρ₀ A B

Small-scale cylinder estimates at admissible centers and a total integral bound imply an explicit Morrey estimate on the one-sided intermediate cylinder. No measurability of the scalar function is needed for this upper-integral estimate.

theorem CKN.Core.Endgame.morreyNorm_one_sided_indicator_le (P τ ρ₀ : ℝ) (A B : ENNReal) (hP : 1 ≤ P) (hPτ : P ≤ τ) (hρ₀ : 0 < ρ₀) (g : Foundation.Parabolic.ParabolicPoint → ℝ) (hsmall : ∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4), ∀ (r : ℝ), 0 < r → r ≤ ρ₀ → Foundation.Parabolic.Morrey.cylinderPowerIntegral P g z r ≤ A * ENNReal.ofReal (r ^ (5 * (1 - P / τ)))) (hglobal : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8), ENNReal.ofReal |g w| ^ P ≤ B) : Foundation.Parabolic.Morrey.morreyNorm P τ ((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator g) ≤ oneSidedMorreyBound P τ ρ₀ A B

Specialization of the quantitative transfer to the fixed intermediate cylinder.