Sufficient input subsets

DefinitionGreedy backward-selection rule#✓fully proved

pick is a greedy backward-selection rule for g: from a nonempty remaining set R it masks a feature i ∈ R maximizing g (R.erase i).

def IsGreedy (g : Finset ι → ℝ) (pick : (R : Finset ι) → R.Nonempty → R) : Prop :=
  ∀ (R : Finset ι) (h : R.Nonempty), ∀ i ∈ R, g (R.erase i) ≤ g (R.erase (pick R h))

Used by 3

Used byExistence of greedy backward-selection rules · Proposition 1 (first part) · Minimality of FindSIS for monotone set functions

TheoremExistence of greedy backward-selection rules#✓fully proved

Greedy rules exist for every g.

theorem exists_isGreedy (g : Finset ι → ℝ) :
    ∃ pick : (R : Finset ι) → R.Nonempty → R, IsGreedy g pick

Uses 1

Statement usesGreedy backward-selection rule

DefinitionBackward-selection chain of remaining feature sets#✓fully proved

Backward selection: the list of remaining sets R₀ = R, R₁, …, ∅, where R_{t+1} is R_t with the feature chosen by pick masked.

def chain (g : Finset ι → ℝ) (pick : (R : Finset ι) → R.Nonempty → R) (R : Finset ι) :
    List (Finset ι) :=
  if h : R.Nonempty then R :: chain g pick (R.erase (pick R h)) else [R]
termination_by R.card
decreasing_by exact card_erase_lt_of_mem (pick R h).2

Used by 9

Used byBackward-selection chain at a nonempty set · Backward-selection chain at the empty set · FindSIS procedure for sufficient input subsets · Proposition 1 (second part) · Proposition 1 (first part) · FindSIS returns a set when the start reaches the threshold · FindSIS returns a sufficient subset of the features · Starting set begins the backward-selection chain · Sets in the backward-selection chain are subsets of the start

DefinitionFindSIS procedure for sufficient input subsets#✓fully proved

FindSIS: un-mask features in reverse order of masking (start from ∅) and return the first set on which the prediction reaches the threshold, or none. The paper's procedure does not test ∅ itself; the two agree whenever g ∅ < τ, the case the paper considers.

noncomputable def findSIS (g : Finset ι → ℝ) (pick : (R : Finset ι) → R.Nonempty → R) (τ : ℝ)
    (R : Finset ι) : Option (Finset ι) :=
  (chain g pick R).reverse.find? fun S => decide (τ ≤ g S)

Uses 1 · Used by 9

Statement usesBackward-selection chain of remaining feature sets

Used byProposition 1 (second part) · Proposition 1 (first part) · FindSIS returns a set when the start reaches the threshold · Minimality of FindSIS for monotone set functions · FindSIS returns a sufficient subset of the features · SIS-collection procedure · Sets of the SIS-collection are pairwise disjoint · Proposition 2 · Sets of the SIS-collection are nonempty and sufficient

TheoremBackward-selection chain at a nonempty set#✓fully proved

Unfolding chain at a nonempty set.

theorem chain_of_nonempty (g : Finset ι → ℝ) (pick : (R : Finset ι) → R.Nonempty → R)
    {R : Finset ι} (h : R.Nonempty) :
    chain g pick R = R :: chain g pick (R.erase (pick R h))

Uses 1 · Used by 5

Statement usesBackward-selection chain of remaining feature sets

Used byProposition 1 (second part) · Proposition 1 (first part) · FindSIS returns a sufficient subset of the features · Starting set begins the backward-selection chain · Sets in the backward-selection chain are subsets of the start

TheoremBackward-selection chain at the empty set#✓fully proved

Unfolding chain at the empty set (the chain stops).

theorem chain_of_not_nonempty (g : Finset ι → ℝ) (pick : (R : Finset ι) → R.Nonempty → R)
    {R : Finset ι} (h : ¬R.Nonempty) : chain g pick R = [R]

Uses 1 · Used by 5

Statement usesBackward-selection chain of remaining feature sets

Used byProposition 1 (second part) · Proposition 1 (first part) · FindSIS returns a sufficient subset of the features · Starting set begins the backward-selection chain · Sets in the backward-selection chain are subsets of the start

TheoremSets in the backward-selection chain are subsets of the start#✓fully proved

Every set in the backward-selection chain is a subset of the starting set.

theorem subset_of_mem_chain {R S : Finset ι} (h : S ∈ chain g pick R) : S ⊆ R

Uses 3 · Used by 3

Statement usesBackward-selection chain of remaining feature sets

Proof usesBackward-selection chain at a nonempty set · Backward-selection chain at the empty set

Used byProposition 1 (second part) · Proposition 1 (first part) · FindSIS returns a sufficient subset of the features

TheoremStarting set begins the backward-selection chain#✓fully proved

The starting set is the first set of the chain.

theorem mem_chain_self (R : Finset ι) : R ∈ chain g pick R

Uses 3 · Used by 2

Statement usesBackward-selection chain of remaining feature sets

Proof usesBackward-selection chain at a nonempty set · Backward-selection chain at the empty set

Used byProposition 1 (first part) · FindSIS returns a set when the start reaches the threshold

TheoremFindSIS returns a set when the start reaches the threshold#✓fully proved

If the prediction on the starting set reaches the threshold, findSIS returns a set.

theorem findSIS_isSome {R : Finset ι} (hR : τ ≤ g R) : (findSIS g pick τ R).isSome

Uses 3 · Used by 1

Statement usesFindSIS procedure for sufficient input subsets

Proof usesBackward-selection chain of remaining feature sets · Starting set begins the backward-selection chain

