Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.Heat.Bounds

Bounds #

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

source
theorem CKN.Foundation.Heat.abs_vec3_component_le_norm (x : Parabolic.Vec3) (i : Fin 3) :
|x i| ≤ Parabolic.vec3EuclideanNorm x
source
noncomputable def CKN.Foundation.Heat.heatKernelGradientNorm (x : Parabolic.Vec3) (t : ℝ) :
ℝ

Sum of absolute spatial derivatives of the heat kernel.

Equations
Instances For
    source
    noncomputable def CKN.Foundation.Heat.heatKernelTimeGradientDerivative (x : Parabolic.Vec3) (t : ℝ) (i : Fin 3) :
    ℝ

    Time derivative of a spatial heat-kernel derivative, extended by zero to nonpositive time.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def CKN.Foundation.Heat.heatKernelTimeGradientNorm (x : Parabolic.Vec3) (t : ℝ) :
      ℝ

      Sum of absolute time derivatives of the spatial heat-kernel gradient.

      Equations
      Instances For
        source
        theorem CKN.Foundation.Heat.heatKernel_gradient_rho_four_le {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) :
        rhoTwo x t ^ 4 * heatKernelGradientNorm x t ≤ 300000
        source
        theorem CKN.Foundation.Heat.heatKernel_time_derivative_rho_five_le {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) :
        rhoTwo x t ^ 5 * |heatKernelTimeDerivative x t| ≤ 10000000
        source
        theorem CKN.Foundation.Heat.heatKernel_time_gradient_rho_six_le {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) :
        rhoTwo x t ^ 6 * heatKernelTimeGradientNorm x t ≤ 30000000000
        source
        theorem CKN.Foundation.Heat.heatKernel_rho_cube_le {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) :
        rhoTwo x t ^ 3 * heatKernel x t ≤ 1000
        source
        theorem CKN.Foundation.Heat.heatKernel_le_rho_inv_cube {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) :
        heatKernel x t ≤ 1000 / rhoTwo x t ^ 3
        source
        theorem CKN.Foundation.Heat.heatKernelGradientNorm_le_rho_inv_four {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) :
        heatKernelGradientNorm x t ≤ 300000 / rhoTwo x t ^ 4
        source
        theorem CKN.Foundation.Heat.heatKernelTimeDerivative_le_rho_inv_five {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) :
        |heatKernelTimeDerivative x t| ≤ 10000000 / rhoTwo x t ^ 5
        source
        theorem CKN.Foundation.Heat.heatKernelTimeGradientNorm_le_rho_inv_six {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) :
        heatKernelTimeGradientNorm x t ≤ 30000000000 / rhoTwo x t ^ 6
        source
        theorem CKN.Foundation.Heat.heatKernelSpaceDerivative_abs_le_rho_inv_four {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) (i : Fin 3) :
        |heatKernelSpaceDerivative x t i| ≤ 300000 / rhoTwo x t ^ 4