Parabolic Morrey cells and norms

This module records the extended-real Morrey seminorm on the backward parabolic cylinders already defined by the parabolic geometry module. The metric-ball version is kept alongside it; the two versions are compared by the inclusions between cylinders and metric balls.

@[reducible, inline]

abbrev CKN.Foundation.Parabolic.Morrey.Q : ℝ

Homogeneous dimension of three-dimensional parabolic space-time.

Equations

• CKN.Foundation.Parabolic.Morrey.Q = 5

noncomputable def CKN.Foundation.Parabolic.Morrey.cylinderPowerIntegral (p : ℝ) (f : ParabolicPoint → ℝ) (z : ParabolicPoint) (r : ℝ) : ENNReal

The integral part of a Morrey cell on a parabolic cylinder.

Equations

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

noncomputable def CKN.Foundation.Parabolic.Morrey.ballPowerIntegral (p : ℝ) (f : ParabolicPoint → ℝ) (z : ParabolicPoint) (r : ℝ) : ENNReal

The integral part of a Morrey cell on a metric ball.

Equations

• CKN.Foundation.Parabolic.Morrey.ballPowerIntegral p f z r = ∫⁻ (w : CKN.Foundation.Parabolic.ParabolicPoint) in Metric.ball z r, ENNReal.ofReal |f w| ^ p

noncomputable def CKN.Foundation.Parabolic.Morrey.morreyCell (p q : ℝ) (f : ParabolicPoint → ℝ) (z : ParabolicPoint) (r : ℝ) : ENNReal

The Morrey cell attached to a positive-radius cylinder.

Equations

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

The fixed homogeneous dimension in the cylinder normalization.

theorem CKN.Foundation.Parabolic.Morrey.morreyCell_eq (p q : ℝ) (f : ParabolicPoint → ℝ) (z : ParabolicPoint) (r : ℝ) : morreyCell p q f z r = ENNReal.ofReal r ^ (-(5 * (1 - p / q) / p)) * cylinderPowerIntegral p f z r ^ (1 / p)

noncomputable def CKN.Foundation.Parabolic.Morrey.morreyBallCell (p q : ℝ) (f : ParabolicPoint → ℝ) (z : ParabolicPoint) (r : ℝ) : ENNReal

The Morrey cell attached to a positive-radius metric ball.

Equations

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

noncomputable def CKN.Foundation.Parabolic.Morrey.morreyNorm (p q : ℝ) (f : ParabolicPoint → ℝ) : ENNReal

The parabolic Morrey seminorm, with homogeneous dimension Q = 5.

Equations

