Blowup Pressure Remainder

Pressure bounds and convergence estimates for the rescaled sequence.

noncomputable def ESS.blowupHarmonicSupExtended (p₂ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : ℝ → ENNReal

The interior harmonic supremum extended by zero outside the source time interval.

Equations

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

theorem ESS.blowupPressureExtension_ae_sup_bound (p₂ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hp₂ : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p₂ (z.1, z.2)) (3 / 2) ((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)))) : ∀ᵐ (t : ℝ), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict (CKN.euclideanBall 0 (3 / 4)), ENNReal.ofReal |goodPointDomain.indicator p₂ (x, t)| ≤ blowupHarmonicSupExtended p₂ t

On the inner spatial ball, the zero-extended pressure is almost everywhere bounded by its harmonic slice supremum.

theorem ESS.blowupHarmonicSupExtended_integrable (p₂ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hp₂ : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p₂ (z.1, z.2)) (3 / 2) ((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)))) (hharm : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), CKN.Foundation.Heat.WeaklyHarmonicOn (CKN.euclideanBall 0 1) fun (x : CKN.Foundation.Parabolic.Vec3) => p₂ (x, t)) : ∫⁻ (t : ℝ), blowupHarmonicSupExtended p₂ t ^ (3 / 2) < ⊤

The zero-extended harmonic supremum is time integrable whenever the pressure remainder has harmonic slices and finite local L^(3/2) mass.

theorem ESS.blowupPressureExtension_aestronglyMeasurable (p₂ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hp₂ : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p₂ (z.1, z.2)) (3 / 2) ((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)))) : MeasureTheory.AEStronglyMeasurable (goodPointDomain.indicator p₂) MeasureTheory.volume

Zero extension of a local L^(3/2) pressure is strongly measurable on all of space-time.

theorem ESS.blowupHarmonicPressure_extension_mass_tendsto_zero (p₂ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hp₂ : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p₂ (z.1, z.2)) (3 / 2) ((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)))) (hharm : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), CKN.Foundation.Heat.WeaklyHarmonicOn (CKN.euclideanBall 0 1) fun (x : CKN.Foundation.Parabolic.Vec3) => p₂ (x, t)) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ S : ℝ) (hS : 0 < S) (r : ℕ → ℝ) (hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2))) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.Foundation.Parabolic.parabolicCylinder 0 0 S, ENNReal.ofReal |parabolicRescalePressure x₀ t₀ (r k) (goodPointDomain.indicator p₂) z| ^ (3 / 2)) Filter.atTop (nhds 0)

The fixed harmonic remainder vanishes under parabolic blow-up on every fixed past cylinder once its slices are harmonic and locally integrable.

theorem ESS.blowupHarmonicPressure_extension_eLpNorm_tendsto_zero (p₂ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hp₂ : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p₂ (z.1, z.2)) (3 / 2) ((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)))) (hharm : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), CKN.Foundation.Heat.WeaklyHarmonicOn (CKN.euclideanBall 0 1) fun (x : CKN.Foundation.Parabolic.Vec3) => p₂ (x, t)) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ S : ℝ) (hS : 0 < S) (r : ℕ → ℝ) (hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2))) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (parabolicRescalePressure x₀ t₀ (r k) (goodPointDomain.indicator p₂)) (3 / 2) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.parabolicCylinder 0 0 S))) Filter.atTop (nhds 0)

The fixed harmonic pressure remainder converges strongly to zero in L^(3/2) on each fixed past cylinder.

theorem ESS.blowupHarmonicPressure_extension_eLpNorm_tendsto_zero_on (p₂ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hp₂ : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p₂ (z.1, z.2)) (3 / 2) ((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)))) (hharm : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), CKN.Foundation.Heat.WeaklyHarmonicOn (CKN.euclideanBall 0 1) fun (x : CKN.Foundation.Parabolic.Vec3) => p₂ (x, t)) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ S : ℝ) (hS : 0 < S) (r : ℕ → ℝ) (hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2))) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) (C : Set CKN.Foundation.Parabolic.ParabolicPoint) (hC : C ⊆ CKN.Foundation.Parabolic.parabolicCylinder 0 0 S) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (parabolicRescalePressure x₀ t₀ (r k) (goodPointDomain.indicator p₂)) (3 / 2) (MeasureTheory.volume.restrict C)) Filter.atTop (nhds 0)

Harmonic pressure remainder convergence holds on any measurable region contained in a fixed past cylinder.

theorem ESS.blowupHarmonicPressure_eLpNorm_tendsto_zero_pastBox (p₂ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hp₂ : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p₂ (z.1, z.2)) (3 / 2) ((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)))) (hharm : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), CKN.Foundation.Heat.WeaklyHarmonicOn (CKN.euclideanBall 0 1) fun (x : CKN.Foundation.Parabolic.Vec3) => p₂ (x, t)) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) (r : ℕ → ℝ) (hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2))) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) (R a : ℝ) (hR : 0 < R) (ha : a < 0) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (parabolicRescalePressure x₀ t₀ (r k) (goodPointDomain.indicator p₂)) (3 / 2) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0))) Filter.atTop (nhds 0)

The harmonic pressure remainder converges strongly on every bounded open past cylinder.

theorem ESS.blowupPressureRemainder_eLpNorm_tendsto_zero_pastBox (p p₁ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hp₂ : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p (z.1, z.2) - p₁ (z.1, z.2)) (3 / 2) ((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)))) (hharm : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), CKN.Foundation.Heat.WeaklyHarmonicOn (CKN.euclideanBall 0 1) fun (x : CKN.Foundation.Parabolic.Vec3) => p (x, t) - p₁ (x, t)) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) (r : ℕ → ℝ) (hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2))) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) (R a : ℝ) (hR : 0 < R) (ha : a < 0) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (blowupPressureRemainder x₀ t₀ (r k) p p₁) (3 / 2) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0))) Filter.atTop (nhds 0)

The remainder of the fixed pressure split vanishes strongly on bounded past cylinders after rescaling.