The unit-scale cutoff with a partition on odd integer translates.

noncomputable def AVenhance.Infra.Cutoff.cardinalXi (t : ℝ) : ℝ

Cardinal cutoff profile with period two and transition margin one quarter.

Equations

• AVenhance.Infra.Cutoff.cardinalXi t = AVenhance.Infra.Cutoff.cellCutoff AVenhance.Infra.Cutoff.cardinalStep 2 (1 / 4) t

theorem AVenhance.Infra.Cutoff.cardinalXi_contDiff : ContDiff ℝ (↑⊤) cardinalXi

theorem AVenhance.Infra.Cutoff.cardinalXi_nonneg (t : ℝ) : 0 ≤ cardinalXi t

theorem AVenhance.Infra.Cutoff.cardinalXi_le_one (t : ℝ) : cardinalXi t ≤ 1

theorem AVenhance.Infra.Cutoff.cardinalXi_eq_one {t : ℝ} (ht₁ : -3 / 4 ≤ t) (ht₂ : t ≤ 3 / 4) : cardinalXi t = 1

theorem AVenhance.Infra.Cutoff.cardinalXi_eq_zero_of_le {t : ℝ} (ht : t ≤ -(5 / 4)) : cardinalXi t = 0

theorem AVenhance.Infra.Cutoff.cardinalXi_eq_zero_of_ge {t : ℝ} (ht : 5 / 4 ≤ t) : cardinalXi t = 0

theorem AVenhance.Infra.Cutoff.cardinalXi_le_indIcc (t : ℝ) : cardinalXi t ≤ indIcc (-(5 / 4)) (5 / 4) t

theorem AVenhance.Infra.Cutoff.cardinalXi_ind_le (t : ℝ) : indIcc (-(3 / 4)) (3 / 4) t ≤ cardinalXi t

theorem AVenhance.Infra.Cutoff.cardinalXi_compact : HasCompactSupport cardinalXi

theorem AVenhance.Infra.Cutoff.cardinalXi_deriv_bound (N : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ j ≤ N, ∀ (t : ℝ), |iteratedDeriv j cardinalXi t| ≤ C

def AVenhance.Infra.Cutoff.BaseCutoffs.oddIntEquiv : ℤ ≃ { k : ℤ // Odd k }

Enumerate the odd integers by the map sending an integer to twice it plus one.

Equations

• AVenhance.Infra.Cutoff.BaseCutoffs.oddIntEquiv = { toFun := fun (n : ℤ) => ⟨2 * n + 1, ⋯⟩, invFun := fun (k : { k : ℤ // Odd k }) => (↑k - 1) / 2, left_inv := ⋯, right_inv := ⋯ }

theorem AVenhance.Infra.Cutoff.cardinalXi_partition (t : ℝ) : ∑' (k : { k : ℤ // Odd k }), cardinalXi (t - ↑↑k) = 1