Generalize Fin.sum_univ_odd_even to arbitrary r

[MavenRain]

Add Fin.sum_univ_even_odd splitting ∑ Fin (2*r) into even and odd index sums, generalizing the previous 2^n-specific version. The original Fin.sum_univ_odd_even is retained as a thin specialization. Remove resolved TODO.

[github-actions]

🤖 Gemini PR Summary

Mathematical Formalization

• Generalizes summation splitting over Fin (2 * r) via Fin.sum_univ_even_odd, which decomposes $\sum_{i \in \text{Fin}(2 \cdot r)} f(i)$ into separate sums over even and odd indices.
• Redefines Fin.sum_univ_odd_even as a thin specialization of the generalized theorem to preserve API stability for $2^n$ ranges.
• Ensures indexing logic correctly maps interleaved elements from the original set to the resulting sub-sum indices.

Refactoring

• Streamlines proof scripts in CompPoly/Data/Fin/BigOperators.lean using more concise tactics to reduce maintenance overhead.
• Removes a resolved TODO regarding the implementation of this generalization.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	27
❌ Lines Removed	52

---

Lean Declarations

✏️ **Added:** 1 declaration(s)

• theorem Fin.sum_univ_even_odd {r : ℕ} {M : Type*} [AddCommMonoid M] (f : ℕ → M) : in CompPoly/Data/Fin/BigOperators.lean

✏️ **Affected:** 1 declaration(s) (line number changed)

• theorem Fin.sum_univ_odd_even {n : ℕ} {M : Type*} [AddCommMonoid M] (f : ℕ → M) : in CompPoly/Data/Fin/BigOperators.lean moved from L172 to L207

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following lines violate the style guide:

• Line 170: Splits a sum over Fin (2 * r) into a sum over even indices and a sum over odd indices.
  • "Use backticks for Lean names: `List.map`." (for Fin)
  • "Use LaTeX for math: $ f(x) = y $." (for 2 * r)
• Line 171: Generalizes Fin.sum_univ_odd_even from 2^n to arbitrary r.
  • "Use backticks for Lean names: `List.map`." (for Fin.sum_univ_odd_even)
  • "Use LaTeX for math: $ f(x) = y $." (for 2^n and r)
• Line 177: set f_even := fun i => f (2 * i)
  • "Functions: Prefer fun x ↦ ... over λ x, ...." (The guideline implies using the ↦ arrow).
• Line 178: set f_odd := fun i => f (2 * i + 1)
  • "Functions: Prefer fun x ↦ ... over λ x, ...."
• Line 181: enter [1, 2, i]; change f_even i
  • "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
• Line 183: enter [2, 2, i]; change f_odd i
  • "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
• Line 189: enter [1]; rw [← Finset.sum_image (g := fun i => 2 * i) (by simp)]
  • "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
  • "Put spaces on both sides of :, :=, and infix operators." (Missing space before := in g :=).
  • "Functions: Prefer fun x ↦ ... over λ x, ...."
• Line 191: enter [2]; rw [← Finset.sum_image (g := fun i => 2 * i + 1) (by simp)]
  • "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
  • "Put spaces on both sides of :, :=, and infix operators." (Missing space before := in g :=).
  • "Functions: Prefer fun x ↦ ... over λ x, ...."
• Line 202: · rcases Finset.mem_image.mp h_even with ⟨k₁, hk₁, rfl⟩; simp at hk₁; omega
  • "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
• Line 203: · rcases Finset.mem_image.mp h_odd with ⟨k₂, hk₂, rfl⟩; simp at hk₂; omega
  • "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
• Line 206: · left; simp only [evens, Finset.mem_image, Finset.mem_range]; use k; omega
  • "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
• Line 207: · right; simp only [odds, Finset.mem_image, Finset.mem_range]; use k; omega
  • "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
• Line 211: /-- Specialized form of Fin.sum_univ_even_odd for r = 2^n. -/
  • "Use LaTeX for math: $ f(x) = y $." (for r = 2^n)

---

📄 **Per-File Summaries**

• CompPoly/Data/Fin/BigOperators.lean: Generalizes the Fin.sum_univ_odd_even theorem by introducing Fin.sum_univ_even_odd, which splits a sum over any range of size 2 * r into even and odd indices. The change refactors the original power-of-two version as a specialized case of this new theorem and streamlines the proofs using more concise tactics. No sorry or admit placeholders were added.

---

Last updated: 2026-04-01 23:49 UTC.