Unconditional singly centred pressure bound for theta decay

The suitable-solution slice and residual estimates identify the selected pressure with the scalar Calderón--Zygmund extension. The component sum contributes a factor nine, retained in the slice constant. The cylinder adapter supplies the pressure input shared by the two regularity criteria. No pressure estimate or source certificate is assumed here.

noncomputable def CKN.czP1ThetaDecayConstant : ℝ

The fixed cylinder constant, including the tensor-component sum and the Sobolev slice-to-cylinder factor.

Equations

• CKN.czP1ThetaDecayConstant = 9 * max CKN.Foundation.Euclidean.czP1OperatorConstant 0 * (9 * CKN.sobolevPoincareL6Constant.toReal)

theorem CKN.czP1ThetaDecayConstant_nonneg : 0 ≤ czP1ThetaDecayConstant

The fixed pressure constant is nonnegative.

theorem CKN.pressureP1_thetaDecay_hCZ_unconditional (q : ℝ) (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) : IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ {z : Foundation.Parabolic.ParabolicPoint} {ρ r : ℝ} (hρ : 0 < ρ), 0 < r → r ≤ ρ / 2 → closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → ENNReal.ofReal (r ^ (-4 / 3)) * MeasureTheory.eLpNorm' (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureP1 (mollifiedBallCutoff z.1 hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f w.2 w.1) (3 / 2) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 r)) ≤ ENNReal.ofReal (czP1ThetaDecayConstant * (r / ρ)⁻¹ * alpha u z ρ * beta u Du z ρ)

The exact singly centred pressure input of theta decay follows from suitability alone, with a constant fixed before all solution data.