The odd cutoff tsum as an integer sum on its filtered finite support.

theorem AVenhance.Infra.Section5.xiMK_odd_tsum_eq_integer_filtered_sum {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (t : ℝ) {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] [Module ℝ α] (F : ℤ → α) : ∑' (q : { k : ℤ // Odd k }), I.xiMK m (↑q) t • F ↑q = ∑ k ∈ ⋯.toFinset with Odd k, I.xiMK m k t • F k

Convert an odd-subtype cutoff tsum to the corresponding finite sum over the integer support filtered to odd indices.

theorem AVenhance.Infra.Section5.xiMK_odd_integer_support_sum_eq_subtype_sum {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (t : ℝ) {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] [Module ℝ α] (F : ℤ → α) : ∑ k ∈ ⋯.toFinset with Odd k, I.xiMK m k t • F k = ∑ q ∈ ⋯.toFinset, I.xiMK m (↑q) t • F ↑q

Reindex an odd-filtered integer support sum to the finite odd-subtype support.

theorem AVenhance.Infra.Section5.xiMK_odd_tsum_eq_subtype_support_sum {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (t : ℝ) {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] [Module ℝ α] (F : { k : ℤ // Odd k } → α) : ∑' (q : { k : ℤ // Odd k }), I.xiMK m (↑q) t • F q = ∑ q ∈ ⋯.toFinset, I.xiMK m (↑q) t • F q

The odd cutoff tsum directly as a sum over the finite odd-subtype support.