Cylinder

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

noncomputable def CKN.Foundation.Heat.backwardHeatTestGradientNorm (r : ℝ) (x : Parabolic.Vec3) (t : ℝ) : ℝ

Spatial-gradient bound for the rescaled backward heat test function.

Equations

• CKN.Foundation.Heat.backwardHeatTestGradientNorm r x t = r ^ 2 * CKN.Foundation.Heat.heatKernelGradientNorm x (r ^ 2 - t)

theorem CKN.Foundation.Heat.backwardHeatTestFunction_lower_on_cylinder {r : ℝ} (hr : 0 < r) {p : Parabolic.ParabolicPoint} (hp : p ∈ Parabolic.parabolicCylinder 0 0 r) : 1 / (2000 * r) ≤ backwardHeatTestFunction r p.1 p.2

theorem CKN.Foundation.Heat.backwardHeatTestFunction_upper_on_cylinder {r ρ : ℝ} (hr : 0 < r) : 0 < ρ → ∀ {p : Parabolic.ParabolicPoint} (hp : p ∈ Parabolic.parabolicCylinder 0 0 ρ), backwardHeatTestFunction r p.1 p.2 ≤ 1000 / r

theorem CKN.Foundation.Heat.backwardHeatTestGradient_upper_on_cylinder {r ρ : ℝ} (hr : 0 < r) : 0 < ρ → ∀ {p : Parabolic.ParabolicPoint} (hp : p ∈ Parabolic.parabolicCylinder 0 0 ρ), backwardHeatTestGradientNorm r p.1 p.2 ≤ 300000 / r ^ 2

theorem CKN.Foundation.Heat.backwardHeatTestFunction_upper_on_annulus {r ρ : ℝ} (hr : 0 < r) (hρ : 0 < ρ) : r ≤ ρ / 2 → ∀ {p : Parabolic.ParabolicPoint} (hp : p ∈ Parabolic.parabolicCylinder 0 0 ρ \ Parabolic.parabolicCylinder 0 0 (ρ / 2)), backwardHeatTestFunction r p.1 p.2 ≤ 8000000 * r ^ 2 / ρ ^ 3

theorem CKN.Foundation.Heat.backwardHeatTestGradient_upper_on_annulus {r ρ : ℝ} (hr : 0 < r) (hρ : 0 < ρ) : r ≤ ρ / 2 → ∀ {p : Parabolic.ParabolicPoint} (hp : p ∈ Parabolic.parabolicCylinder 0 0 ρ \ Parabolic.parabolicCylinder 0 0 (ρ / 2)), backwardHeatTestGradientNorm r p.1 p.2 ≤ 5000000 * r ^ 2 / ρ ^ 4