ValidSplit: combinatorial splits of 2m into two groups of m

A ValidSplit m is an assignment of each of 2m indices to one of two groups, with exactly m indices assigned to the first group. The type has cardinality Nat.choose (2 * m) m and comes equipped with Fintype and (discrete) MeasurableSpace instances.

structure ProbabilityTheory.ValidSplit (m : ℕ) : Type

A split of a 2m-element set into two groups of m.

• assign : Fin (2 * m) → Bool

  Assignment of each of 2 * m indices to one of two groups.

• card_true : {i : Fin (2 * m) | self.assign i = true}.card = m

  Exactly m indices are assigned to the first group.

def ProbabilityTheory.instDecidableEqValidSplit.decEq {m✝ : ℕ} (x✝ x✝¹ : ValidSplit m✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance ProbabilityTheory.instDecidableEqValidSplit {m✝ : ℕ} : DecidableEq (ValidSplit m✝)

Equations

• ProbabilityTheory.instDecidableEqValidSplit = ProbabilityTheory.instDecidableEqValidSplit.decEq

@[implicit_reducible]

noncomputable instance instFintypeValidSplit (m : ℕ) : Fintype (ProbabilityTheory.ValidSplit m)

ValidSplit m is finite: a subtype of the finite type Fin (2*m) → Bool.

Equations

• instFintypeValidSplit m = Fintype.ofInjective (fun (vs : ProbabilityTheory.ValidSplit m) => vs.assign) ⋯

@[implicit_reducible]

instance instMeasurableSpaceValidSplit (m : ℕ) : MeasurableSpace (ProbabilityTheory.ValidSplit m)

Discrete measurable space on ValidSplit m (all sets measurable).

Equations

• instMeasurableSpaceValidSplit m = ⊤