Kernels Basic

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

def CKN.Foundation.Harmonic.Commutator.q (x : Vec 3) : ℝ

Squared Euclidean radius used in Newtonian derivative formulas.

Equations

• CKN.Foundation.Harmonic.Commutator.q x = CKN.vecNormSq x

noncomputable def CKN.Foundation.Harmonic.Commutator.radialInverse (x : Vec 3) : ℝ

The inverse Euclidean radius, extended by zero at the origin.

Equations

• CKN.Foundation.Harmonic.Commutator.radialInverse x = if x = 0 then 0 else CKN.Foundation.Harmonic.Commutator.q x ^ (-1 / 2)

theorem CKN.Foundation.Harmonic.Commutator.hasFDerivAt_radialInverse {x : Vec 3} (hx : x ≠ 0) : HasFDerivAt radialInverse ((-1 / 2 * q x ^ (-1 / 2 - 1)) • ∑ i : Fin 3, (2 * x i) • ContinuousLinearMap.proj i) x

theorem CKN.Foundation.Harmonic.Commutator.spatialDeriv_radialInverse {x : Vec 3} (hx : x ≠ 0) (i : Fin 3) : spatialDeriv radialInverse i x = -x i * q x ^ (-3 / 2)

noncomputable def CKN.Foundation.Harmonic.Commutator.firstFormula (i : Fin 3) (x : Vec 3) : ℝ

First derivative formula for the inverse Euclidean radius.

Equations

• CKN.Foundation.Harmonic.Commutator.firstFormula i x = -x i * CKN.Foundation.Harmonic.Commutator.q x ^ (-3 / 2)

theorem CKN.Foundation.Harmonic.Commutator.hasFDerivAt_firstFormula {x : Vec 3} (hx : x ≠ 0) (i : Fin 3) : HasFDerivAt (firstFormula i) (-q x ^ (-3 / 2) • ContinuousLinearMap.proj i + -x i • (-3 / 2 * q x ^ (-3 / 2 - 1)) • ∑ k : Fin 3, (2 * x k) • ContinuousLinearMap.proj k) x

theorem CKN.Foundation.Harmonic.Commutator.spatialDeriv_firstFormula {x : Vec 3} (hx : x ≠ 0) (i j : Fin 3) : spatialDeriv (firstFormula i) j x = 3 * x i * x j * q x ^ (-5 / 2) - (if i = j then 1 else 0) * q x ^ (-3 / 2)

noncomputable def CKN.Foundation.Harmonic.Commutator.secondFormula (i j : Fin 3) (x : Vec 3) : ℝ

Second derivative formula for the inverse Euclidean radius.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.Foundation.Harmonic.Commutator.qDerivative (p : ℝ) (x : Vec 3) : Vec 3 →L[ℝ] ℝ

Continuous linear differential of a power of the squared radius.

Equations

• CKN.Foundation.Harmonic.Commutator.qDerivative p x = (p * CKN.Foundation.Harmonic.Commutator.q x ^ (p - 1)) • ∑ k : Fin 3, (2 * x k) • ContinuousLinearMap.proj k

noncomputable def CKN.Foundation.Harmonic.Commutator.secondDerivative (i j : Fin 3) (x : Vec 3) : Vec 3 →L[ℝ] ℝ

Continuous linear differential of the second inverse-radius derivative formula.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Foundation.Harmonic.Commutator.hasFDerivAt_secondFormula {x : Vec 3} (hx : x ≠ 0) (i j : Fin 3) : HasFDerivAt (secondFormula i j) (secondDerivative i j x) x

theorem CKN.Foundation.Harmonic.Commutator.spatialDeriv_secondFormula {x : Vec 3} (hx : x ≠ 0) (i j m : Fin 3) : spatialDeriv (secondFormula i j) m x = (3 * if m = i then 1 else 0) * x j * q x ^ (-5 / 2) + (3 * x i * if m = j then 1 else 0) * q x ^ (-5 / 2) - 15 * x i * x j * x m * q x ^ (-7 / 2) + (3 * if i = j then 1 else 0) * x m * q x ^ (-5 / 2)

theorem CKN.Foundation.Harmonic.Commutator.spatialDeriv_third_radialInverse {x : Vec 3} (hx : x ≠ 0) (i j m : Fin 3) : spatialDeriv (spatialDeriv (spatialDeriv radialInverse i) j) m x = (3 * if m = i then 1 else 0) * x j * q x ^ (-5 / 2) + (3 * x i * if m = j then 1 else 0) * q x ^ (-5 / 2) - 15 * x i * x j * x m * q x ^ (-7 / 2) + (3 * if i = j then 1 else 0) * x m * q x ^ (-5 / 2)

noncomputable def CKN.Foundation.Harmonic.Commutator.inverseThirdFormula (m j l : Fin 3) (x : Vec 3) : ℝ

The third derivative of the inverse Euclidean radius, in the convention used by the Newtonian kernel.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Foundation.Harmonic.Commutator.third_derivative_inverse_norm {x : Vec 3} (hx : x ≠ 0) (m j l : Fin 3) : spatialDeriv (spatialDeriv (spatialDeriv radialInverse l) j) m x = inverseThirdFormula m j l x

noncomputable def CKN.Foundation.Harmonic.Commutator.inverseThirdFormulaQ (m j l : Fin 3) (x : Vec 3) : ℝ

Third inverse-radius derivative expressed using powers of the squared radius.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.Foundation.Harmonic.Commutator.inverseThirdFormulaQDerivative (m j l : Fin 3) (x : Vec 3) : Vec 3 →L[ℝ] ℝ

Continuous linear differential of the third inverse-radius derivative formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.Foundation.Harmonic.Commutator.newtonianPotential (x : Vec 3) : ℝ

The Newtonian potential and its third-derivative kernel.

Equations

• CKN.Foundation.Harmonic.Commutator.newtonianPotential x = -(4 * Real.pi)⁻¹ * CKN.Foundation.Harmonic.Commutator.radialInverse x

noncomputable def CKN.Foundation.Harmonic.Commutator.newtonianKernel (m j l : Fin 3) (x : Vec 3) : ℝ

Normalized third Newtonian derivative kernel used in the commutator estimates.

Equations

• CKN.Foundation.Harmonic.Commutator.newtonianKernel m j l x = -(4 * Real.pi)⁻¹ * CKN.Foundation.Harmonic.Commutator.inverseThirdFormula m j l x

theorem CKN.Foundation.Harmonic.Commutator.newtonianKernel_spatialDeriv_size_bound {x : Vec 3} (hx : x ≠ 0) (m j l n : Fin 3) : |spatialDeriv (newtonianKernel m j l) n x| ≤ 204 / (4 * Real.pi) * vecEuclideanNorm x ^ (-5)