Cardinality of a finite set

Stream: new members

[Park Sanghyeok]

import MIL.Common
import Mathlib.Data.Set.Basic

open Set

-- Shatter coefficient Fail
def shatter_coefficient_Fail (Λ : Set (Set (Fin d → ℝ)))[MeasurableSpace Λ] (S :Finset (Fin d → ℝ)) : ℕ :=
  Finset.card {(↑S) ∩ H | H ∈ Λ}

-- Shatter coefficient Correction 1
noncomputable def shatter_coefficient0 (Λ : Set (Set (Fin d → ℝ)))[MeasurableSpace Λ] (S :Finset (Fin d → ℝ)) : ℕ :=
  Nat.card {(↑S) ∩ H | H ∈ Λ}

-- Shatter coefficient Correction 2
def Finset_intersection (S : Finset α) (H : Set α) [DecidablePred (fun x ↦ x ∈ H)]: Finset α :=
  S.filter (fun x ↦ x ∈ H)

def shatter_coefficient (Λ : Set (Set (Fin d → ℝ)))[MeasurableSpace Λ] (S :Finset (Fin d → ℝ)) [∀ H ∈ Λ, DecidablePred (fun x ↦ x ∈ H)]: ℕ :=
  {Finset_intersection S H | H ∈ Λ}.card

I tried to define the shatter coefficient as above.
First, shatter_coefficient_Fail fails because (↑S) ∩ H is not Finset.

In correction 1, there is no error.
I use Nat.card instead of Finset.card.
However, I also had to use 'noncomputable' which is awkward for the definition of shatter coefficient.

In correction 2, I define Finset_intersection to make the intersection of S and H to be finite.
However there's an error at [∀ H ∈ Λ, DecidablePred (fun x ↦ x ∈ H)] which I cannot solve.

[Bbbbbbbbba]

I guess changing it to (h : ∀ H ∈ Λ, DecidablePred (fun x ↦ x ∈ H)) is a first step

[Bbbbbbbbba]

I got as far as this, but the problem now is that {Finset_intersection S H (h H h0) | (H : _) (h0: H ∈ Λ)} is still not a Finset --- it's a Set of Finset:

def Finset_intersection (S : Finset α) (H : Set α) (_ : DecidablePred (fun x ↦ x ∈ H)): Finset α :=
  S.filter (fun x ↦ x ∈ H)

def shatter_coefficient (Λ : Set (Set (Fin d → ℝ)))[MeasurableSpace Λ] (S : Finset (Fin d → ℝ)) (h : ∀ H ∈ Λ, DecidablePred (fun x ↦ x ∈ H)): ℕ :=
  {Finset_intersection S H (h H h0) | (H : _) (h0: H ∈ Λ)}.card

[Ruben Van de Velde]

Yes, { ... | ... } syntax always creates a Set right now

[Bbbbbbbbba]

I think what you want might be this:

def shatter_coefficient (Λ : Set (Set (Fin d → ℝ))) [MeasurableSpace Λ] (S : Finset (Fin d → ℝ)) (_ : DecidablePred (fun x ↦ ∃H ∈ Λ, x = (↑S) ∩ H)) : ℕ :=
  Finset.card (S.powerset.filter (fun (x : Finset (Fin d → ℝ)) ↦ ∃H ∈ Λ, x = (↑S) ∩ H))

[Bbbbbbbbba]

(_ : DecidablePred (fun x ↦ ∃H ∈ Λ, x = (↑S) ∩ H)) might be hard to satisfy, but if you think about it, that is what it takes to compute the cardinality

[Yaël Dillies]

May I advertise #11582 which makes {x | p x} notation (and similar) available on Finset?

[Bbbbbbbbba]

Yaël Dillies said:

May I advertise #11582 which makes {x | p x} notation (and similar) available on Finset?

What happens if DecidablePred p isn't available?

[Yaël Dillies]

Then it complains that DecidablePred p isn't available

[Bbbbbbbbba]

So if the user just wants a Set they need to use {x ∈ (s : Set) | p x}?

[Yaël Dillies]

No, it depends on the expected types. Please read the PR description for the full explanation.