The two-reflection extension on the unit ball

The radial maps in this file are the two reflections used to continue a smooth function across the unit sphere. The geometric estimates are recorded on the closed annulus and the gluing interface is kept independent of the radial maps.

def CKN.seeleyAnnulus : Set (Vec 3)

The open annulus on which both radial reflections are smooth.

Equations

• CKN.seeleyAnnulus = {x : CKN.Vec 3 | 1 / 2 < CKN.vecEuclideanNorm x ∧ CKN.vecEuclideanNorm x < 3}

def CKN.seeleyClosedAnnulus : Set (Vec 3)

The closed annulus used for the extension estimates.

Equations

• CKN.seeleyClosedAnnulus = {x : CKN.Vec 3 | 1 ≤ CKN.vecEuclideanNorm x ∧ CKN.vecEuclideanNorm x ≤ 2}

noncomputable def CKN.seeleyReflectionOne (x : Vec 3) : Vec 3

The first radial reflection, x ↦ x / |x|².

Equations

• CKN.seeleyReflectionOne x = (CKN.vecNormSq x)⁻¹ • x

noncomputable def CKN.seeleyReflectionTwo (x : Vec 3) : Vec 3

The second radial reflection, x ↦ x / ((2|x| - 1)|x|).

Equations

• CKN.seeleyReflectionTwo x = ((2 * CKN.vecEuclideanNorm x - 1) * CKN.vecEuclideanNorm x)⁻¹ • x

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

The exterior formula in the two-reflection extension.

Equations

• CKN.seeleyExterior v x = 3 * v (CKN.seeleyReflectionOne x) - 2 * v (CKN.seeleyReflectionTwo x)

theorem CKN.seeleyReflectionOne_contDiffOn : ContDiffOn ℝ (↑⊤) seeleyReflectionOne seeleyAnnulus

theorem CKN.seeleyReflectionTwo_contDiffOn : ContDiffOn ℝ (↑⊤) seeleyReflectionTwo seeleyAnnulus

theorem CKN.seeleyReflectionOne_fderiv_apply {x : Vec 3} (hx : x ∈ seeleyAnnulus) (z : Vec 3) : (fderiv ℝ seeleyReflectionOne x) z = (vecNormSq x)⁻¹ • z - ((vecNormSq x)⁻¹ ^ 2 * (2 * ∑ i : Fin 3, x i * z i)) • x

theorem CKN.seeleyReflectionOne_fderiv_sphere {x : Vec 3} (hx : vecEuclideanNorm x = 1) (z : Vec 3) : (fderiv ℝ seeleyReflectionOne x) z = z - (2 * ∑ i : Fin 3, x i * z i) • x

theorem CKN.seeleyReflectionTwo_fderiv_sphere {x : Vec 3} (hx : vecEuclideanNorm x = 1) (z : Vec 3) : (fderiv ℝ seeleyReflectionTwo x) z = z - (3 * ∑ i : Fin 3, x i * z i) • x

theorem CKN.seeleyReflectionTwo_fderiv_apply {x : Vec 3} (hx : x ∈ seeleyAnnulus) (z : Vec 3) : (fderiv ℝ seeleyReflectionTwo x) z = ((2 * vecEuclideanNorm x - 1) * vecEuclideanNorm x)⁻¹ • z - (((2 * vecEuclideanNorm x - 1) * vecEuclideanNorm x)⁻¹ ^ 2 * ((4 * vecEuclideanNorm x - 1) * ((2 * vecEuclideanNorm x)⁻¹ * (2 * ∑ i : Fin 3, x i * z i)))) • x

theorem CKN.seeleyExterior_eq_on_sphere (v : Vec 3 → ℝ) {x : Vec 3} (hx : vecEuclideanNorm x = 1) : seeleyExterior v x = v x

theorem CKN.seeleyExterior_fderiv_on_sphere (v : Vec 3 → ℝ) (hv : ContDiff ℝ 1 v) {x : Vec 3} (hx : vecEuclideanNorm x = 1) (z : Vec 3) : (fderiv ℝ (seeleyExterior v) x) z = (fderiv ℝ v x) z

