Finiteness of the explicit Adams constants

The geometric series and maximal-function constants are finite under the same strict exponent conditions as the potential estimate.

theorem CKN.Core.Endgame.hedberg_near_constant_lt_top {β : ℝ} (hβ : 0 < β) : Foundation.Parabolic.Morrey.parabolicHedbergNearConstant β < ⊤

The near-field geometric constant is finite at every positive order.

theorem CKN.Core.Endgame.tail_kernel_constant_lt_top {β τ : ℝ} (hτ : 0 < τ) (hβτ : β * τ < 5) : Foundation.Parabolic.Morrey.parabolicTailKernelConstant β τ < ⊤

The far-field geometric constant is finite in the subcritical range.

theorem CKN.Core.Endgame.maximal_strong_constant_lt_top {P : ℝ} (hP : 1 < P) : Foundation.Parabolic.parabolicMaximalStrongConstant P < ⊤

The explicit maximal-function constant is finite for P > 1.

theorem CKN.Core.Endgame.adams_maximal_constant_lt_top {P τ : ℝ} (hP : 1 < P) (hPτ : P ≤ τ) : Foundation.Parabolic.Morrey.parabolicAdamsMaximalConstant P τ < ⊤

The localized maximal constant is finite throughout the Adams range.

theorem CKN.Core.Endgame.adams_potential_constant_lt_top {β P τ : ℝ} (hβ : 0 < β) (hP : 1 < P) (hPτ : P ≤ τ) (hβτ : β * τ < 5) : Foundation.Parabolic.Morrey.parabolicAdamsPotentialConstant β P τ < ⊤

No finiteness assumption on the explicit Adams coefficient is needed in the strict subcritical exponent range.