Exponential sums on integer frequency lattices

theorem AVenhance.Infra.Ergodic.summable_exp_neg_abs_int {a : ℝ} (ha : 0 < a) : Summable fun (z : ℤ) => Real.exp (-a * |↑z|)

Exponential weights in one integer variable are summable.

theorem AVenhance.Infra.Ergodic.LatticeDecay.summable_exp_neg_piNorm_aux (d : ℕ) {a : ℝ} : 0 < a → Summable fun (k : Fin d → ℤ) => Real.exp (-a * ‖k‖)

theorem AVenhance.Infra.Ergodic.summable_exp_neg_piNorm {d : ℕ} {a : ℝ} (ha : 0 < a) : Summable fun (k : Fin d → ℤ) => Real.exp (-a * ‖k‖)

The exponential lattice sum converges in every finite dimension.

noncomputable def AVenhance.Infra.Ergodic.LatticeDecay.fastFrequencyQuotient {d N : ℕ} (k : { k : Fin d → ℤ // IsFastFrequency N k }) : Fin d → ℤ

Quotient coordinates for the frequency sublattice N ℤ^d.

Equations

• AVenhance.Infra.Ergodic.LatticeDecay.fastFrequencyQuotient k i = Classical.choose ⋯

theorem AVenhance.Infra.Ergodic.LatticeDecay.fastFrequency_eq_scale {d N : ℕ} (k : { k : Fin d → ℤ // IsFastFrequency N k }) : ↑k = fun (i : Fin d) => ↑N * fastFrequencyQuotient k i

theorem AVenhance.Infra.Ergodic.LatticeDecay.fastFrequencyQuotient_injective {d N : ℕ} : Function.Injective fastFrequencyQuotient

theorem AVenhance.Infra.Ergodic.LatticeDecay.norm_fastFrequency_eq {d N : ℕ} (k : { k : Fin d → ℤ // IsFastFrequency N k }) : ‖↑k‖ = ↑N * ‖fastFrequencyQuotient k‖

theorem AVenhance.Infra.Ergodic.LatticeDecay.norm_ge_one_of_ne_zero_intVector {d : ℕ} {k : Fin d → ℤ} (hk : k ≠ 0) : 1 ≤ ‖k‖

theorem AVenhance.Infra.Ergodic.fastFrequency_expTail_le {d N : ℕ} (hN : 0 < N) {t : ℝ} (ht : 0 < t) (hscale : 1 / 512 ≤ t * ↑N) : (∑' (k : Fin d → ℤ), if k = 0 then 0 else if IsFastFrequency N k then Real.exp (-t * ‖k‖) else 0) ≤ (∑' (ℓ : Fin d → ℤ), Real.exp (-(1 / 1024) * ‖ℓ‖)) * Real.exp (-(t * ↑N) / 2)

The nonzero exponential tail on N ℤ^d has a dimension-only prefactor. The scale condition is tN ≥ 1/512; the estimate decays as exp(-tN/2).