Documentation

Complexity.Foundations.Data.BitString.List.Vote

Signed margins of vote lists #

The signed margin is the number of correct votes minus the number of incorrect votes. A positive margin ensures that the existing strict-majority operation returns the supplied label, including a precise account of empty lists and ties.

Main definitions #

Main results #

References #

Holenstein, Claim 2.16. Adapted from Crypto/Computational/Pseudoentropy/Boosting/Vote.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing the shared strict-majority operation.

source
def Cslib.BitString.listVoteMargin (votes : List Bool) (truth : Bool) :
ℝ

Correct votes minus incorrect votes, represented as a real number for the analysis.

Instances For
    source
    def Cslib.BitString.signedVote (vote truth : Bool) :
    ℝ

    A correct prediction contributes one to the margin; an incorrect prediction subtracts one.

    Instances For
      source
      @[simp]
      theorem Cslib.BitString.abs_signedVote (vote truth : Bool) :
      |signedVote vote truth| = 1

      Each vote contributes ±1 to the margin: |signedVote vote truth| = 1.

      source
      @[simp]
      theorem Cslib.BitString.listVoteMargin_nil (truth : Bool) :
      listVoteMargin [] truth = 0

      The empty vote list has margin zero.

      source
      theorem Cslib.BitString.listVoteMargin_cons (vote : Bool) (votes : List Bool) (truth : Bool) :
      listVoteMargin (vote :: votes) truth = listVoteMargin votes truth + signedVote vote truth

      Adding a predictor updates the margin by its signed prediction.

      source
      theorem Cslib.BitString.listNonpositiveMargin_eq_true (votes : List Bool) (truth : Bool) :
      listNonpositiveMargin votes truth = true ↔ listVoteMargin votes truth ≤ 0

      The training test agrees exactly with the real margin event used by the potential proof.

      source
      @[simp]
      theorem Cslib.BitString.listVoteMargin_not (votes : List Bool) (truth : Bool) :
      (listVoteMargin votes !truth) = -listVoteMargin votes truth

      Reversing the label negates the signed margin of the same observable vote word.

      source
      theorem Cslib.BitString.abs_listVoteMargin_le (votes : List Bool) (truth : Bool) :
      |listVoteMargin votes truth| ≤ ↑votes.length

      The magnitude of the signed margin is at most the number of votes.

      source
      theorem Cslib.BitString.listStrictMajority_eq_of_pos {votes : List Bool} {truth : Bool} (hmargin : 0 < listVoteMargin votes truth) :
      listStrictMajority votes = truth

      A positive signed margin guarantees that the executable majority predicts the label.