Trapezoidal cutoff functions

DefinitionInterval cutoff#✓fully proved

For real numbers \(a\), \(b\) and \(\delta\), the interval cutoff is the function \(\chi_{a,b,\delta} \colon \mathbb{R} \to \mathbb{R}\) defined by

\[ \chi_{a,b,\delta}(x) = \max\{0, \min\{1, (x - a)/\delta, (b - x)/\delta\}\}, \]

where division by zero is taken to give \(0\).

It vanishes at \(a\) and at \(b\). For \(\delta > 0\) it equals \(1\) on \([a + \delta, b - \delta]\), which is nonempty when \(2\delta \le b - a\); for \(\delta = 0\) it is identically zero.

noncomputable def intervalCutoff (a b δ x : ℝ) : ℝ :=
  max 0 (min 1 (min ((x - a) / δ) ((b - x) / δ)))

Used by 11

Used byContinuity of the interval cutoff · The interval cutoff equals one on its plateau · The interval cutoff vanishes at the left endpoint · The interval cutoff vanishes right of the interval · The interval cutoff vanishes left of the interval · The interval cutoff vanishes at the right endpoint · The interval cutoff is at most one · The interval cutoff is nonnegative · The interval cutoff of zero width vanishes · Vanishing cutoff factor · Weyl's equidistribution criterion

TheoremThe interval cutoff is nonnegative#✓fully proved

For all real numbers \(a\), \(b\), \(\delta\) and \(x\), the interval cutoff \(\chi_{a,b,\delta}\) with endpoints \(a\), \(b\) and width \(\delta\) satisfies \(0 \le \chi_{a,b,\delta}(x)\).

theorem intervalCutoff_nonneg (a b δ x : ℝ) : 0 ≤ intervalCutoff a b δ x

Uses 1 · Used by 2

Statement usesInterval cutoff

Used byThe vanishing cutoff factor is nonnegative · Weyl's equidistribution criterion

TheoremThe interval cutoff is at most one#✓fully proved

For all real numbers \(a\), \(b\), \(\delta\) and \(x\), the interval cutoff \(\chi_{a,b,\delta}\) with endpoints \(a\), \(b\) and width \(\delta\) satisfies \(\chi_{a,b,\delta}(x) \le 1\).

theorem intervalCutoff_le_one (a b δ x : ℝ) : intervalCutoff a b δ x ≤ 1

Uses 1 · Used by 2

Statement usesInterval cutoff

Used byThe vanishing cutoff factor is at most one · Weyl's equidistribution criterion

TheoremContinuity of the interval cutoff#✓fully proved

For all real numbers \(a\), \(b\) and \(\delta\), including \(\delta = 0\), the interval cutoff \(\chi_{a,b,\delta} \colon \mathbb{R} \to \mathbb{R}\) with endpoints \(a\), \(b\) and width \(\delta\) is continuous.

theorem intervalCutoff_continuous (a b δ : ℝ) : Continuous (intervalCutoff a b δ)

Uses 1 · Used by 2

Statement usesInterval cutoff

Used byContinuity of the vanishing cutoff factor · Weyl's equidistribution criterion

TheoremThe interval cutoff vanishes at the left endpoint#✓fully proved

For all real numbers \(a\), \(b\) and \(\delta\), the interval cutoff \(\chi_{a,b,\delta}\) with endpoints \(a\), \(b\) and width \(\delta\) satisfies \(\chi_{a,b,\delta}(a) = 0\).

theorem intervalCutoff_eq_zero_left (a b δ : ℝ) : intervalCutoff a b δ a = 0

Uses 1 · Used by 1

Statement usesInterval cutoff

Used byThe vanishing cutoff factor vanishes at the left endpoint

TheoremThe interval cutoff vanishes at the right endpoint#✓fully proved

For all real numbers \(a\), \(b\) and \(\delta\), the interval cutoff \(\chi_{a,b,\delta}\) with endpoints \(a\), \(b\) and width \(\delta\) satisfies \(\chi_{a,b,\delta}(b) = 0\).

theorem intervalCutoff_eq_zero_right (a b δ : ℝ) : intervalCutoff a b δ b = 0

Uses 1 · Used by 1

Statement usesInterval cutoff

Used byThe vanishing cutoff factor vanishes at the right endpoint

TheoremThe interval cutoff of zero width vanishes#✓fully proved

For all real numbers \(a\), \(b\) and \(x\), the interval cutoff \(\chi_{a,b,0}\) with endpoints \(a\), \(b\) and width \(0\) satisfies \(\chi_{a,b,0}(x) = 0\).

theorem intervalCutoff_zero_width (a b x : ℝ) : intervalCutoff a b 0 x = 0

Uses 1

Statement usesInterval cutoff

TheoremThe interval cutoff vanishes left of the interval#✓fully proved

For real numbers \(a\), \(b\), \(\delta\) and \(x\) with \(\delta > 0\) and \(x \le a\), the interval cutoff \(\chi_{a,b,\delta}\) with endpoints \(a\), \(b\) and width \(\delta\) satisfies \(\chi_{a,b,\delta}(x) = 0\).

theorem intervalCutoff_eq_zero_of_le (a b δ x : ℝ) (hδ : 0 < δ) (hx : x ≤ a) :
    intervalCutoff a b δ x = 0

Uses 1 · Used by 1

Statement usesInterval cutoff

Used byWeyl's equidistribution criterion

TheoremThe interval cutoff vanishes right of the interval#✓fully proved

For real numbers \(a\), \(b\), \(\delta\) and \(x\) with \(\delta > 0\) and \(b \le x\), the interval cutoff \(\chi_{a,b,\delta}\) with endpoints \(a\), \(b\) and width \(\delta\) satisfies \(\chi_{a,b,\delta}(x) = 0\).

theorem intervalCutoff_eq_zero_of_ge (a b δ x : ℝ) (hδ : 0 < δ) (hx : b ≤ x) :
    intervalCutoff a b δ x = 0

Uses 1 · Used by 1

Statement usesInterval cutoff

Used byWeyl's equidistribution criterion

TheoremThe interval cutoff equals one on its plateau#✓fully proved

For real numbers \(a\), \(b\), \(\delta\) and \(x\) with \(\delta > 0\) and \(a + \delta \le x \le b - \delta\), the interval cutoff \(\chi_{a,b,\delta}\) with endpoints \(a\), \(b\) and width \(\delta\) satisfies \(\chi_{a,b,\delta}(x) = 1\).

theorem intervalCutoff_eq_one (a b δ x : ℝ) (hδ : 0 < δ)
    (hx1 : a + δ ≤ x) (hx2 : x ≤ b - δ) : intervalCutoff a b δ x = 1

Uses 1 · Used by 2

Statement usesInterval cutoff

Used byThe vanishing cutoff factor equals one on its plateau · Weyl's equidistribution criterion

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.