Route AGradient Producer Uniform Exponents

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

theorem CKN.Core.Step4.routeA_uniform_kappa_base : (1 / (25 / 3) + 8 / 25)⁻¹ = 25 / 11

The pressure-gradient Morrey exponent κ(τ) = (1/τ + 8/25)⁻¹ at the lower velocity endpoint τ = 25/3 is 25/11: the lower end of the range produced by the one-round improvement.

theorem CKN.Core.Step4.routeA_uniform_kappa_mono {τ τ' : ℝ} (hτ : 0 < τ) (hττ' : τ ≤ τ') : (1 / τ + 8 / 25)⁻¹ ≤ (1 / τ' + 8 / 25)⁻¹

The exponent κ(τ) = (1/τ + 8/25)⁻¹ is nondecreasing on the positive half-line: a larger velocity exponent τ yields a larger pressure-gradient exponent.

theorem CKN.Core.Step4.routeA_uniform_kappa_min_lower {q τ : ℝ} (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) : 6 / 5 ≤ min (1 / τ + 8 / 25)⁻¹ q

For q > 5/2 and τ ≥ 25/3 the capped pressure-gradient exponent min κ(τ) q is at least 6/5.