group sum/prod in pairs even and odd summands

Stream: Is there code for X?

[Moritz Firsching]

If I have a sum/prod over an even range or Ioc or Icc, is there some function to group it by pairs, each containing an odd an an evenly indexed summand/factor.

-- TODO: find good place and name and prove additive/multiplicative version in generality
theorem prod_even_odd (n : ℕ) (f : ℕ → ℕ) :
    ∏ x in Icc 1 (2 * n), f x =  ∏ x in Icc 1 (n), (f (2 * x)) * (f (2 * x - 1)) := by
  induction' n with n hn
  · rfl
  · have h : 2 * succ n = succ (succ (2 * n)) := by rfl
    rw [h, ← Ico_succ_right, prod_Ico_succ_top <| le_add_left 1 (2 * n + 1),
        prod_Ico_succ_top <| le_add_left 1 (2 * n)]
    simp only [← Ico_succ_right, h] at hn
    rw [hn, ← Ico_succ_right, prod_Ico_succ_top <| le_add_left 1 n, succ_eq_add_one, mul_add,
        mul_one, mul_comm (f (2 * n + 2)), mul_assoc]
    rfl

Is there already some theorem like that, I searched but couldn't find it? I think it could be useful in general, but maybe there is an even better generalization that is already there and I am not seeing.

[Yaël Dillies]

This is morally docs#Finset.prod_product, but we're missing some glue.

[Moritz Firsching]

