The C¹ Seeley extension

This file supplies the global differentiability and compact-support interface for the two-reflection extension. The derivative is glued across the unit sphere using the matching identities from Seeley.

noncomputable def CKN.seeleyC1Derivative (v : Vec 3 → ℝ) (x : Vec 3) : Vec 3 →L[ℝ] ℝ

Derivative formula for the two-reflection Seeley extension outside the unit ball.

Equations

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

theorem CKN.seeleyExtension_contDiff (v : Vec 3 → ℝ) (hv : ContDiff ℝ 1 v) : ContDiff ℝ 1 (seeleyExtension v)

theorem CKN.seeleyExtension_eq_on_closedBall {v : Vec 3 → ℝ} {x : Vec 3} (hx : x ∈ euclideanClosedBall 0 1) : seeleyExtension v x = v x

theorem CKN.seeleyExtension_fderiv_eq_of_mem_closedBall (v : Vec 3 → ℝ) (hv : ContDiff ℝ 1 v) {x : Vec 3} (hx : x ∈ euclideanClosedBall 0 1) : fderiv ℝ (seeleyExtension v) x = fderiv ℝ v x

theorem CKN.seeleyExtension_classicalGradient_eq_of_mem_closedBall (v : Vec 3 → ℝ) (hv : ContDiff ℝ 1 v) {x : Vec 3} (hx : x ∈ euclideanClosedBall 0 1) : classicalGradient (seeleyExtension v) x = classicalGradient v x

theorem CKN.seeleyExtension_fderiv_eq_reflection_combo_of_mem_annulus (v : Vec 3 → ℝ) (hv : ContDiff ℝ 1 v) {x : Vec 3} (hx : 1 < vecEuclideanNorm x ∧ vecEuclideanNorm x < 2) : fderiv ℝ (seeleyExtension v) x = 3 • fderiv ℝ (v ∘ seeleyReflectionOne) x - 2 • fderiv ℝ (v ∘ seeleyReflectionTwo) x

noncomputable def CKN.seeleyCutoffExtension (v : Vec 3 → ℝ) : Vec 3 → ℝ

Seeley extension multiplied by a compactly supported spatial cutoff.

Equations

• CKN.seeleyCutoffExtension v = CKN.canonicalBallCutoff 0 1 2 * CKN.seeleyExtension v