The combined decay inequality with an absolute leading constant

Paper label lem:theta-decay (eq:theta-decay-1 and eq:theta-decay-2): there are an absolute constant C₂₇ and a constant C₂₈ = C₂₈(q) such that the combined quantity θ = α + β + κ⁻⁴δ² decays from scale ρ to scale κρ. The order of the two constants matters downstream: κ, η and ε_* of conv:kappa are built from C₂₇ alone, so C₂₇ has to be fixed before the integrability exponent q of the force.

Stating the same two displays with q quantified first would only give ∀ q, ∃ C₂₇. The theorem below exchanges the two quantifiers: the witness, thetaDecayC₂₇ gagliardoConstant √(2 · max pressureP12Constant czP1ThetaDecayConstant) caccioppoliC₂₅, mentions no q, so it can be produced before q is introduced. The Calderón–Zygmund input of thm:pressure-decay is discharged from the solution by CKN.theoremA_hCZ_p1_of_sws.

Following conv:kappa the displays are taken at κ = iterationKappa C₂₇.

theorem CKN.thetaDecay_T_of_sws_absolute : ∃ (C₂₇ : ℝ), 0 < C₂₇ ∧ ∀ (q : ℝ), ∃ (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 ρ)

Paper label lem:theta-decay, displays eq:theta-decay-1 and eq:theta-decay-2, with the leading constant C₂₇ absolute (fixed before the force exponent q) and C₂₈ = C₂₈(q), at the scale ratio κ of conv:kappa.