• CKN.Foundation.Parabolic.Morrey.morreyNorm p q f = ⨆ (z : CKN.Foundation.Parabolic.ParabolicPoint), ⨆ (r : { r : ℝ // 0 < r }), CKN.Foundation.Parabolic.Morrey.morreyCell p q f z ↑r

noncomputable def CKN.Foundation.Parabolic.Morrey.morreyBallNorm (p q : ℝ) (f : ParabolicPoint → ℝ) : ENNReal

The metric-ball version of the parabolic Morrey seminorm.

Equations

• CKN.Foundation.Parabolic.Morrey.morreyBallNorm p q f = ⨆ (z : CKN.Foundation.Parabolic.ParabolicPoint), ⨆ (r : { r : ℝ // 0 < r }), CKN.Foundation.Parabolic.Morrey.morreyBallCell p q f z ↑r

def CKN.Foundation.Parabolic.Morrey.truncate (A : ℝ) (f : ParabolicPoint → ℝ) : ParabolicPoint → ℝ

The pointwise truncation used in the monotonicity statements.

Equations

• CKN.Foundation.Parabolic.Morrey.truncate A f z = max (-A) (min A (f z))

theorem CKN.Foundation.Parabolic.Morrey.morreyNorm_le_eLpNorm' {p q : ℝ} (hp : 1 ≤ p) (hpq : p ≤ q) {f : ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) : morreyNorm p q f ≤ MeasureTheory.volume (parabolicCylinder 0 0 1) ^ (1 / p - 1 / q) * MeasureTheory.eLpNorm' f q MeasureTheory.volume

theorem CKN.Foundation.Parabolic.Morrey.cylinderPowerIntegral_parabolicPullback {a : ℝ} (ha : 0 < a) (x : Vec3) (t r p : ℝ) (u : ParabolicPoint → ℝ) (hp : 0 ≤ p) (hsource : MeasureTheory.IntegrableOn (fun (z : ParabolicPoint) => |u (parabolicTranslate x t (parabolicScale a z))| ^ p) (parabolicCylinder 0 0 r) MeasureTheory.volume) (htarget : MeasureTheory.IntegrableOn (fun (z : ParabolicPoint) => |u z| ^ p) (parabolicCylinder x t (a * r)) MeasureTheory.volume) : cylinderPowerIntegral p (fun (z : ParabolicPoint) => u (parabolicTranslate x t (parabolicScale a z))) (0, 0) r = ENNReal.ofReal a ^ (-5) * cylinderPowerIntegral p u (x, t) (a * r)

theorem CKN.Foundation.Parabolic.Morrey.cylinderPowerIntegral_translate {x : Vec3} {t r p : ℝ} (u : ParabolicPoint → ℝ) (hp : 0 ≤ p) (hsource : MeasureTheory.IntegrableOn (fun (z : ParabolicPoint) => |u (parabolicTranslate x t z)| ^ p) (parabolicCylinder 0 0 r) MeasureTheory.volume) (htarget : MeasureTheory.IntegrableOn (fun (z : ParabolicPoint) => |u z| ^ p) (parabolicCylinder x t r) MeasureTheory.volume) : cylinderPowerIntegral p (fun (z : ParabolicPoint) => u (parabolicTranslate x t z)) (0, 0) r = cylinderPowerIntegral p u (x, t) r

theorem CKN.Foundation.Parabolic.Morrey.morreyNorm_mul_le {p p₁ p₂ q q₁ q₂ : ℝ} (hp₁ : 1 ≤ p₁) (hp₂ : 1 ≤ p₂) (hrelp : 1 / p = 1 / p₁ + 1 / p₂) (hrelq : 1 / q = 1 / q₁ + 1 / q₂) {f g : ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) (hg : AEMeasurable g MeasureTheory.volume) : (morreyNorm p q fun (z : ParabolicPoint) => f z * g z) ≤ morreyNorm p₁ q₁ f * morreyNorm p₂ q₂ g

theorem CKN.Foundation.Parabolic.Morrey.morreyNorm_lower_p {p' p q : ℝ} (hp' : 1 ≤ p') (hpp : p' ≤ p) (hpq : p ≤ q) {f : ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) : morreyNorm p' q f ≤ MeasureTheory.volume (parabolicCylinder 0 0 1) ^ (1 / p' - 1 / p) * morreyNorm p q f

theorem CKN.Foundation.Parabolic.Morrey.cylinderPowerIntegral_mono {p : ℝ} (hp : 0 ≤ p) {f g : ParabolicPoint → ℝ} {z : ParabolicPoint} {r : ℝ} (hfg : ∀ w ∈ parabolicCylinder z.1 z.2 r, |f w| ≤ |g w|) : cylinderPowerIntegral p f z r ≤ cylinderPowerIntegral p g z r

theorem CKN.Foundation.Parabolic.Morrey.ballPowerIntegral_mono {p : ℝ} (hp : 0 ≤ p) {f g : ParabolicPoint → ℝ} {z : ParabolicPoint} {r : ℝ} (hfg : ∀ w ∈ Metric.ball z r, |f w| ≤ |g w|) : ballPowerIntegral p f z r ≤ ballPowerIntegral p g z r

theorem CKN.Foundation.Parabolic.Morrey.morreyCell_mono {p q : ℝ} (hp : 0 ≤ p) {f g : ParabolicPoint → ℝ} {z : ParabolicPoint} {r : ℝ} (hfg : ∀ w ∈ parabolicCylinder z.1 z.2 r, |f w| ≤ |g w|) : morreyCell p q f z r ≤ morreyCell p q g z r

theorem CKN.Foundation.Parabolic.Morrey.morreyBallCell_mono {p q : ℝ} (hp : 0 ≤ p) {f g : ParabolicPoint → ℝ} {z : ParabolicPoint} {r : ℝ} (hfg : ∀ w ∈ Metric.ball z r, |f w| ≤ |g w|) : morreyBallCell p q f z r ≤ morreyBallCell p q g z r

theorem CKN.Foundation.Parabolic.Morrey.morreyNorm_mono {p q : ℝ} (hp : 0 ≤ p) {f g : ParabolicPoint → ℝ} (hfg : ∀ (w : ParabolicPoint), |f w| ≤ |g w|) : morreyNorm p q f ≤ morreyNorm p q g

Pointwise domination passes to the cylinder Morrey seminorm.

theorem CKN.Foundation.Parabolic.Morrey.morreyBallNorm_mono {p q : ℝ} (hp : 0 ≤ p) {f g : ParabolicPoint → ℝ} (hfg : ∀ (w : ParabolicPoint), |f w| ≤ |g w|) : morreyBallNorm p q f ≤ morreyBallNorm p q g

Pointwise domination passes to the metric-ball Morrey seminorm.

theorem CKN.Foundation.Parabolic.Morrey.morreyNorm_indicator_le {p q : ℝ} (hp : 0 ≤ p) (s : Set ParabolicPoint) (f : ParabolicPoint → ℝ) : morreyNorm p q (s.indicator f) ≤ morreyNorm p q f

Indicator truncation cannot increase a Morrey seminorm.

theorem CKN.Foundation.Parabolic.Morrey.morreyNorm_truncate_le {p q : ℝ} (hp : 0 ≤ p) {A : ℝ} (hA : 0 ≤ A) (f : ParabolicPoint → ℝ) : morreyNorm p q (truncate A f) ≤ morreyNorm p q f

A nonnegative truncation cannot increase a Morrey seminorm.

theorem CKN.Foundation.Parabolic.Morrey.morreyNorm_le_morreyBallNorm {p q : ℝ} (hp : 0 ≤ p) : p ≤ q → ∀ (f : ParabolicPoint → ℝ), morreyNorm p q f ≤ morreyBallNorm p q f

theorem CKN.Foundation.Parabolic.Morrey.ballPowerIntegral_le_cylinderPowerIntegral {p : ℝ} : 0 ≤ p → ∀ {x : Vec3} {t R : ℝ} (hR : 0 < R) (f : ParabolicPoint → ℝ), ballPowerIntegral p f (x, t) R ≤ cylinderPowerIntegral p f (x, t + 2 * R ^ 2) (2 * R)