Zero

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

Parabolic Morrey quantities of the zero function

This module records the cylinder and ball power integrals, Morrey cells and Morrey seminorms of the zero function.

theorem CKN.Foundation.Parabolic.Morrey.cylinderPowerIntegral_zero {p : ℝ} (hp : 0 < p) (z : ParabolicPoint) (r : ℝ) : cylinderPowerIntegral p (fun (x : ParabolicPoint) => 0) z r = 0

The cylinder power integral of the zero function vanishes at every centre and radius.

theorem CKN.Foundation.Parabolic.Morrey.ballPowerIntegral_zero {p : ℝ} (hp : 0 < p) (z : ParabolicPoint) (r : ℝ) : ballPowerIntegral p (fun (x : ParabolicPoint) => 0) z r = 0

The ball power integral of the zero function vanishes at every centre and radius.

theorem CKN.Foundation.Parabolic.Morrey.morreyCell_zero {p q : ℝ} (hp : 0 < p) (z : ParabolicPoint) (r : ℝ) : morreyCell p q (fun (x : ParabolicPoint) => 0) z r = 0

The Morrey cell quantity of the zero function vanishes at every centre and radius.

theorem CKN.Foundation.Parabolic.Morrey.morreyBallCell_zero {p q : ℝ} (hp : 0 < p) (z : ParabolicPoint) (r : ℝ) : morreyBallCell p q (fun (x : ParabolicPoint) => 0) z r = 0

The Morrey ball cell quantity of the zero function vanishes at every centre and radius.

theorem CKN.Foundation.Parabolic.Morrey.morreyNorm_zero {p q : ℝ} (hp : 0 < p) : (morreyNorm p q fun (x : ParabolicPoint) => 0) = 0

The Morrey norm of the zero function vanishes identically.

theorem CKN.Foundation.Parabolic.Morrey.morreyBallNorm_zero {p q : ℝ} (hp : 0 < p) : (morreyBallNorm p q fun (x : ParabolicPoint) => 0) = 0

The Morrey ball norm of the zero function vanishes identically.