The two cutoffs at the large time scale.

noncomputable def AVenhance.Infra.Cutoff.hatXiProfile (ratio x : ℝ) : ℝ

Cell cutoff with unit transition margin and a specified period ratio.

Equations

• AVenhance.Infra.Cutoff.hatXiProfile ratio x = AVenhance.Infra.Cutoff.cellCutoff AVenhance.Infra.Cutoff.step ratio 1 x

noncomputable def AVenhance.Infra.Cutoff.hatXiCutoff (period margin t : ℝ) : ℝ

Cell cutoff with a specified period and transition margin.

Equations

• AVenhance.Infra.Cutoff.hatXiCutoff period margin t = AVenhance.Infra.Cutoff.cellCutoff AVenhance.Infra.Cutoff.step period margin t

noncomputable def AVenhance.Infra.Cutoff.hatZetaProfile (ratio x : ℝ) : ℝ

Product profile for the enlarged time cutoff in normalized coordinates.

Equations

• AVenhance.Infra.Cutoff.hatZetaProfile ratio x = AVenhance.Infra.Cutoff.step (x + ratio / 2 - 1) * AVenhance.Infra.Cutoff.step (ratio / 2 - 1 - x)

noncomputable def AVenhance.Infra.Cutoff.hatZetaCutoff (period margin t : ℝ) : ℝ

Enlarged time cutoff with a specified period and transition margin.

Equations

• AVenhance.Infra.Cutoff.hatZetaCutoff period margin t = AVenhance.Infra.Cutoff.step ((t + period / 2 - margin) / margin) * AVenhance.Infra.Cutoff.step ((period / 2 - margin - t) / margin)

theorem AVenhance.Infra.Cutoff.hatXiProfile_contDiff (ratio : ℝ) : ContDiff ℝ (↑⊤) (hatXiProfile ratio)

theorem AVenhance.Infra.Cutoff.hatZetaProfile_contDiff (ratio : ℝ) : ContDiff ℝ (↑⊤) (hatZetaProfile ratio)

theorem AVenhance.Infra.Cutoff.hatXiCutoff_contDiff (period margin : ℝ) : ContDiff ℝ (↑⊤) (hatXiCutoff period margin)

theorem AVenhance.Infra.Cutoff.hatZetaCutoff_contDiff (period margin : ℝ) : ContDiff ℝ (↑⊤) (hatZetaCutoff period margin)

theorem AVenhance.Infra.Cutoff.hatXiCutoff_nonneg (period margin t : ℝ) : 0 ≤ hatXiCutoff period margin t

theorem AVenhance.Infra.Cutoff.hatXiCutoff_le_one (period margin t : ℝ) : hatXiCutoff period margin t ≤ 1

theorem AVenhance.Infra.Cutoff.hatXiCutoff_one_on_core {period margin t : ℝ} (hm : 0 < margin) (ht₁ : -period / 2 + margin ≤ t) (ht₂ : t ≤ period / 2 - margin) : hatXiCutoff period margin t = 1

theorem AVenhance.Infra.Cutoff.hatXiCutoff_zero_of_le {period margin t : ℝ} (hm : 0 < margin) (ht : t ≤ -(period / 2 + margin)) : hatXiCutoff period margin t = 0

theorem AVenhance.Infra.Cutoff.hatXiCutoff_zero_of_ge {period margin t : ℝ} (hm : 0 < margin) (ht : period / 2 + margin ≤ t) : hatXiCutoff period margin t = 0

theorem AVenhance.Infra.Cutoff.hatZetaCutoff_nonneg (period margin t : ℝ) : 0 ≤ hatZetaCutoff period margin t

theorem AVenhance.Infra.Cutoff.hatZetaCutoff_le_one (period margin t : ℝ) : hatZetaCutoff period margin t ≤ 1

theorem AVenhance.Infra.Cutoff.hatZetaCutoff_one_on_core {period margin t : ℝ} (hm : 0 < margin) (ht₁ : -period / 2 + 2 * margin ≤ t) (ht₂ : t ≤ period / 2 - 2 * margin) : hatZetaCutoff period margin t = 1

theorem AVenhance.Infra.Cutoff.hatZetaCutoff_zero_of_le {period margin t : ℝ} (hm : 0 < margin) (ht : t ≤ -period / 2 + margin) : hatZetaCutoff period margin t = 0

theorem AVenhance.Infra.Cutoff.hatZetaCutoff_zero_of_ge {period margin t : ℝ} (hm : 0 < margin) (ht : period / 2 - margin ≤ t) : hatZetaCutoff period margin t = 0

theorem AVenhance.Infra.Cutoff.hatXiCutoff_eq_profile {period margin t : ℝ} (hm : margin ≠ 0) : hatXiCutoff period margin t = hatXiProfile (period / margin) (t / margin)