theorem CKN.seeley_glue_hasFDerivAt {C : Set (Vec 3)} {g h : Vec 3 → ℝ} (hC : IsClosed C) {x : Vec 3} (hx : x ∈ frontier C) (hvalue : g x = h x) {L : Vec 3 →L[ℝ] ℝ} (hg : HasFDerivAt g L x) (hh : HasFDerivAt h L x) : HasFDerivAt (fun (y : Vec 3) => if y ∈ C then g y else h y) L x

theorem CKN.seeley_glue_hasFDerivAt_of_mem_interior {C : Set (Vec 3)} {g h : Vec 3 → ℝ} {x : Vec 3} (hx : x ∈ interior C) {L : Vec 3 →L[ℝ] ℝ} (hg : HasFDerivAt g L x) : HasFDerivAt (fun (y : Vec 3) => if y ∈ C then g y else h y) L x

theorem CKN.seeley_glue_hasFDerivAt_of_not_mem {C : Set (Vec 3)} {g h : Vec 3 → ℝ} {x : Vec 3} (hC : IsClosed C) (hx : x ∉ C) {L : Vec 3 →L[ℝ] ℝ} (hh : HasFDerivAt h L x) : HasFDerivAt (fun (y : Vec 3) => if y ∈ C then g y else h y) L x

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

The piecewise two-reflection extension, before a cutoff is applied.

Equations

• CKN.seeleyExtension v x = if x ∈ CKN.euclideanClosedBall 0 1 then v x else CKN.seeleyExterior v x

theorem CKN.seeleyReflectionOne_maps_closedAnnulus {x : Vec 3} (hx : x ∈ seeleyClosedAnnulus) : seeleyReflectionOne x ∈ euclideanClosedBall 0 1

theorem CKN.seeleyReflectionTwo_maps_closedAnnulus {x : Vec 3} (hx : x ∈ seeleyClosedAnnulus) : seeleyReflectionTwo x ∈ euclideanClosedBall 0 1

theorem CKN.seeleyReflectionOne_injectiveOn_closedAnnulus : Set.InjOn seeleyReflectionOne seeleyClosedAnnulus

theorem CKN.seeleyReflectionTwo_injectiveOn_closedAnnulus : Set.InjOn seeleyReflectionTwo seeleyClosedAnnulus

theorem CKN.seeleyClosedAnnulus_measurableSet : MeasurableSet seeleyClosedAnnulus

theorem CKN.seeleyReflectionOne_hasFDerivWithinAt {x : Vec 3} (hx : x ∈ seeleyClosedAnnulus) : HasFDerivWithinAt seeleyReflectionOne (fderiv ℝ seeleyReflectionOne x) seeleyClosedAnnulus x

theorem CKN.seeleyReflectionTwo_hasFDerivWithinAt {x : Vec 3} (hx : x ∈ seeleyClosedAnnulus) : HasFDerivWithinAt seeleyReflectionTwo (fderiv ℝ seeleyReflectionTwo x) seeleyClosedAnnulus x

theorem CKN.seeley_changeVariables_lintegral_one {g : Vec 3 → ENNReal} : ∫⁻ (x : Vec 3) in seeleyReflectionOne '' seeleyClosedAnnulus, g x = ∫⁻ (x : Vec 3) in seeleyClosedAnnulus, ENNReal.ofReal |(fderiv ℝ seeleyReflectionOne x).det| * g (seeleyReflectionOne x)

theorem CKN.seeley_changeVariables_lintegral_two {g : Vec 3 → ENNReal} : ∫⁻ (x : Vec 3) in seeleyReflectionTwo '' seeleyClosedAnnulus, g x = ∫⁻ (x : Vec 3) in seeleyClosedAnnulus, ENNReal.ofReal |(fderiv ℝ seeleyReflectionTwo x).det| * g (seeleyReflectionTwo x)