Kappa Cap Arithmetic

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

theorem CKN.Core.Step4.min_q_twentyFive_div_eleven {q : ℝ} (hq : 5 / 2 < q) : min q (25 / 11) = 25 / 11

For q > 5/2 the cap min q (25/11) is the base value 25/11.

theorem CKN.Core.Step4.min_twentyFive_div_eleven_q {q : ℝ} (hq : 5 / 2 < q) : min (25 / 11) q = 25 / 11

For q > 5/2 the cap min (25/11) q is the base value 25/11.

theorem CKN.Core.Step4.min_kappa_base_le {q τ : ℝ} (hτ : 25 / 3 ≤ τ) : min (25 / 11) q ≤ min (1 / τ + 8 / 25)⁻¹ q

At the base velocity τ = 25/3 the capped exponent min (25/11) q is at most min κ(τ) q for any τ ≥ 25/3.

theorem CKN.Core.Step4.min_kappa_pos {q τ : ℝ} (hτ : 0 < τ) (hq : 0 < q) : 0 < min (1 / τ + 8 / 25)⁻¹ q

The capped exponent is positive when both τ and q are positive.