Coarse-graining support: Support.Sobolev.Foundations.Cutoff.Ball

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Ball cutoffs on Vec d

This file builds the smooth squared-radius cutoff formula using the explicit Euclidean balls from Cutoff.Euclidean.

noncomputable def HCPolySupport.QuantitativeTransitionProfile.ballArgument {d : ℕ} (x₀ : Vec d) (r s : ℝ) (x : Vec d) : ℝ

Squared-radius interpolation variable for a Euclidean ball cutoff.

Equations

• HCPolySupport.QuantitativeTransitionProfile.ballArgument x₀ r s x = (s ^ 2 - HCPolySupport.euclideanSqDist x x₀) / (s ^ 2 - r ^ 2)

noncomputable def HCPolySupport.QuantitativeTransitionProfile.ballCutoff {d : ℕ} (θ : QuantitativeTransitionProfile) (x₀ : Vec d) (r s : ℝ) (x : Vec d) : ℝ

Ball cutoff generated by a one-dimensional transition profile.

Equations

• θ.ballCutoff x₀ r s x = θ.toFun (HCPolySupport.QuantitativeTransitionProfile.ballArgument x₀ r s x)

theorem HCPolySupport.QuantitativeTransitionProfile.fderiv_ballArgument_apply_basisVec {d : ℕ} (x₀ : Vec d) (r s : ℝ) (j : Fin d) (x : Vec d) : (fderiv ℝ (ballArgument x₀ r s) x) (basisVec j) = -(2 * (x j - x₀ j)) / (s ^ 2 - r ^ 2)

Exact coordinate-direction derivative of the ball interpolation variable.

theorem HCPolySupport.QuantitativeTransitionProfile.norm_fderiv_ballArgument_le_of_mem_euclideanClosedBall {d : ℕ} {x₀ : Vec d} {r s : ℝ} (hr : 0 < r) (hrs : r < s) {x : Vec d} (hx : x ∈ euclideanClosedBall x₀ s) : ‖fderiv ℝ (ballArgument x₀ r s) x‖ ≤ 2 * ↑d / (s - r)

On the outer closed ball, the ball interpolation variable has first derivative of size at most 2 d / (s - r) in the default product/sup norm on Vec d.

theorem HCPolySupport.QuantitativeTransitionProfile.norm_iteratedFDeriv_two_ballArgument_le {d : ℕ} {x₀ : Vec d} {r s : ℝ} (hr : 0 < r) (hrs : r < s) (x : Vec d) : ‖iteratedFDeriv ℝ 2 (ballArgument x₀ r s) x‖ ≤ 2 * ↑d / (s - r) ^ 2

Global second-derivative bound for the ball interpolation variable.

theorem HCPolySupport.QuantitativeTransitionProfile.ballCutoff_smooth {d : ℕ} (θ : QuantitativeTransitionProfile) (x₀ : Vec d) {r s : ℝ} (hr : 0 < r) (hrs : r < s) : ContDiff ℝ (↑⊤) (θ.ballCutoff x₀ r s)

theorem HCPolySupport.QuantitativeTransitionProfile.ballCutoff_nonneg {d : ℕ} (θ : QuantitativeTransitionProfile) (x₀ : Vec d) (r s : ℝ) (x : Vec d) : 0 ≤ θ.ballCutoff x₀ r s x

theorem HCPolySupport.QuantitativeTransitionProfile.ballCutoff_le_one {d : ℕ} (θ : QuantitativeTransitionProfile) (x₀ : Vec d) (r s : ℝ) (x : Vec d) : θ.ballCutoff x₀ r s x ≤ 1

theorem HCPolySupport.QuantitativeTransitionProfile.ballCutoff_eq_one_of_mem_euclideanBall {d : ℕ} (θ : QuantitativeTransitionProfile) {x₀ : Vec d} {r s : ℝ} (hr : 0 < r) (hrs : r < s) {x : Vec d} (hx : x ∈ euclideanBall x₀ r) : θ.ballCutoff x₀ r s x = 1

theorem HCPolySupport.QuantitativeTransitionProfile.ballCutoff_eq_zero_of_notMem_euclideanClosedBall {d : ℕ} (θ : QuantitativeTransitionProfile) {x₀ : Vec d} {r s : ℝ} (hr : 0 < r) (hrs : r < s) {x : Vec d} (hx : x ∉ euclideanClosedBall x₀ s) : θ.ballCutoff x₀ r s x = 0

theorem HCPolySupport.QuantitativeTransitionProfile.ballCutoff_support_subset_euclideanClosedBall {d : ℕ} (θ : QuantitativeTransitionProfile) {x₀ : Vec d} {r s : ℝ} (hr : 0 < r) (hrs : r < s) : Function.support (θ.ballCutoff x₀ r s) ⊆ euclideanClosedBall x₀ s

theorem HCPolySupport.QuantitativeTransitionProfile.ballCutoff_tsupport_subset_euclideanClosedBall {d : ℕ} (θ : QuantitativeTransitionProfile) {x₀ : Vec d} {r s : ℝ} (hr : 0 < r) (hrs : r < s) : tsupport (θ.ballCutoff x₀ r s) ⊆ euclideanClosedBall x₀ s

theorem HCPolySupport.QuantitativeTransitionProfile.ballCutoff_hasCompactSupport {d : ℕ} (θ : QuantitativeTransitionProfile) {x₀ : Vec d} {r s : ℝ} (hr : 0 < r) (hrs : r < s) : HasCompactSupport (θ.ballCutoff x₀ r s)

theorem HCPolySupport.QuantitativeTransitionProfile.norm_fderiv_ballCutoff_le {d : ℕ} (θ : QuantitativeTransitionProfile) {x₀ : Vec d} {r s : ℝ} (hr : 0 < r) (hrs : r < s) (x : Vec d) : ‖fderiv ℝ (θ.ballCutoff x₀ r s) x‖ ≤ θ.derivBound * (2 * ↑d / (s - r))

Global first-derivative bound for the ball cutoff with an intermediate support radius.

theorem HCPolySupport.QuantitativeTransitionProfile.norm_iteratedFDeriv_two_ballCutoff_le {d : ℕ} (θ : QuantitativeTransitionProfile) {x₀ : Vec d} {r s : ℝ} (hr : 0 < r) (hrs : r < s) (x : Vec d) : ‖iteratedFDeriv ℝ 2 (θ.ballCutoff x₀ r s) x‖ ≤ 2 * max 1 (max θ.derivBound θ.secondDerivBound) * (2 * ↑d / (s - r)) ^ 2

Global second-derivative bound for the ball cutoff with an intermediate support radius.

theorem HCPolySupport.QuantitativeTransitionProfile.ballCutoff_tsupport_subset_euclideanBall {d : ℕ} (θ : QuantitativeTransitionProfile) {x₀ : Vec d} {r s R : ℝ} (hr : 0 < r) (hrs : r < s) (hsR : s < R) : tsupport (θ.ballCutoff x₀ r s) ⊆ euclideanBall x₀ R