Documentation

Complexity.Crypto.Computational.Pseudoentropy.Boosting.Potential

The potential for hard-core boosting #

The signed margin of a collection of predictors is the number of correct votes minus the number of incorrect votes. For a positive rate and relative to a movable threshold, weight rate margin assigns full weight to nonpositive margins, decreases linearly with slope -rate, and vanishes at 1 / rate. potential rate margin is the area under this curve to the right of the margin.

The quadratic upper bound on a change of potential gives both the progress from adding a predictor and the cost of moving the threshold. These are scalar inequalities; no real-valued operation here is being asserted to have an efficient implementation.

Main definitions #

Main results #

References #

The potential argument of Holenstein, Section 2.2, Figure 1 and Claims 2.10–2.11. Our rate is the product γδ, and our margin is N_C(x) - s in that write-up. Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

source
def Cslib.Crypto.Pseudoentropy.Boosting.weight (rate margin : ℝ) :
ℝ

The clipped linear weight on an example's signed margin relative to the threshold.

Instances For
    source
    noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.potential (rate margin : ℝ) :
    ℝ

    The area to the right of the margin under the clipped linear weight curve.

    Instances For
      source
      theorem Cslib.Crypto.Pseudoentropy.Boosting.weight_mem_Icc (rate margin : ℝ) :
      weight rate margin ∈ Set.Icc 0 1

      Weights are probabilities.

      source
      theorem Cslib.Crypto.Pseudoentropy.Boosting.weight_antitone {rate : ℝ} (hrate : 0 ≤ rate) :
      Antitone (weight rate)

      Increasing a margin can only decrease its weight.

      source
      theorem Cslib.Crypto.Pseudoentropy.Boosting.weight_of_nonpos {rate margin : ℝ} (hrate : 0 ≤ rate) (hmargin : margin ≤ 0) :
      weight rate margin = 1

      An example at or below the threshold has full weight.

      source
      theorem Cslib.Crypto.Pseudoentropy.Boosting.potential_of_nonpos (rate : ℝ) {margin : ℝ} (hmargin : margin ≤ 0) :
      potential rate margin = 1 / (2 * rate) - margin

      Below the threshold, the potential has slope -1.

      source
      theorem Cslib.Crypto.Pseudoentropy.Boosting.potential_nonneg {rate : ℝ} (hrate : 0 < rate) (margin : ℝ) :
      0 ≤ potential rate margin

      The potential is nonnegative.

      source
      theorem Cslib.Crypto.Pseudoentropy.Boosting.potential_lower_bound {rate : ℝ} (hrate : 0 < rate) (margin : ℝ) :
      1 / (2 * rate) - margin ≤ potential rate margin

      The affine part of the potential is a global lower bound, including above the threshold.

      source
      theorem Cslib.Crypto.Pseudoentropy.Boosting.potential_le_quadratic {rate : ℝ} (hrate : 0 < rate) (x y : ℝ) :
      potential rate y ≤ potential rate x - weight rate x * (y - x) + rate * (y - x) ^ 2 / 2

      A quadratic remainder controls the change in potential at any margin.

      source
      theorem Cslib.Crypto.Pseudoentropy.Boosting.potential_add_one_le {rate : ℝ} (hrate : 0 < rate) (margin : ℝ) :
      potential rate (margin + 1) ≤ potential rate margin - weight rate margin + rate / 2

      A correct vote decreases the potential by its current weight, up to rate / 2.

      source
      theorem Cslib.Crypto.Pseudoentropy.Boosting.potential_sub_one_le {rate : ℝ} (hrate : 0 < rate) (margin : ℝ) :
      potential rate (margin - 1) ≤ potential rate margin + weight rate margin + rate / 2

      An incorrect vote, or a unit threshold increase, costs at most the weight plus rate / 2.

      source
      theorem Cslib.Crypto.Pseudoentropy.Boosting.potential_sub_one_of_nonpos (rate : ℝ) {margin : ℝ} (hmargin : margin ≤ 0) :
      potential rate (margin - 1) = potential rate margin + 1

      At a nonpositive margin a unit threshold increase costs exactly one, with no remainder.