BigOperators for Multiset?

Stream: new members

[Kevin Cheung]

It doesn't seem like the notation ∑ x in s, f x is available when s is a Multiset. Can one expect this to be added in the near future?

[Ruben Van de Velde]

I don't expect it

[Bernardo Borges]

Is there a fundamental limitation on how bigoperators work for that to be the case?

[Alex J. Best]

There is no limitation, most frontend things of this sort that you could imagine are almost surely possible in Lean with a bit of work. Its only that getting these things right (writing custom elaborators and delaborators) takes some skills and many users tend not to make this sort of customization so the rate of additions of this nature is lower.

[Kevin Cheung]

So if I really need that kind of feature, I can try doing it myself and perhaps making a pull request once it's sufficiently polished?

[Yaël Dillies]

Yeah sure. My two cents is that it will be moderately hard to get the notation to work without breaking the existing uses.

[Yaël Dillies]

I should however ask: Why do you need to consider sums indexed by a multiset? This is a bit pathological

[Kevin Cheung]

I am trying to formalize some results in combinatorial designs. There, the blocks form a multiset. A lot of the arguments make use of sums over multisets.

[Yaël Dillies]

Are they sums of a multiset or indexed by a multiset?

[Kevin Cheung]

The proof I was looking at does require a sum indexed by elements of the blocks (a multiset).

[Yaël Dillies]

So ∑ x ∈ s, f x does not do what you want You edited your message

[Yaël Dillies]

Mind showing the proof?

[Kevin Cheung]

Screenshot-2024-05-25-at-4.45.46AM.png
From Combinatorial Designs by Doug Stinson.

[Kevin Cheung]

It doesn't explicitly use such sums. But my attempt at formalizing the argument leads to such sums.

[Kevin Cheung]

In any case, I am kind of stuck because I need the equivalent of Finset.sum_comm for Multiset. But that doesn't seem to exist.

[Yaël Dillies]

Are you aware of file#Combinatorics/Enumerative/DoubleCounting ?

[Yaël Dillies]

Kevin Cheung said:

Screenshot-2024-05-25-at-4.45.46AM.png
From Combinatorial Designs by Doug Stinson.

And do you have a Lean statement I can look at?

[Kevin Cheung]

This is a very preliminary version:

import Mathlib.Data.Finset.Basic
import Mathlib.Tactic.linarith
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Algebra.BigOperators.Fin

structure Design {α : Type*} [DecidableEq α] where
  points : Finset α
  blocks : Multiset { x // x ⊆ points }

structure BIBD {α : Type*} [DecidableEq α] (v k lambda: ℕ) extends @Design α _ where
  incomplete : v > k
  nontrivial : k ≥ 2
  points_count : points.card = v
  block_size : ∀ x ∈ blocks, x.val.card = k
  balance : ∀ x y, x ≠ y → blocks.countP (fun b ↦ x ∈ b.val ∧ y ∈ b.val) = lambda

theorem thm_1_8 {α : Type*} [DecidableEq α] (d : @BIBD α _ v k lambda) :
  ∀ x ∈ d.points, (k - 1) * (d.blocks.countP (fun b ↦ x ∈ b.val)) = lambda * (v - 1) := sorry

I hope things are correct so far.

[Yaël Dillies]

Unrelated to the rest of the discussion, but surely you want structure Design (α : Type*) [DecidableEq α] where

[Kevin Cheung]

Yaël Dillies said:

Are you aware of file#Combinatorics/Enumerative/DoubleCounting ?

I'm not aware. Do you suggest to somehow formulate blocks as some sort of FinType instead of Multiset?

[Yaël Dillies]

Unclear to me so far, but I think you will suffer a lot with those multisets. The fundamental issue with multisets is that if you have a function f : α → β then you can't send two copies of the same element a : α in m : Multiset α to different elements in β

[Kevin Cheung]

I see.

[Kevin Cheung]

Perhaps I need to go the route of an incidence matrix of a BIBD.

[Kevin Cheung]

Hmm. Maybe I want to define blocks as a Finset of functions that map from a finite set to subsets of the points.

[Kevin Cheung]

Looks like using Multsets is going to be a dead end. I will need to talk to my design colleague and see what's the best way to go about this.

[Yaël Dillies]

Kevin Cheung said:

Hmm. Maybe I want to define blocks as a Finset of functions that map from a finite set to subsets of the points.

Yes, that's my first thought as well