Defining a function: size of lower contour.

Stream: new members

[Greg Leo]

I am trying to define a function that for any x in some finite A returns the size of the set of y in A such that R x y for some relation R. I know how to define some basic functions, and how to define some basic sets, but I can't seem to combine my knowledge to define this function.

[Patrick Johnson]

import tactic

def f {α : Type} (A : finset α) (x ∈ A) (R : α → α → Prop) [decidable_rel R] : ℕ :=
(A.filter (R x)).card

[Yaël Dillies]

import combinatorics.double_counting

def your_thing {α β : Type*} (r : α → β → Prop) (t : finset β) (a : α) [Π a, decidable (r a b)] :
  ℕ :=
(s.bipartite_above r a).card

[Greg Leo]

I'll need to read about a few things before I understand these. Having two different options should help me figure things out. Thank you!

[Yaël Dillies]

The two options are definitionally equal. The advantage of Patrick's is that it's rather transparent in what it does. The advantage of mine is that it directly plugs onto the theory of double-counting.

[Patrick Johnson]

They're not definitionally equal, not only because of the order of arguments, but also because they are actually different functions (your definition fixes the second argument of the relation, while mine fixes the first argument).

#reduce f {1, 2} 1 dec_trivial (<) -- 1
#reduce your_thing (<) {1, 2} 1    -- 0

"Function that for any x in some finite A returns the size of the set of y in A such that R x y for some relation R" sounds like x should be fixed.

[Greg Leo]

If I was programming it (in some made-up python-like language), I would have something like:

f = function(x){
  size = 0
  for (y in A){
    if(R x y){size = size  + 1}
  }
  return(size)
}

[Greg Leo]

So yeah, x is fixed, and I want to count up the y such that R x y. That is, how many y are there in A that are "worse than" x?

[Patrick Johnson]

Then my definition of f is what you need.

[Yaël Dillies]

Ah sorry, I meant docs#finset.bipartite_above