Locally finite partitions generated by complementary smooth steps.

noncomputable def AVenhance.Infra.Cutoff.cellCutoff (s : ℝ → ℝ) (period margin x : ℝ) : ℝ

A one-dimensional cutoff around the center of a lattice cell. margin is the distance from the cell edge to the edge of the support.

Equations

• AVenhance.Infra.Cutoff.cellCutoff s period margin x = s ((x + period / 2 + margin) / (2 * margin)) * s ((period / 2 + margin - x) / (2 * margin))

theorem AVenhance.Infra.Cutoff.cellCutoff_even (s : ℝ → ℝ) (period margin x : ℝ) : cellCutoff s period margin (-x) = cellCutoff s period margin x

theorem AVenhance.Infra.Cutoff.cellCutoff_zero_of_le {s : ℝ → ℝ} {period margin x : ℝ} (hm : 0 < margin) (hs : ∀ y ≤ 0, s y = 0) (hx : x ≤ -(period / 2 + margin)) : cellCutoff s period margin x = 0

theorem AVenhance.Infra.Cutoff.cellCutoff_zero_of_ge {s : ℝ → ℝ} {period margin x : ℝ} (hm : 0 < margin) (hs : ∀ y ≤ 0, s y = 0) (hx : period / 2 + margin ≤ x) : cellCutoff s period margin x = 0

theorem AVenhance.Infra.Cutoff.cellCutoff_one_on_core {s : ℝ → ℝ} {period margin x : ℝ} (hm : 0 < margin) (hs : ∀ (y : ℝ), 1 ≤ y → s y = 1) (hx₁ : -period / 2 + margin ≤ x) (hx₂ : x ≤ period / 2 - margin) : cellCutoff s period margin x = 1

theorem AVenhance.Infra.Cutoff.cellCutoff_pair_right {s : ℝ → ℝ} {period margin x : ℝ} (hm : 0 < margin) (hs₁ : ∀ (y : ℝ), 1 ≤ y → s y = 1) (hs₂ : ∀ (y : ℝ), s (1 - y) = 1 - s y) (hpm : 2 * margin ≤ period) (hx₁ : period / 2 - margin ≤ x) (hx₂ : x ≤ period / 2) : cellCutoff s period margin x + cellCutoff s period margin (x - period) = 1

theorem AVenhance.Infra.Cutoff.cellCutoff_pair_left {s : ℝ → ℝ} {period margin x : ℝ} (hm : 0 < margin) (hs₁ : ∀ (y : ℝ), 1 ≤ y → s y = 1) (hs₂ : ∀ (y : ℝ), s (1 - y) = 1 - s y) (hpm : 2 * margin ≤ period) (hx₁ : -period / 2 ≤ x) (hx₂ : x ≤ -period / 2 + margin) : cellCutoff s period margin x + cellCutoff s period margin (x + period) = 1

theorem AVenhance.Infra.Cutoff.cellCutoff_lattice_partition {s : ℝ → ℝ} {period margin t : ℝ} (hperiod : 0 < period) (hmargin : 0 < margin) (hmargin' : 2 * margin ≤ period) (hzero : ∀ y ≤ 0, s y = 0) (hone : ∀ (y : ℝ), 1 ≤ y → s y = 1) (hcomp : ∀ (y : ℝ), s (1 - y) = 1 - s y) : ∑' (k : ℤ), cellCutoff s period margin (t - ↑k * period) = 1