theorem AVenhance.Infra.Cutoff.hatZetaCutoff_eq_profile {period margin t : ℝ} (hm : margin ≠ 0) : hatZetaCutoff period margin t = hatZetaProfile (period / margin) (t / margin)

theorem AVenhance.Infra.Cutoff.hatXiProfile_deriv_bound {N : ℕ} {M : ℝ} (hM : 1 ≤ M) (hstep : ∀ j ≤ N, ∀ (x : ℝ), |iteratedDeriv j step x| ≤ M) (ratio : ℝ) (j : ℕ) : j ≤ N → ∀ (x : ℝ), |iteratedDeriv j (hatXiProfile ratio) x| ≤ 2 ^ N * M ^ 2

theorem AVenhance.Infra.Cutoff.hatZetaProfile_deriv_bound {N : ℕ} {M : ℝ} (hM : 1 ≤ M) (hstep : ∀ j ≤ N, ∀ (x : ℝ), |iteratedDeriv j step x| ≤ M) (ratio : ℝ) (j : ℕ) : j ≤ N → ∀ (x : ℝ), |iteratedDeriv j (hatZetaProfile ratio) x| ≤ 2 ^ N * M ^ 2

theorem AVenhance.Infra.Cutoff.hatXi_partition {period margin : ℝ} (hp : 0 < period) (hm : 0 < margin) (hmp : 2 * margin ≤ period) (t : ℝ) : ∑' (l : ℤ), shiftCutoff (hatXiCutoff period margin) (↑l * period) t = 1

theorem AVenhance.Infra.Cutoff.hatXi_shift_ge {period margin : ℝ} (hm : 0 < margin) (_hspace : 2 * margin ≤ period) (l : ℤ) (t : ℝ) : indIcc ((↑l - 1 / 2) * period + margin) ((↑l + 1 / 2) * period - margin) t ≤ shiftCutoff (hatXiCutoff period margin) (↑l * period) t

theorem AVenhance.Infra.Cutoff.hatXi_shift_le {period margin : ℝ} (hm : 0 < margin) (l : ℤ) (t : ℝ) : shiftCutoff (hatXiCutoff period margin) (↑l * period) t ≤ indIcc ((↑l - 1 / 2) * period - margin) ((↑l + 1 / 2) * period + margin) t

theorem AVenhance.Infra.Cutoff.hatZeta_shift_ge {period margin : ℝ} (hm : 0 < margin) (_hspace : 4 * margin ≤ period) (l : ℤ) (t : ℝ) : indIcc ((↑l - 1 / 2) * period + 2 * margin) ((↑l + 1 / 2) * period - 2 * margin) t ≤ shiftCutoff (hatZetaCutoff period margin) (↑l * period) t

theorem AVenhance.Infra.Cutoff.hatZeta_shift_le {period margin : ℝ} (hm : 0 < margin) (l : ℤ) (t : ℝ) : shiftCutoff (hatZetaCutoff period margin) (↑l * period) t ≤ indIcc ((↑l - 1 / 2) * period + margin) ((↑l + 1 / 2) * period - margin) t

theorem AVenhance.Infra.Cutoff.hatXi_shift_normalized {period margin : ℝ} (hm : 0 < margin) (l : ℤ) : shiftCutoff (hatXiCutoff period margin) (↑l * period) = fun (t : ℝ) => hatXiProfile (period / margin) (t / margin - ↑l * (period / margin))

theorem AVenhance.Infra.Cutoff.hatZeta_shift_normalized {period margin : ℝ} (hm : 0 < margin) (l : ℤ) : shiftCutoff (hatZetaCutoff period margin) (↑l * period) = fun (t : ℝ) => hatZetaProfile (period / margin) (t / margin - ↑l * (period / margin))

theorem AVenhance.Infra.Cutoff.hatXi_scaled_deriv_bound {period margin : ℝ} {N : ℕ} {M : ℝ} (hm : 0 < margin) (hM : 1 ≤ M) (hstep : ∀ j ≤ N, ∀ (x : ℝ), |iteratedDeriv j step x| ≤ M) (_hspace : 2 * margin ≤ period) (l : ℤ) {j : ℕ} (hj : j ≤ N) (t : ℝ) : margin ^ j * |iteratedDeriv j (shiftCutoff (hatXiCutoff period margin) (↑l * period)) t| ≤ 2 ^ N * M ^ 2

theorem AVenhance.Infra.Cutoff.hatZeta_scaled_deriv_bound {period margin : ℝ} {N : ℕ} {M : ℝ} (hm : 0 < margin) (hM : 1 ≤ M) (hstep : ∀ j ≤ N, ∀ (x : ℝ), |iteratedDeriv j step x| ≤ M) (l : ℤ) {j : ℕ} (hj : j ≤ N) (t : ℝ) : margin ^ j * |iteratedDeriv j (shiftCutoff (hatZetaCutoff period margin) (↑l * period)) t| ≤ 2 ^ N * M ^ 2