Source Exponents

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

theorem CKN.Core.Endgame.heat_source_exponent_eq {q : ℝ} (hq : 5 / 2 < q) : stepTheta₀ (stepGamma₀ q) = min q (25 / 9)

The heat-source exponent is exactly the minimum of the force exponent and the exponent obtained after the velocity improvement.

theorem CKN.Core.Endgame.derivative_source_exponent_le (q : ℝ) : stepTheta₁ (stepGamma₀ q) ≤ 25 / 3

The derivative-source exponent may be lowered from the initial velocity Morrey exponent on a bounded support.

theorem CKN.Core.Endgame.source_norm_bounds_at_holder_exponents (q R : ℝ) (KF KG : ENNReal) (hq : 5 / 2 < q) (hR : 0 < R) {z₀ : Foundation.Parabolic.ParabolicPoint} {F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {G : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hF : ∀ (i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9)) fun (z : Foundation.Parabolic.ParabolicPoint) => F z i) ≤ KF) (hG : ∀ (j i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 3) fun (z : Foundation.Parabolic.ParabolicPoint) => G j z i) ≤ KG) (hsupp : ∀ (j i : Fin 3), ∀ z ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, G j z i = 0) : (∀ (i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (stepTheta₀ (stepGamma₀ q)) fun (z : Foundation.Parabolic.ParabolicPoint) => F z i) ≤ KF) ∧ ∀ (j i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (stepTheta₁ (stepGamma₀ q)) fun (z : Foundation.Parabolic.ParabolicPoint) => G j z i) ≤ ENNReal.ofReal R ^ (5 * (1 / stepTheta₁ (stepGamma₀ q) - 3 / 25)) * KG

Bounded-support source norms at the paper's exponents supply precisely the quantitative bounds required by the heat Hölder theorem.

theorem CKN.Core.Endgame.source_norm_bounds_at_holder_exponents_on_ball (q R : ℝ) (KF KG : ENNReal) (hq : 5 / 2 < q) (hR : 0 < R) {z₀ : Foundation.Parabolic.ParabolicPoint} {F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {G : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hF : ∀ (i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9)) fun (z : Foundation.Parabolic.ParabolicPoint) => F z i) ≤ KF) (hG : ∀ (j i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 3) fun (z : Foundation.Parabolic.ParabolicPoint) => G j z i) ≤ KG) (hsupp : ∀ (j i : Fin 3), ∀ z ∉ Metric.ball z₀ R, G j z i = 0) : (∀ (i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (stepTheta₀ (stepGamma₀ q)) fun (z : Foundation.Parabolic.ParabolicPoint) => F z i) ≤ KF) ∧ ∀ (j i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (stepTheta₁ (stepGamma₀ q)) fun (z : Foundation.Parabolic.ParabolicPoint) => G j z i) ≤ ENNReal.ofReal (2 * R) ^ (5 * (1 / stepTheta₁ (stepGamma₀ q) - 3 / 25)) * KG

A symmetric ball support gives the same exponent conversion with the explicit radius factor from a containing backward cylinder.

theorem CKN.Core.Endgame.source_norm_bounds_at_holder_exponents_unit (q : ℝ) (KF KG : ENNReal) (hq : 5 / 2 < q) {F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {G : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hF : ∀ (i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9)) fun (z : Foundation.Parabolic.ParabolicPoint) => F z i) ≤ KF) (hG : ∀ (j i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 3) fun (z : Foundation.Parabolic.ParabolicPoint) => G j z i) ≤ KG) (hsupp : ∀ (j i : Fin 3), ∀ z ∉ Foundation.Parabolic.parabolicCylinder 0 0 1, G j z i = 0) : (∀ (i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (stepTheta₀ (stepGamma₀ q)) fun (z : Foundation.Parabolic.ParabolicPoint) => F z i) ≤ KF) ∧ ∀ (j i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (stepTheta₁ (stepGamma₀ q)) fun (z : Foundation.Parabolic.ParabolicPoint) => G j z i) ≤ KG

On the unit support cylinder the change of derivative-source exponent does not enlarge either numerical source bound.

theorem CKN.Core.Endgame.source_norms_at_holder_exponents {q R : ℝ} (hq : 5 / 2 < q) (hR : 0 < R) {z₀ : Foundation.Parabolic.ParabolicPoint} {F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {G : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hF : ∀ (i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9)) fun (z : Foundation.Parabolic.ParabolicPoint) => F z i) < ⊤) (hG : ∀ (j i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 3) fun (z : Foundation.Parabolic.ParabolicPoint) => G j z i) < ⊤) (hsupp : ∀ (j i : Fin 3), ∀ z ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, G j z i = 0) : (∀ (i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (stepTheta₀ (stepGamma₀ q)) fun (z : Foundation.Parabolic.ParabolicPoint) => F z i) < ⊤) ∧ ∀ (j i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (stepTheta₁ (stepGamma₀ q)) fun (z : Foundation.Parabolic.ParabolicPoint) => G j z i) < ⊤

Bounded-support source norms at the paper's exponents supply precisely the exponents required by the heat Hölder theorem.