Thanks @Yaël Dillies, I see why this is related.
I tried deducing the result from docs#Finset.prod_product, but it turned out to be quite cumbersome, especially because of the use of docs#Finset.prod_bij' afterwards.
What is the glue that we missing precisely (I'm happy to produce it!). Do you have some canonical way in mind to write Icc 1 (2 * n) as a cartesian product?

theorem prod_even_odd (n : ℕ) (f : ℕ → ℕ) :
    ∏ x in Icc 1 (2 * n), f x =  ∏ x in Icc 1 (n), (f (2 * x)) * (f (2 * x - 1)) := by
  set i : ℕ × ℕ → ℕ := fun a => 2 * a.1 - a.2
  set g : ℕ × ℕ → ℕ := fun a => f (i a)
  have := @Finset.prod_product _ _ _ _ ((Icc 1 n)) ({0, 1}) g
  convert this
  · refine' prod_bij' _ _ _ _ _ _ _
    · intro a ha
      exact ⟨1 + (a - 1) / 2, a % 2⟩
    · intros a ha
      simp only [mem_singleton, mem_product, mem_Icc, mem_insert]
      constructor
      · simp at ha
        constructor
        · exact le_add_right 1 ((a - 1) / 2)
        · have := ha.2
          by_cases Even a
          · sorry
          · sorry
      · exact mod_two_eq_zero_or_one a
    · intros a ha
      simp only
      congr
      by_cases Even a
      · sorry
      · sorry
    · intro a ha
      exact i a
    · intro a ha
      simp only [mem_singleton, mem_product, mem_Icc, mem_insert] at ha
      cases' ha with ha_left ha_right
      simp only [_root_.mul_eq_zero, false_or, mem_Icc, tsub_le_iff_right]
      constructor
      · have : 2 ≤ 2 * a.1 := by simp [ha_left.1]
        by_cases a.2 = 1
        · rw [h]
          exact le_pred_of_lt this
        · have h : a.2 = 0 := by tauto
          rw [h]
          exact one_le_of_lt this
      · by_cases a.2 = 1
        have := ha_left.2
        · rw [h]
          linarith
        · have h : a.2 = 0 := by tauto
          rw [h]
          linarith
    · intro a ha
      dsimp only
      by_cases Even a
      · sorry
      · sorry
    · intro a ha
      dsimp only
      congr
      · sorry
      · sorry
  · simp

[Yaël Dillies]

Will have a look tomorrow morning, but does docs#finProdFinEquiv help?

[Moritz Firsching]

This is starting to make sense. I suppose one missing potentially useful theorem is prod_finProd as an analogue to docs#Finset.prod_product, what do you think?

@[to_additive]
theorem prod_finProd {n : ℕ} {m : ℕ} {f : Fin n × Fin m → ℕ} :
    ∏ x : Fin n × Fin m, f x = ∏ x : Fin n, ∏ y : Fin m, f (x, y) := by
  refine prod_finset_product univ univ (fun _ ↦ univ) ?h
  exact fun p => ⟨fun _ => ⟨mem_univ p.1, mem_univ p.2⟩, fun _ => mem_univ p⟩

theorem prod_even_odd (n : ℕ) (f : ℕ → ℕ) :
    ∏ x : Fin (n * 2), f x =  ∏ x : Fin n, (f (2 * x)) * (f (1 + 2 * x)) := by
  let g x := (f (2 * x)) * (f (1 + 2 * x))
  have : ∏ x : Fin n, f (2 * ↑x) * f (1 + 2 * ↑x ) = ∏ x : Fin n, g x := by rfl
  rw [this]
  have : ∏ x : Fin (n * 2), f ↑x =  ∏ y : (Fin n) × (Fin 2), f (finProdFinEquiv y) := by
    exact
      (Equiv.prod_comp' finProdFinEquiv (fun i ↦ f ↑(finProdFinEquiv i)) (fun i ↦ f ↑i)
          (congrFun rfl)).symm
  rw [this, prod_finProd]
  simp

[Moritz Firsching]

I suggest to add prod_finProd and friends here: #7955

[Yaël Dillies]

Uh, your prod_finProd is defeq to docs#Finset.prod_product.

[Moritz Firsching]

I see.
Is this

def  range_product_rangeEquiv {m n : ℕ} : (range m) ×ˢ (range n) ≃ range (m * n) where

also defeq to something in the library?

[Eric Wieser]

That should be very close to docs#finProdFinEquiv

[Moritz Firsching]

Thanks!
When using this, I made up two more lemmas:

def rangeFinEquiv {n : ℕ} : range n ≃ Fin n where
  toFun := fun x => ⟨x, List.mem_range.mp x.2⟩
  invFun := fun x => ⟨x.1, mem_range.mpr x.2⟩
  left_inv := congrFun rfl
  right_inv := congrFun rfl

def range_prod_rangeEquiv {m n : ℕ} : (range m) × (range n) ≃ range (m * n) :=
  Equiv.trans (Equiv.prodCongr rangeFinEquiv rangeFinEquiv)
  <| (finProdFinEquiv ).trans (rangeFinEquiv).symm

def range_sprod_rangeEquiv {m n : ℕ} : (range m) ×ˢ (range n) ≃ range (m * n) := by
  refine' Equiv.trans _ range_prod_rangeEquiv
  convert Equiv.subtypeProdEquivProd
  simp only [mem_product, mem_range]

I feel like rangeFinEquiv surely should be already there somewhere, but I couldn't find it. If not, should any of those be added to mathlib?

Even without those lemmas, I was able to change use docs#Finset.prod_product for a version of the statement that I actually need in #7924

theorem prod_even_odd (n : ℕ) (f : ℕ → ℕ) :
    ∏ x : Fin (n * 2), f x =  ∏ x : Fin n, (f (2 * x)) * (f (1 + 2 * x)) := by
  rw [(Equiv.prod_comp' finProdFinEquiv (fun i ↦ f ↑(finProdFinEquiv i)) (fun i ↦ f ↑i)
          (congrFun rfl)).symm, Fintype.prod_prod_type]
  simp only [finProdFinEquiv_apply_val]
  congr
  ext x
  rw [Fin.prod_univ_eq_prod_range (fun x_1 => f (↑x_1 + 2 * ↑x)) 2, Finset.prod_range_succ]
  simp

[Eric Wieser]

Can you make those mwes, with imports?

[Eric Wieser]

In particular, which range is that?

[Eric Wieser]

If it's Finset.range, then this works for the first one:

def rangeFinEquiv {n : ℕ} : Finset.range n ≃ Fin n :=
  (Equiv.subtypeEquivProp <| by simp).trans Fin.equivSubtype.symm

[Moritz Firsching]

sure, as mwe:

import Mathlib.Logic.Equiv.Fin
import Mathlib.Logic.Equiv.Basic
import Mathlib.Data.Fintype.BigOperators
import Mathlib.Algebra.BigOperators.Intervals

open Finset

def rangeFinEquiv {n : ℕ} : range n ≃ Fin n :=
  (Equiv.subtypeEquivProp <| by simp).trans Fin.equivSubtype.symm

def range_prod_rangeEquiv {m n : ℕ} : (range m) × (range n) ≃ range (m * n) :=
  Equiv.trans (Equiv.prodCongr rangeFinEquiv rangeFinEquiv)
  <| (finProdFinEquiv ).trans (rangeFinEquiv).symm

def range_sprod_rangeEquiv {m n : ℕ} : (range m) ×ˢ (range n) ≃ range (m * n) := by
  refine' Equiv.trans _ range_prod_rangeEquiv
  convert Equiv.subtypeProdEquivProd
  simp only [mem_product, mem_range]

open BigOperators Nat

theorem prod_even_odd (n : ℕ) (f : ℕ → ℕ) :
    ∏ x : Fin (n * 2), f x =  ∏ x : Fin n, (f (2 * x)) * (f (1 + 2 * x)) := by
  rw [(Equiv.prod_comp' finProdFinEquiv (fun i ↦ f ↑(finProdFinEquiv i)) (fun i ↦ f ↑i)
          (congrFun rfl)).symm, Fintype.prod_prod_type]
  simp only [finProdFinEquiv_apply_val]
  congr
  ext x
  rw [Fin.prod_univ_eq_prod_range (fun x_1 => f (↑x_1 + 2 * ↑x)) 2, Finset.prod_range_succ]
  simp