The parabolic seminorm of a spatial mean

A spatial mean over a fixed ball is, on any set of centres inside a slightly smaller ball, dominated by a spatial convolution of the averaged field with the indicator of one larger ball. Minkowski's inequality for the parabolic seminorm then bounds the mean's seminorm by that of the field itself, with the ratio of the two ball volumes as the only coefficient. No covering of the averaging ball by cells of the running radius is needed.

noncomputable def CKN.Core.Step4.gapMeanKernel (ρ : ℝ) : Foundation.Parabolic.Vec3 → ENNReal

The averaging kernel: the normalized indicator of the enlarged ball.

Equations

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

theorem CKN.Core.Step4.gapMeanKernel_measurable (ρ : ℝ) : Measurable (gapMeanKernel ρ)

theorem CKN.Core.Step4.gapMeanKernel_ne_top {ρ : ℝ} (hρ : 0 < ρ) (y : Foundation.Parabolic.Vec3) : gapMeanKernel ρ y ≠ ⊤

theorem CKN.Core.Step4.gapMeanKernel_lintegral {ρ : ℝ} (hρ : 0 < ρ) : ∫⁻ (y : Foundation.Parabolic.Vec3), gapMeanKernel ρ y = ENNReal.ofReal ((7 / 4) ^ 3)

The kernel has total mass the ratio of the two ball volumes.

theorem CKN.Core.Step4.gap_constant_slice_le_convolution (x₀ : Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) {g : Foundation.Parabolic.ParabolicPoint → ℝ} (hg : Measurable g) {m : ℝ → ℝ} {S : Set Foundation.Parabolic.ParabolicPoint} (hScar : ∀ w ∈ S, w.1 ∈ Foundation.Parabolic.vec3Ball x₀ (3 * ρ / 4)) (w : Foundation.Parabolic.ParabolicPoint) (hdom : w ∈ S → ENNReal.ofReal |m w.2| * MeasureTheory.volume (Foundation.Parabolic.vec3Ball 0 ρ) ≤ ∫⁻ (z : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, ENNReal.ofReal |g (z, w.2)|) : ENNReal.ofReal |S.indicator (fun (v : Foundation.Parabolic.ParabolicPoint) => m v.2) w| ≤ Foundation.Parabolic.Morrey.spatialConvolution (gapMeanKernel ρ) (fun (v : Foundation.Parabolic.ParabolicPoint) => ENNReal.ofReal |g v|) w

A slice-constant field carried by a ball of radius 3ρ/4 is dominated by the spatial convolution of the averaged field with the averaging kernel.

theorem CKN.Core.Step4.gap_morreyENorm_mono_ae {p q : ℝ} (hp : 0 ≤ p) {f g : Foundation.Parabolic.ParabolicPoint → ENNReal} (hfg : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint), f z ≤ g z) : Foundation.Parabolic.Morrey.morreyENorm p q f ≤ Foundation.Parabolic.Morrey.morreyENorm p q g

The a.e. form of the extended-valued seminorm comparison.

theorem CKN.Core.Step4.gap_ae_of_ae_time {P : Foundation.Parabolic.ParabolicPoint → Prop} (h : ∀ᵐ (s : ℝ), ∀ (x : Foundation.Parabolic.Vec3), P (x, s)) : ∀ᵐ (w : Foundation.Parabolic.ParabolicPoint), P w

A time-indexed almost-everywhere statement holds almost everywhere in space-time.

theorem CKN.Core.Step4.gap_constant_slice_morreyNorm_le_ae (x₀ : Foundation.Parabolic.Vec3) {ρ τ : ℝ} (hρ : 0 < ρ) (hτ : 3 ≤ τ) {g : Foundation.Parabolic.ParabolicPoint → ℝ} (hg : Measurable g) (hfin : Foundation.Parabolic.Morrey.morreyNorm 3 τ g ≠ ⊤) {m : ℝ → ℝ} {S : Set Foundation.Parabolic.ParabolicPoint} (hScar : ∀ w ∈ S, w.1 ∈ Foundation.Parabolic.vec3Ball x₀ (3 * ρ / 4)) (hdom : ∀ᵐ (w : Foundation.Parabolic.ParabolicPoint), w ∈ S → ENNReal.ofReal |m w.2| * MeasureTheory.volume (Foundation.Parabolic.vec3Ball 0 ρ) ≤ ∫⁻ (z : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, ENNReal.ofReal |g (z, w.2)|) : Foundation.Parabolic.Morrey.morreyNorm 3 τ (S.indicator fun (v : Foundation.Parabolic.ParabolicPoint) => m v.2) ≤ ENNReal.ofReal ((7 / 4) ^ 3) * Foundation.Parabolic.Morrey.morreyNorm 3 τ g

The a.e. form of the mean seminorm bound.

theorem CKN.Core.Step4.gap_centred_mean_mass_le (x₀ : Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (s : ℝ) (k : Fin 3) : ENNReal.ofReal |sourceSliceCentredMean x₀ ρ u s k| * MeasureTheory.volume (Foundation.Parabolic.vec3Ball 0 ρ) ≤ ∫⁻ (z : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, ENNReal.ofReal |u (z, s) k|

The spatial mean's mass on its own averaging ball.

theorem CKN.Core.Step4.gap_centred_mean_carrier_morreyNorm_le (x₀ : Foundation.Parabolic.Vec3) {ρ R₀ τ : ℝ} (hρ : 0 < ρ) (hτ : 3 ≤ τ) (hball : Foundation.Parabolic.vec3Ball x₀ ρ ⊆ Foundation.Parabolic.vec3Ball 0 R₀) {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (k : Fin 3) {KU : ENNReal} (hKU : KU ≠ ⊤) (hmeas : AEMeasurable ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => u w k) MeasureTheory.volume) (hU : Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => u w k) ≤ KU) {S : Set Foundation.Parabolic.ParabolicPoint} (hScar : ∀ w ∈ S, w.1 ∈ Foundation.Parabolic.vec3Ball x₀ (3 * ρ / 4)) (hStime : ∀ w ∈ S, w.2 ∈ Set.Ioc (-R₀ ^ 2) 0) : Foundation.Parabolic.Morrey.morreyNorm 3 τ (S.indicator fun (w : Foundation.Parabolic.ParabolicPoint) => sourceSliceCentredMean x₀ ρ u w.2 k) ≤ ENNReal.ofReal ((7 / 4) ^ 3) * KU

The parabolic seminorm of the centred spatial mean on a carrier inside the inner ball and the source time window is the velocity seminorm times (7/4)³.