Product of i < j and j < i

Stream: Is there code for X?

[Riccardo Brasca]

This was nonsense.
Does someone see a quick way of proving the following?

[Alex J. Best]

Is this true as stated? Why can't the set of i larger than a be empty say and the other one not be?

[Riccardo Brasca]

Because I am stupid.

[Riccardo Brasca]

Time for coffee

[Riccardo Brasca]

Ok, the real question is

import data.fin.interval

open_locale big_operators

example {R : Type*} [comm_ring R] {n : ℕ} (f : fin n → R) :
  ∏ i, (∏ j in finset.univ.filter (λ j, j < i), (f j - f i) * (f i - f j)) =
  ∏ i, (∏ j in finset.univ.filter (λ j, i ≠ j), (f j - f i)) := sorry

I am not asking to do my work, but suggestions are welcome :)

[Eric Wieser]

I think the RHS is ∏ i in (finset.univ : finset ℕ).off_diag, f i.2 - f i.1?

[Yaël Dillies]

You can move multiplication out of the LHS, swap the products on the right factor, then split the prod on the RHS as the i < j and j < i bits.

[Eric Wieser]

Do we have something like docs#finset.filter_or

[Riccardo Brasca]

It's the "swap the product" part that is causing me troubles.

[Riccardo Brasca]

Ah, docs#finset.filter_or seems relevant

[Eric Wieser]

Yeah, simp_rw [ne_iff_lt_or_gt, finset.filter_or], is a good start

[Yaël Dillies]

You might need to turn the double sum in a single one using docs#finset.product and docs#finset.prod_product.

[Yaël Dillies]

And once again Eric, finset.prod_product_right would come in handy!

[Eric Wieser]

Well, no more handy than rw [prod_product, prod_comm]

[Eric Wieser]

This gets through some of the pain:

example {R : Type*} [comm_ring R] {n : ℕ} (f : fin n → R) :
  ∏ i, (∏ j in finset.univ.filter (λ j, j < i), (f j - f i) * (f i - f j)) =
  ∏ i, (∏ j in finset.univ.filter (λ j, i ≠ j), (f j - f i)) :=
begin
  simp_rw [ne_iff_lt_or_gt, finset.filter_or],
  refine eq.trans _ (congr_arg (finset.prod _) (funext $ λ i, (finset.prod_union _).symm)),
  simp_rw [finset.prod_mul_distrib],
  sorry,
  { rintro x hx,
    obtain ⟨⟨_, hl⟩, ⟨_, hg⟩⟩ := (finset.mem_inter.1 hx).imp finset.mem_filter.1 finset.mem_filter.1,
    exact (lt_asymm hl hg).elim, },
end

[Riccardo Brasca]

example {R : Type*} [comm_ring R] {n : ℕ} (f : fin n → R) :
  ∏ i, (∏ j in finset.univ.filter (λ j, j < i), (f j - f i) * (f i - f j)) =
  ∏ i, (∏ j in finset.univ.filter (λ j, i ≠ j), (f j - f i)) :=
begin
  simp_rw [ne_iff_lt_or_gt, finset.filter_or],
  refine eq.trans _ (congr_arg (finset.prod _) (funext $ λ i, (finset.prod_union _).symm)),
  simp_rw [finset.prod_mul_distrib],
  { conv_rhs {
      congr, skip, congr, skip, funext,
      conv {
        congr, skip, funext,
        rw [← neg_sub, neg_eq_neg_one_mul] },
        rw [finset.prod_mul_distrib, finset.prod_const], },
    simp_rw [finset.prod_mul_distrib],
    rw [← mul_assoc],
    congr,
    sorry,
  },
  { rintro x hx,
    obtain ⟨⟨_, hl⟩, ⟨_, hg⟩⟩ := (finset.mem_inter.1 hx).imp finset.mem_filter.1 finset.mem_filter.1,
    exact (lt_asymm hl hg).elim, },
end

Takes care of one half of the product, the easy part...

[Riccardo Brasca]

And let's simp for the win.

lemma prod_filter_lt_mul_neg_eq_prod_off_diag {R : Type*} [comm_ring R] {n : ℕ} (f : fin n → R) :
  ∏ i, (∏ j in finset.univ.filter (λ j, j < i), (f j - f i) * (f i - f j)) =
  ∏ i, (∏ j in finset.univ.filter (λ j, i ≠ j), (f j - f i)) :=
begin
  simp_rw [ne_iff_lt_or_gt, finset.filter_or],
  refine eq.trans _ (congr_arg (finset.prod _) (funext $ λ i, (finset.prod_union _).symm)),
  simp_rw [finset.prod_mul_distrib],
  { conv_rhs {
      congr, skip, congr, skip, funext,
      conv {
        congr, skip, funext,
        rw [← neg_sub, neg_eq_neg_one_mul] },
      rw [finset.prod_mul_distrib, finset.prod_const] },
    simp_rw [finset.prod_mul_distrib],
    rw [← mul_assoc],
    congr,
    conv_lhs {
      congr, skip, funext,
      conv {
        congr, skip, funext,
        rw [← neg_sub, neg_eq_neg_one_mul] },
      rw [finset.prod_mul_distrib, finset.prod_const] },
    simp_rw [finset.prod_mul_distrib, filter_gt_card],
    nth_rewrite 0 [mul_comm],
    congr' 1,
    rw [finset.prod_sigma', finset.prod_sigma'],
    exact finset.prod_bij' (λ i hi, ⟨i.2, i.1⟩) (by simp) (by simp) (λ i hi, ⟨i.2, i.1⟩)
      (by simp) (by simp) (by simp) },
  { rintro x hx,
    obtain ⟨⟨_, hl⟩, ⟨_, hg⟩⟩ := (finset.mem_inter.1 hx).imp finset.mem_filter.1 finset.mem_filter.1,
    exact (lt_asymm hl hg).elim, },
end

[Eric Wieser]

Does this lemma generalize to g i j = f i - f j?

[Floris van Doorn]

Probably, as long as g i j = - g j i.

[Floris van Doorn]

Oh, or maybe that condition is not even needed

[Floris van Doorn]

It can probably be further generalized by replacing ...
edit: nevermind

[Riccardo Brasca]

Yes, it should be generalized and golfed