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

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

Smooth box cutoffs

For a closed axis box B = ∏ᵢ [loᵢ, hiᵢ] (lo ≤ hi componentwise) and a margin ℓ > 0, this file constructs a smooth cutoff η : Vec d → ℝ (Vec d = Fin d → ℝ) that is 1 on B, 0 off the ℓ-enlargement ∏ᵢ [loᵢ − ℓ, hiᵢ + ℓ], valued in [0, 1], with coordinate partial derivatives bounded by 16 / ℓ.

The construction is the coordinatewise product η(x) = ∏ᵢ ψᵢ(xᵢ) of the one-dimensional plateau profiles ψᵢ = profile (loᵢ) (hiᵢ) ℓ, each built from Real.smoothTransition. The development has three layers:

• an explicit derivative bound |smoothTransition'| ≤ 8, proved by elementary calculus on the building block expNegInvGlue;
• the one-dimensional plateau profile lo hi ℓ, equal to 1 on [lo, hi], 0 off [lo − ℓ, hi + ℓ], with derivative bounded by 16 / ℓ;
• the d-dimensional product cutoff boxCutoff, bundled as SmoothBoxCutoff, with the coordinate derivative bound, squared-gradient bound, and support-volume bound (exists_smoothBoxCutoff).

Partial derivatives are exposed as fderiv ℝ η x (Pi.single i 1), matching the ambient HasWeakPartialDerivOn pairing. The explicit gradient constant is C = 16.

theorem HCPolySupport.expNegInvGlue_le_one (x : ℝ) : expNegInvGlue x ≤ 1

expNegInvGlue never exceeds 1.

theorem HCPolySupport.expNegInvGlue_hasDerivAt (x : ℝ) : HasDerivAt expNegInvGlue (x⁻¹ ^ 2 * expNegInvGlue x) x

The derivative of expNegInvGlue at x equals x⁻² · expNegInvGlue x (interpreting 0⁻¹ = 0, so both sides vanish for x ≤ 0).

theorem HCPolySupport.mul_exp_neg_le (s : ℝ) : s * Real.exp (-s) ≤ Real.exp (-1)

One-variable calculus fact: s · e^{-s} ≤ e^{-1} for every real s (equality at s = 1).

theorem HCPolySupport.expNegInvGlue_deriv_le (x : ℝ) : x⁻¹ ^ 2 * expNegInvGlue x ≤ 4 * Real.exp (-2)

Derivative maximum for the building block: x⁻² · expNegInvGlue x ≤ 4 e⁻² for every x. The sharp value 4 e⁻² is attained at x = 1/2.

theorem HCPolySupport.expNegInvGlue_ge_of_half_le {y : ℝ} (hy : 1 / 2 ≤ y) : Real.exp (-2) ≤ expNegInvGlue y

On [1/2, ∞) the building block is bounded below by e⁻².

theorem HCPolySupport.denom_ge (x : ℝ) : Real.exp (-2) ≤ expNegInvGlue x + expNegInvGlue (1 - x)

Denominator lower bound for smoothTransition: since one of x, 1 - x is ≥ 1/2, we have e⁻² ≤ g x + g(1 - x).

theorem HCPolySupport.smoothTransition_hasDerivAt (x : ℝ) : HasDerivAt Real.smoothTransition ((x⁻¹ ^ 2 * expNegInvGlue x * expNegInvGlue (1 - x) + expNegInvGlue x * ((1 - x)⁻¹ ^ 2 * expNegInvGlue (1 - x))) / (expNegInvGlue x + expNegInvGlue (1 - x)) ^ 2) x

Explicit derivative of Real.smoothTransition, in the form (g'(x) g(1-x) + g(x) g'(1-x)) / (g(x) + g(1-x))² with both numerator summands manifestly nonnegative.

theorem HCPolySupport.smoothTransition_deriv_abs_le (x : ℝ) : |deriv Real.smoothTransition x| ≤ 8

Explicit derivative bound for Real.smoothTransition. For every x, |smoothTransition'(x)| ≤ 8. (The sharp constant is 2, at x = 1/2; 8 is what the elementary route below delivers.)

noncomputable def HCPolySupport.profile (lo hi ℓ t : ℝ) : ℝ

One-dimensional smooth plateau profile: 1 on [lo, hi], 0 off [lo - ℓ, hi + ℓ], valued in [0, 1].

Equations

• HCPolySupport.profile lo hi ℓ t = ((t - (lo - ℓ)) / ℓ).smoothTransition * ((hi + ℓ - t) / ℓ).smoothTransition

theorem HCPolySupport.profile_nonneg {lo hi ℓ : ℝ} (t : ℝ) : 0 ≤ profile lo hi ℓ t

theorem HCPolySupport.profile_le_one {lo hi ℓ : ℝ} (t : ℝ) : profile lo hi ℓ t ≤ 1

theorem HCPolySupport.profile_abs_le_one {lo hi ℓ : ℝ} (t : ℝ) : |profile lo hi ℓ t| ≤ 1

theorem HCPolySupport.profile_contDiff {lo hi ℓ : ℝ} : ContDiff ℝ (↑⊤) (profile lo hi ℓ)