Used byProposition 2

TheoremFindSIS returns a sufficient subset of the features#✓fully proved

Criterion (1): the returned SIS is a subset of the starting features and is sufficient.

theorem findSIS_sufficient {R S : Finset ι} (h : findSIS g pick τ R = some S) :
    S ⊆ R ∧ τ ≤ g S

Uses 5 · Used by 4

Statement usesFindSIS procedure for sufficient input subsets

Proof usesBackward-selection chain of remaining feature sets · Backward-selection chain at a nonempty set · Backward-selection chain at the empty set · Sets in the backward-selection chain are subsets of the start

Used bySIS-collection procedure · Sets of the SIS-collection are pairwise disjoint · Proposition 2 · Sets of the SIS-collection are nonempty and sufficient

TheoremProposition 1 (first part)#✓fully proved

Proposition 1 (first part) of Carter et al.: no feature of the returned SIS can be additionally masked while keeping the prediction at or above the threshold.

theorem findSIS_erase_lt (hpick : IsGreedy g pick) {R S : Finset ι}
    (h : findSIS g pick τ R = some S) : ∀ s ∈ S, g (S.erase s) < τ

Uses 7 · Used by 1

Statement usesGreedy backward-selection rule · FindSIS procedure for sufficient input subsets

Proof usesBackward-selection chain of remaining feature sets · Backward-selection chain at a nonempty set · Backward-selection chain at the empty set · Starting set begins the backward-selection chain · Sets in the backward-selection chain are subsets of the start

Used byMinimality of FindSIS for monotone set functions

TheoremProposition 1 (second part)#✓fully proved

Proposition 1 (second part) of Carter et al.: among the sets met during backward selection, the returned SIS has the smallest cardinality among the sufficient ones.

theorem findSIS_card_le {R S T : Finset ι} (h : findSIS g pick τ R = some S)
    (hT : T ∈ chain g pick R) (hTτ : τ ≤ g T) : S.card ≤ T.card

Uses 5

Statement usesBackward-selection chain of remaining feature sets · FindSIS procedure for sufficient input subsets

Proof usesBackward-selection chain at a nonempty set · Backward-selection chain at the empty set · Sets in the backward-selection chain are subsets of the start

TheoremMinimality of FindSIS for monotone set functions#✓fully proved

For a monotone set function (masking more features never raises the prediction), the returned SIS is inclusion-minimal: no proper subset is sufficient. (Derived; the paper states only Proposition 1.)

theorem findSIS_minimal_of_monotone (hpick : IsGreedy g pick) (hg : Monotone g)
    {R S : Finset ι} (h : findSIS g pick τ R = some S) {T : Finset ι} (hT : T ⊂ S) :
    g T < τ

Uses 3

Statement usesGreedy backward-selection rule · FindSIS procedure for sufficient input subsets

Proof usesProposition 1 (first part)

DefinitionSIS-collection procedure#✓fully proved

SIScollection: while the remaining features R are sufficient (τ ≤ g R), find a SIS among them, record it and mask it. Stops if findSIS returns an empty set (only possible when τ ≤ g ∅).

noncomputable def sisCollection (g : Finset ι → ℝ) (pick : (R : Finset ι) → R.Nonempty → R)
    (τ : ℝ) (R : Finset ι) : List (Finset ι) :=
  if τ ≤ g R then
    match hS : findSIS g pick τ R with
    | some S =>
        if hne : S.Nonempty then
          have _ : (R \ S).card < R.card :=
            card_lt_card (sdiff_ssubset (findSIS_sufficient hS).1 hne)
          S :: sisCollection g pick τ (R \ S)
        else []
    | none => []
  else []
termination_by R.card
decreasing_by assumption

Uses 2 · Used by 3

Statement usesFindSIS procedure for sufficient input subsets · FindSIS returns a sufficient subset of the features

Used bySets of the SIS-collection are pairwise disjoint · Proposition 2 · Sets of the SIS-collection are nonempty and sufficient

TheoremSets of the SIS-collection are nonempty and sufficient#✓fully proved

Every set of the SIS-collection is a nonempty sufficient subset of the starting features.

theorem sisCollection_sufficient {R S : Finset ι} (h : S ∈ sisCollection g pick τ R) :
    S.Nonempty ∧ S ⊆ R ∧ τ ≤ g S

Uses 3 · Used by 1

Statement usesSIS-collection procedure

Proof usesFindSIS procedure for sufficient input subsets · FindSIS returns a sufficient subset of the features

Used bySets of the SIS-collection are pairwise disjoint

TheoremSets of the SIS-collection are pairwise disjoint#✓fully proved

The sets of the SIS-collection are pairwise disjoint.

theorem sisCollection_pairwiseDisjoint (R : Finset ι) :
    (sisCollection g pick τ R).Pairwise Disjoint

Uses 4

Statement usesSIS-collection procedure

Proof usesFindSIS procedure for sufficient input subsets · FindSIS returns a sufficient subset of the features · Sets of the SIS-collection are nonempty and sufficient

TheoremProposition 2#✓fully proved

Proposition 2 of Carter et al.: if the fully masked input is below the threshold, masking every set of the SIS-collection leaves the prediction below the threshold.

theorem sisCollection_remaining_lt (hempty : g ∅ < τ) (R : Finset ι) :
    g (R \ (sisCollection g pick τ R).foldr (fun A B => A ∪ B) ∅) < τ

Uses 4

Statement usesSIS-collection procedure

Proof usesFindSIS procedure for sufficient input subsets · FindSIS returns a set when the start reaches the threshold · FindSIS returns a sufficient subset of the features

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.