Reindex finite sums between the odd-integer support and its odd subtype, and identify the corresponding locally finite tsum.

theorem AVenhance.Infra.Section5.xiMK_odd_support_sum_reindex {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (t : ℝ) {α : Type u_1} [AddCommMonoid α] (F : { k : ℤ // Odd k } → α) : (let S := Finset.filter Odd ⋯.toFinset; ∑ q ∈ S.attach, F ⟨↑q, ⋯⟩) = ∑ k ∈ ⋯.toFinset, F k

Reindex the odd support of xiMK from the filtered integer support to the source's odd subtype.

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

A compact form of tsum_eq_sum for the odd cutoff support.