theorem HCPolySupport.profile_differentiable {lo hi ℓ : ℝ} : Differentiable ℝ (profile lo hi ℓ)

theorem HCPolySupport.profile_eq_one {lo hi ℓ : ℝ} (hℓ : 0 < ℓ) {t : ℝ} (hlo : lo ≤ t) (hhi : t ≤ hi) : profile lo hi ℓ t = 1

The profile is identically 1 on the core interval [lo, hi].

theorem HCPolySupport.profile_eq_zero_left {lo hi ℓ : ℝ} (hℓ : 0 < ℓ) {t : ℝ} (ht : t ≤ lo - ℓ) : profile lo hi ℓ t = 0

The profile vanishes to the left of the enlarged interval.

theorem HCPolySupport.profile_eq_zero_right {lo hi ℓ : ℝ} (hℓ : 0 < ℓ) {t : ℝ} (ht : hi + ℓ ≤ t) : profile lo hi ℓ t = 0

The profile vanishes to the right of the enlarged interval.

theorem HCPolySupport.profile_eq_zero_of_notMem {lo hi ℓ : ℝ} (hℓ : 0 < ℓ) {t : ℝ} (ht : t ∉ Set.Icc (lo - ℓ) (hi + ℓ)) : profile lo hi ℓ t = 0

Off the enlarged interval [lo - ℓ, hi + ℓ] the profile is 0.

theorem HCPolySupport.profile_deriv_abs_le {lo hi ℓ : ℝ} (hℓ : 0 < ℓ) (t : ℝ) : |deriv (profile lo hi ℓ) t| ≤ 16 / ℓ

Derivative bound for the 1-d profile: |profile'(t)| ≤ 16 / ℓ.

noncomputable def HCPolySupport.boxCutoff {d : ℕ} (lo hi : Vec d) (ℓ : ℝ) : Vec d → ℝ

The smooth box cutoff: coordinatewise product of the 1-d plateau profiles.

Equations

• HCPolySupport.boxCutoff lo hi ℓ x = ∏ i : Fin d, HCPolySupport.profile (lo i) (hi i) ℓ (x i)

theorem HCPolySupport.boxCutoff_apply {d : ℕ} {lo hi : Vec d} {ℓ : ℝ} (x : Vec d) : boxCutoff lo hi ℓ x = ∏ i : Fin d, profile (lo i) (hi i) ℓ (x i)

theorem HCPolySupport.factor_contDiff {d : ℕ} {lo hi : Vec d} {ℓ : ℝ} (i : Fin d) : ContDiff ℝ ↑⊤ fun (x : Vec d) => profile (lo i) (hi i) ℓ (x i)

Each coordinate factor is C^∞.

theorem HCPolySupport.boxCutoff_contDiff {d : ℕ} {lo hi : Vec d} {ℓ : ℝ} : ContDiff ℝ (↑⊤) (boxCutoff lo hi ℓ)

theorem HCPolySupport.boxCutoff_nonneg {d : ℕ} {lo hi : Vec d} {ℓ : ℝ} (x : Vec d) : 0 ≤ boxCutoff lo hi ℓ x

theorem HCPolySupport.boxCutoff_le_one {d : ℕ} {lo hi : Vec d} {ℓ : ℝ} (x : Vec d) : boxCutoff lo hi ℓ x ≤ 1

theorem HCPolySupport.boxCutoff_eq_one {d : ℕ} {lo hi : Vec d} {ℓ : ℝ} (hℓ : 0 < ℓ) {x : Vec d} (hx : x ∈ Set.Icc lo hi) : boxCutoff lo hi ℓ x = 1

On the core box x ∈ [lo, hi], the cutoff is identically 1.

theorem HCPolySupport.boxCutoff_eq_zero {d : ℕ} {lo hi : Vec d} {ℓ : ℝ} (hℓ : 0 < ℓ) {x : Vec d} (hx : x ∉ Set.Icc (fun (i : Fin d) => lo i - ℓ) fun (i : Fin d) => hi i + ℓ) : boxCutoff lo hi ℓ x = 0

Off the ℓ-enlargement [lo - ℓ, hi + ℓ], the cutoff vanishes.

theorem HCPolySupport.boxCutoff_hasFDerivAt {d : ℕ} {lo hi : Vec d} {ℓ : ℝ} (x : Vec d) : HasFDerivAt (boxCutoff lo hi ℓ) (∑ i : Fin d, (∏ j ∈ Finset.univ.erase i, profile (lo j) (hi j) ℓ (x j)) • deriv (profile (lo i) (hi i) ℓ) (x i) • ContinuousLinearMap.proj i) x

HasFDerivAt for the box cutoff, via the finite-product rule on the coordinate factors.

theorem HCPolySupport.boxCutoff_fderiv_single {d : ℕ} {lo hi : Vec d} {ℓ : ℝ} (x : Vec d) (k : Fin d) : (fderiv ℝ (boxCutoff lo hi ℓ) x) (Pi.single k 1) = (∏ j ∈ Finset.univ.erase k, profile (lo j) (hi j) ℓ (x j)) * deriv (profile (lo k) (hi k) ℓ) (x k)

