Blowup Pressure Assembly

Pressure bounds and convergence estimates for the rescaled sequence.

theorem ESS.blowup_pressure_split_eventually_pastBox (p p₁ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) (r : ℕ → ℝ) (hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2))) (ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) (R a : ℝ) : ∀ᶠ (k : ℕ) in Filter.atTop, ∀ z ∈ CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0, blowupPressure x₀ t₀ (r k) p z = blowupRieszPressure x₀ t₀ (r k) p₁ z + blowupPressureRemainder x₀ t₀ (r k) p p₁ z

The fixed pressure decomposition holds throughout each bounded past cylinder once that cylinder fits inside the rescaled source domain.

theorem ESS.blowup_pressure_tendsto_of_split {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (p p₁ p₂ : ℕ → α → ℝ) (q : α → ℝ) (hsplit : ∀ᶠ (k : ℕ) in Filter.atTop, p k =ᵐ[μ] fun (z : α) => p₁ k z + p₂ k z) (h₁ : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : α) => p₁ k z - q z) (3 / 2) μ) Filter.atTop (nhds 0)) (h₂ : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (p₂ k) (3 / 2) μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : α) => p k z - q z) (3 / 2) μ) Filter.atTop (nhds 0)

Convergence of the whole-space pressure and vanishing of the harmonic remainder give convergence of their sum on a fixed cylinder.

theorem ESS.blowup_pressure_eventually_bounded_of_split {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (p p₁ p₂ : ℕ → α → ℝ) (hsplit : ∀ᶠ (k : ℕ) in Filter.atTop, p k =ᵐ[μ] fun (z : α) => p₁ k z + p₂ k z) (h₁ : ∃ B < ⊤, ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.eLpNorm (p₁ k) (3 / 2) μ ≤ B) (h₂ : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (p₂ k) (3 / 2) μ) Filter.atTop (nhds 0)) : ∃ B < ⊤, ∀ᶠ (k : ℕ) in Filter.atTop, MeasureTheory.eLpNorm (p k) (3 / 2) μ ≤ B

A uniformly bounded whole-space pressure and a vanishing remainder give an eventual local bound for the full pressure.

theorem ESS.blowupPressure_tendsto_of_riesz (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))) (ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) (R a : ℝ) (hR : 0 < R) (ha : a < 0) (q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (h₁ : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => blowupRieszPressure x₀ t₀ (r k) p₁ z - q z) (3 / 2) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => blowupPressure x₀ t₀ (r k) p z - q z) (3 / 2) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0))) Filter.atTop (nhds 0)

Once the whole-space pressure converges, the original rescaled pressure has the same strong local L^(3/2) limit.