Theta Decay

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

The source-scale assembly below is the interface between the analytic estimates and the elementary combination theorem. The pressure estimate is kept as a display-shaped input until the pressure decomposition estimates are available at solution level.

theorem CKN.Core.Step3.thetaDecay_of_pressure_and_caccioppoli {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {ρ r C₁₄ C₁₅ C₂₅ C₂₆ : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hrr : r ≤ ρ / 2) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) : 0 ≤ C₁₄ → 0 ≤ C₁₅ → ∀ (hC₂₅ : 0 ≤ C₂₅) (hC₂₆ : 0 ≤ C₂₆) (hpressure : delta p z r ≤ C₁₄ * (r / ρ) ^ (-1 / 2) * √(alpha u z ρ) * √(beta u Du z ρ) + C₁₄ * (r / ρ) ^ (1 / 3) * delta p z ρ + C₁₅ * (r / ρ) ^ (1 / 2) * √(lambda q f z ρ)) (hcacc : alpha u z r + beta u Du z r ≤ C₂₅ * (r / ρ) * alpha u z ρ + C₂₅ * (r / ρ)⁻¹ * √(alpha u z ρ) * √(beta u Du z ρ) * √(gamma u z ρ) + C₂₅ * (r / ρ)⁻¹ * delta p z ρ * √(gamma u z ρ) + C₂₆ * (r / ρ) ^ (-1 / 2) * √(gamma u z ρ) * √(lambda q f z ρ)), theta (r / ρ) u Du p z r ≤ thetaDecayC₂₇ gagliardoConstant C₁₄ C₂₅ * (r / ρ) ^ (2 / 3) * theta (r / ρ) u Du p z ρ + thetaDecayC₂₇ gagliardoConstant C₁₄ C₂₅ * (r / ρ) ^ (-5) * (beta u Du z ρ ^ (1 / 2) + beta u Du z ρ) * theta (r / ρ) u Du p z ρ + thetaDecayC₂₈ gagliardoConstant C₁₅ C₂₆ * (r / ρ) ^ (-1 / 2) * theta (r / ρ) u Du p z ρ ^ (1 / 2) * lambda q f z ρ ^ (1 / 2) + thetaDecayC₂₈ gagliardoConstant C₁₅ C₂₆ * (r / ρ) ^ (-3) * lambda q f z ρ

Assemble the first display of lem:theta-decay from the pressure and Caccioppoli displays, using the established Gagliardo estimate.

This is the source-input wrapper. The pressure side is kept conditional on the annular cylinder inputs until the unconditional Pk bounds land.

theorem CKN.Core.Step3.thetaDecay_small_of_pressure_and_caccioppoli {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {ρ r C₁₄ C₁₅ C₂₅ C₂₆ : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hrr : r ≤ ρ / 2) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) : 0 ≤ C₁₄ → 0 ≤ C₁₅ → ∀ (hC₂₅ : 0 ≤ C₂₅) (hC₂₆ : 0 ≤ C₂₆) (hθ : theta (r / ρ) u Du p z ρ ≤ 1) (hpressure : delta p z r ≤ C₁₄ * (r / ρ) ^ (-1 / 2) * √(alpha u z ρ) * √(beta u Du z ρ) + C₁₄ * (r / ρ) ^ (1 / 3) * delta p z ρ + C₁₅ * (r / ρ) ^ (1 / 2) * √(lambda q f z ρ)) (hcacc : alpha u z r + beta u Du z r ≤ C₂₅ * (r / ρ) * alpha u z ρ + C₂₅ * (r / ρ)⁻¹ * √(alpha u z ρ) * √(beta u Du z ρ) * √(gamma u z ρ) + C₂₅ * (r / ρ)⁻¹ * delta p z ρ * √(gamma u z ρ) + C₂₆ * (r / ρ) ^ (-1 / 2) * √(gamma u z ρ) * √(lambda q f z ρ)), theta (r / ρ) u Du p z r ≤ thetaDecayC₂₇ gagliardoConstant C₁₄ C₂₅ * (r / ρ) ^ (2 / 3) * theta (r / ρ) u Du p z ρ + 2 * thetaDecayC₂₇ gagliardoConstant C₁₄ C₂₅ * (r / ρ) ^ (-5) * theta (r / ρ) u Du p z ρ ^ (1 / 2) * theta (r / ρ) u Du p z ρ + thetaDecayC₂₈ gagliardoConstant C₁₅ C₂₆ * (r / ρ) ^ (-1 / 2) * theta (r / ρ) u Du p z ρ ^ (1 / 2) * lambda q f z ρ ^ (1 / 2) + thetaDecayC₂₈ gagliardoConstant C₁₅ C₂₆ * (r / ρ) ^ (-3) * lambda q f z ρ

The small-theta display assembled from the same three source estimates.

The fixed-ratio wrapper below is a lower-level conditional adapter. It keeps the full pressure and Caccioppoli display bundle explicit; the Step 3 producer is thetaDecay_T_of_inputs in ThetaDecayTShape.lean.

Lower-level conditional adapter: this is not the paper's Step 3 producer. The producer-facing theorem is thetaDecay_T_of_inputs, whose only named analytic input is the CZ pressure-one display.