The i-th partial derivative of the box cutoff: only the i-th factor is differentiated, the rest form the product with i removed.

theorem HCPolySupport.boxCutoff_deriv_bound {d : ℕ} {lo hi : Vec d} {ℓ : ℝ} (hℓ : 0 < ℓ) (x : Vec d) (k : Fin d) : |(fderiv ℝ (boxCutoff lo hi ℓ) x) (Pi.single k 1)| ≤ 16 / ℓ

Coordinate derivative bound: |∂ᵢ η x| ≤ 16 / ℓ (with C = 16).

theorem HCPolySupport.boxCutoff_sq_grad_bound {d : ℕ} {lo hi : Vec d} {ℓ : ℝ} (hℓ : 0 < ℓ) (x : Vec d) : ∑ i : Fin d, (fderiv ℝ (boxCutoff lo hi ℓ) x) (Pi.single i 1) ^ 2 ≤ ↑d * (16 / ℓ) ^ 2

Squared-gradient bound: Σᵢ |∂ᵢ η x|² ≤ d · (16/ℓ)².

theorem HCPolySupport.boxCutoff_support_volume_le {d : ℕ} {lo hi : Vec d} {ℓ : ℝ} (hℓ : 0 < ℓ) (hle : lo ≤ hi) : MeasureTheory.volume (Function.support (boxCutoff lo hi ℓ)) ≤ ENNReal.ofReal (∏ i : Fin d, (hi i - lo i + 2 * ℓ))

Support-volume bound: the support of η is contained in the enlarged box, whose volume is ∏ᵢ (hiᵢ − loᵢ + 2ℓ).

structure HCPolySupport.SmoothBoxCutoff {d : ℕ} (lo hi : Vec d) (ℓ : ℝ) : Type

Bundled smooth box cutoff data (support, range, plateau, and derivative bounds as named fields).

• toFun : Vec d → ℝ

  The cutoff function.

• contDiff : ContDiff ℝ (↑⊤) self.toFun

  Smoothness.

• mem_Icc (x : Vec d) : self.toFun x ∈ Set.Icc 0 1

  Values lie in [0, 1].

• eq_one_of_mem (x : Vec d) : x ∈ Set.Icc lo hi → self.toFun x = 1

  Identically 1 on the core box [lo, hi].

• eq_zero_of_notMem_enlarged (x : Fin d → ℝ) : (x ∉ Set.Icc (fun (i : Fin d) => lo i - ℓ) fun (i : Fin d) => hi i + ℓ) → self.toFun x = 0

  Vanishes off the ℓ-enlargement [lo − ℓ, hi + ℓ].

• deriv_bound (x : Vec d) (i : Fin d) : |(fderiv ℝ self.toFun x) (Pi.single i 1)| ≤ 16 / ℓ

  Coordinate derivative bound with explicit constant 16 / ℓ.

noncomputable def HCPolySupport.smoothBoxCutoff {d : ℕ} (lo hi : Vec d) {ℓ : ℝ} (hℓ : 0 < ℓ) : SmoothBoxCutoff lo hi ℓ

The concrete smooth box cutoff.

Equations

• HCPolySupport.smoothBoxCutoff lo hi hℓ = { toFun := HCPolySupport.boxCutoff lo hi ℓ, contDiff := ⋯, mem_Icc := ⋯, eq_one_of_mem := ⋯, eq_zero_of_notMem_enlarged := ⋯, deriv_bound := ⋯ }

theorem HCPolySupport.exists_smoothBoxCutoff {d : ℕ} (lo hi : Vec d) (ℓ : ℝ) (hℓ : 0 < ℓ) (hle : lo ≤ hi) : ∃ (η : Vec d → ℝ), ContDiff ℝ (↑⊤) η ∧ (∀ (x : Vec d), η x ∈ Set.Icc 0 1) ∧ (∀ x ∈ Set.Icc lo hi, η x = 1) ∧ (∀ x ∉ Set.Icc (fun (i : Fin d) => lo i - ℓ) fun (i : Fin d) => hi i + ℓ, η x = 0) ∧ (∀ (x : Vec d) (i : Fin d), |(fderiv ℝ η x) (Pi.single i 1)| ≤ 16 / ℓ) ∧ (∀ (x : Vec d), ∑ i : Fin d, (fderiv ℝ η x) (Pi.single i 1) ^ 2 ≤ ↑d * (16 / ℓ) ^ 2) ∧ MeasureTheory.volume (Function.support η) ≤ ENNReal.ofReal (∏ i : Fin d, (hi i - lo i + 2 * ℓ))

Smooth box cutoff existence theorem. For any closed box [lo, hi] (lo ≤ hi) and margin ℓ > 0, there is a C^∞ cutoff, valued in [0, 1], equal to 1 on the box, supported in the ℓ-enlargement, with coordinate derivative bound 16/ℓ, squared-gradient bound d·(16/ℓ)², and support volume ≤ ∏ᵢ (hiᵢ−loᵢ+2ℓ).