A smooth ball cut-off with two derivative bounds

The native carrier is Fin 3 → ℝ. The cut-off below is obtained by convolving the indicator of the 7ρ/10 ball with a normalized smooth bump. The bump is chosen with a slightly smaller inherited-metric radius so that its Euclidean support has a strict collar in the native carrier. This keeps the stated Euclidean radii literal while avoiding an implicit change of norm.

noncomputable def CKN.ballIndicator (x₀ : Vec 3) (R : ℝ) : Vec 3 → ℝ

Indicator of a Euclidean ball, used as the source for mollified cutoffs.

Equations

• CKN.ballIndicator x₀ R = (CKN.euclideanBall x₀ R).indicator fun (x : CKN.Vec 3) => 1

noncomputable def CKN.unitBallCutoff : Vec 3 → ℝ

Fixed smooth unit-scale cutoff obtained by mollifying a smaller ball indicator.

Equations

• CKN.unitBallCutoff = CKN.mollify (CKN.ballIndicator 0 (7 / 10)) (1 / 100) CKN.unitBallCutoff._proof_1

noncomputable def CKN.mollifiedBallCutoff (x₀ : Vec 3) {ρ : ℝ} (_hρ : 0 < ρ) : Vec 3 → ℝ

The convolution cut-off at center x₀ and radius ρ.

Equations

• CKN.mollifiedBallCutoff x₀ _hρ x = CKN.unitBallCutoff (ρ⁻¹ • (x - x₀))

theorem CKN.mollifiedBallCutoff_smooth (x₀ : Vec 3) {ρ : ℝ} (hρ : 0 < ρ) : ContDiff ℝ (↑⊤) (mollifiedBallCutoff x₀ hρ)

theorem CKN.mollifiedBallCutoff_nonneg (x₀ : Vec 3) {ρ : ℝ} (hρ : 0 < ρ) (x : Vec 3) : 0 ≤ mollifiedBallCutoff x₀ hρ x

theorem CKN.mollifiedBallCutoff_le_one (x₀ : Vec 3) {ρ : ℝ} (hρ : 0 < ρ) (x : Vec 3) : mollifiedBallCutoff x₀ hρ x ≤ 1

theorem CKN.mollifiedBallCutoff_eq_one_on_inner (x₀ : Vec 3) {ρ : ℝ} (hρ : 0 < ρ) {x : Vec 3} (hx : x ∈ euclideanBall x₀ (13 * ρ / 20)) : mollifiedBallCutoff x₀ hρ x = 1

theorem CKN.mollifiedBallCutoff_hasCompactSupport (x₀ : Vec 3) {ρ : ℝ} (hρ : 0 < ρ) : HasCompactSupport (mollifiedBallCutoff x₀ hρ)

theorem CKN.mollifiedBallCutoff_tsupport_subset_outer (x₀ : Vec 3) {ρ : ℝ} (hρ : 0 < ρ) : tsupport (mollifiedBallCutoff x₀ hρ) ⊆ euclideanBall x₀ (3 * ρ / 4)

noncomputable def CKN.cutoffGradientConstant : ℝ

The absolute unit-scale gradient constant of the convolution cut-off.

Equations

• CKN.cutoffGradientConstant = sSup (Set.range fun (x : CKN.Vec 3) => CKN.vecEuclideanNorm (CKN.classicalGradient CKN.unitBallCutoff x))

noncomputable def CKN.cutoffSecondDerivativeConstant : ℝ

The absolute unit-scale second-derivative constant of the convolution cut-off.

Equations

• CKN.cutoffSecondDerivativeConstant = sSup (Set.range fun (x : CKN.Vec 3) => ‖fderiv ℝ (CKN.classicalGradient CKN.unitBallCutoff) x‖)

theorem CKN.mollifiedBallCutoff_derivatives_vanish_outside_annulus (x₀ : Vec 3) {ρ : ℝ} (hρ : 0 < ρ) {x : Vec 3} (hx : x ∉ euclideanBall x₀ (3 * ρ / 4) \ euclideanClosedBall x₀ (13 * ρ / 20)) : classicalGradient (mollifiedBallCutoff x₀ hρ) x = 0 ∧ fderiv ℝ (classicalGradient (mollifiedBallCutoff x₀ hρ)) x = 0

theorem CKN.cutoff_annulus_distance (x₀ : Vec 3) {ρ r : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hrr : r ≤ ρ / 2) {x y : Vec 3} (hx : x ∈ euclideanBall x₀ r) (hy : y ∈ euclideanBall x₀ (3 * ρ / 4) \ euclideanClosedBall x₀ (13 * ρ / 20)) : 3 * ρ / 20 ≤ vecEuclideanNorm (x - y)

theorem CKN.mollifiedBallCutoff_gradient_bound (x₀ : Vec 3) {ρ : ℝ} (hρ : 0 < ρ) (x : Vec 3) : vecEuclideanNorm (classicalGradient (mollifiedBallCutoff x₀ hρ) x) ≤ cutoffGradientConstant / ρ

theorem CKN.mollifiedBallCutoff_second_derivative_bound (x₀ : Vec 3) {ρ : ℝ} (hρ : 0 < ρ) (x : Vec 3) : ‖fderiv ℝ (classicalGradient (mollifiedBallCutoff x₀ hρ)) x‖ ≤ cutoffSecondDerivativeConstant / ρ ^ 2