Theta Decay TShape

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

The final provider-shaped export of the one-step theta estimate. The two remaining analytic producers are kept at their solution-level, arbitrary-scale shapes; the unconditional annular estimates and Caccioppoli estimate are discharged in the body.

theorem CKN.Core.Step3.thetaDecay_T_of_inputs (q C₁₂_p1 : ℝ) (hCZ_p1 : ∀ (Ω : 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 (C₁₂_p1 * (r / ρ)⁻¹ * alpha u z ρ * beta u Du z ρ)) : ∃ (C₂₇ : ℝ) (C₂₈ : ℝ), 0 < C₂₇ ∧ 0 < C₂₈ ∧ ∀ (Ω : 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} {ρ : ℝ}, 0 < ρ → closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → theta (iterationKappa C₂₇) u Du p z (iterationKappa C₂₇ * ρ) ≤ C₂₇ * iterationKappa C₂₇ ^ (2 / 3) * theta (iterationKappa C₂₇) u Du p z ρ + C₂₇ * iterationKappa C₂₇ ^ (-5) * (beta u Du z ρ ^ (1 / 2) + beta u Du z ρ) * theta (iterationKappa C₂₇) u Du p z ρ + C₂₈ * iterationKappa C₂₇ ^ (-1 / 2) * theta (iterationKappa C₂₇) u Du p z ρ ^ (1 / 2) * lambda q f z ρ ^ (1 / 2) + C₂₈ * iterationKappa C₂₇ ^ (-3) * lambda q f z ρ ∧ (theta (iterationKappa C₂₇) u Du p z ρ ≤ 1 → theta (iterationKappa C₂₇) u Du p z (iterationKappa C₂₇ * ρ) ≤ C₂₇ * iterationKappa C₂₇ ^ (2 / 3) * theta (iterationKappa C₂₇) u Du p z ρ + 2 * C₂₇ * iterationKappa C₂₇ ^ (-5) * theta (iterationKappa C₂₇) u Du p z ρ ^ (1 / 2) * theta (iterationKappa C₂₇) u Du p z ρ + C₂₈ * iterationKappa C₂₇ ^ (-1 / 2) * theta (iterationKappa C₂₇) u Du p z ρ ^ (1 / 2) * lambda q f z ρ ^ (1 / 2) + C₂₈ * iterationKappa C₂₇ ^ (-3) * lambda q f z ρ)