The rescaled pressure decomposition

The whole-space pressure is extended by zero only in time, while its harmonic remainder is extended by zero from the original cylinder. Their sum equals the rescaled original pressure on the rescaled source domain (lem:pressure-split).

noncomputable def ESS.blowupTimeExtendedPressure (p₁ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : CKN.Foundation.Parabolic.ParabolicPoint → ℝ

Time extension of the whole-space pressure from the source time interval.

Equations

• ESS.blowupTimeExtendedPressure p₁ z = (Set.Ioo (-1) 0).indicator (fun (t : ℝ) => p₁ (z.1, t)) z.2

noncomputable def ESS.blowupRieszPressure (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (p₁ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : CKN.Foundation.Parabolic.ParabolicPoint → ℝ

The rescaled whole-space pressure, extended by zero only in time.

Equations

• ESS.blowupRieszPressure x₀ t₀ r p₁ = ESS.parabolicRescalePressure x₀ t₀ r (ESS.blowupTimeExtendedPressure p₁)

noncomputable def ESS.blowupPressureRemainder (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (p p₁ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : CKN.Foundation.Parabolic.ParabolicPoint → ℝ

The rescaled harmonic remainder of the fixed original pressure split.

Equations

• ESS.blowupPressureRemainder x₀ t₀ r p p₁ = ESS.parabolicRescalePressure x₀ t₀ r (ESS.goodPointDomain.indicator fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => p z - p₁ z)

theorem ESS.blowupPressure_eq_riesz_add_remainder_of_mem (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (p p₁ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ blowupDomain x₀ t₀ r) : blowupPressure x₀ t₀ r p z = blowupRieszPressure x₀ t₀ r p₁ z + blowupPressureRemainder x₀ t₀ r p p₁ z

The fixed pressure split is preserved on the rescaled source cylinder.