Clipped randomized prediction from votes

The predictor returns true with probability clippedProbability slope (listVoteMargin votes true). Its implementation uses a natural numerator and an exact dyadic coin. The label is needed only by the correctness statement, not by the predictor.

The lower-tail argument turns a positive margin on every dense soft set into a prediction advantage. Its cutoff is only an analysis witness. Approximating its reciprocal by a finite grid gives an efficiently representable candidate; empirical selection is a separate program.

Main definitions

• clippedProbability, clippedError: the clipped affine law and its average error.
• clippedPredict: exact fair-bit prediction from a public vote list.

Main results

• eval_clippedPredict_correct, isPPTOn_clippedPredict: semantics and strict PPT certificate.
• exists_dyadic_clippedError_le: a finite slope grid contains a good dense-margin predictor.

References

[Hol05], Lemma 2.4 and Claim 2.15. Fractional lower tails handle arbitrary finite sources, and a finite slope grid permits exact fair-bit sampling. Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.clippedProbability (slope margin : ℝ) : ℝ

The clipped affine probability associated with a signed margin.

theorem Cslib.Crypto.Pseudoentropy.Boosting.clippedProbability_mem_Icc (slope margin : ℝ) : clippedProbability slope margin ∈ Set.Icc 0 1

Clipping always gives a probability, including for arbitrary parameter values.

theorem Cslib.Crypto.Pseudoentropy.Boosting.clippedProbability_eq_one {slope margin : ℝ} (h : 1 ≤ slope * margin) : clippedProbability slope margin = 1

A margin at the positive clipping threshold is predicted with certainty.

theorem Cslib.Crypto.Pseudoentropy.Boosting.le_clippedProbability {slope margin : ℝ} (h : slope * margin ≤ 1) : (1 + slope * margin) / 2 ≤ clippedProbability slope margin

Below the positive threshold, clipping can only increase the affine probability.

theorem Cslib.Crypto.Pseudoentropy.Boosting.clippedProbability_eq_zero {slope margin : ℝ} (h : slope * margin ≤ -1) : clippedProbability slope margin = 0

A margin at the negative clipping threshold is predicted incorrectly with certainty.

@[simp]

theorem Cslib.Crypto.Pseudoentropy.Boosting.clippedProbability_neg (slope margin : ℝ) : clippedProbability slope (-margin) = 1 - clippedProbability slope margin

Negating the signed margin complements the probability.

theorem Cslib.Crypto.Pseudoentropy.Boosting.clippedProbability_lipschitz (slope slope' margin : ℝ) : |clippedProbability slope margin - clippedProbability slope' margin| ≤ |slope - slope'| * |margin| / 2

Rounding the slope loses at most half the margin times the rounding error.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.clippedPredict (bound numerator : ℕ) (votes : List Bool) : ProbComp Bool

Predict from the observable vote word with slope numerator / dyadicSize bound. The larger dyadic range supplies the additional fair bit needed for the factor 1 / 2.

theorem Cslib.Crypto.Pseudoentropy.Boosting.eval_clippedPredict_true (bound numerator : ℕ) (votes : List Bool) : ((clippedPredict bound numerator votes).eval true).toReal = clippedProbability (↑numerator / ↑(Probability.dyadicSize bound)) (BitString.listVoteMargin votes true)

The executable predictor realizes the clipped affine probability exactly.

theorem Cslib.Crypto.Pseudoentropy.Boosting.eval_clippedPredict_correct (bound numerator : ℕ) (votes : List Bool) (truth : Bool) : ((clippedPredict bound numerator votes).eval truth).toReal = clippedProbability (↑numerator / ↑(Probability.dyadicSize bound)) (BitString.listVoteMargin votes truth)

Correctness is expressed using the signed margin for either label; the label is not an input.

theorem Cslib.Crypto.Pseudoentropy.Boosting.eval_clippedPredict_wrong (bound numerator : ℕ) (votes : List Bool) (truth : Bool) : ((clippedPredict bound numerator votes).eval !truth).toReal = 1 - clippedProbability (↑numerator / ↑(Probability.dyadicSize bound)) (BitString.listVoteMargin votes truth)

The opposite label has the complementary clipped probability.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_clippedPredict {α : Type} {input : α ↪ List Bool} {bound numerator : α → ℕ} {votes : α → List Bool} (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hnumerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime numerator input Turing.MultiTapeTM.encUnary) (hvotes : Turing.MultiTapeTM.ComputableTidilyInPolyTime votes input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => clippedPredict (bound a) (numerator a) (votes a)

Efficient parameters and votes give a strict PPT predictor through ordinary combinators.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.clippedError {α : Type u_1} [Fintype α] (source : PMF α) (margin : α → ℝ) (slope : ℝ) : ℝ

The average error of clipped prediction on a finite source with signed margins.

theorem Cslib.Crypto.Pseudoentropy.Boosting.clippedError_eq_error {α : Type u_1} [Fintype α] (source : PMF α) (votes : α → List Bool) (truth : α → Bool) (bound numerator : ℕ) : clippedError source (fun (x : α) => BitString.listVoteMargin (votes x) (truth x)) (↑numerator / ↑(Probability.dyadicSize bound)) = ∑ x : α, (source x).toReal * ((clippedPredict bound numerator (votes x)).eval !truth x).toReal

The abstract error is exactly the source-averaged error of the executable dyadic predictor.

theorem Cslib.Crypto.Pseudoentropy.Boosting.clippedError_perturbation {α : Type u_1} [Fintype α] (source : PMF α) (margin : α → ℝ) {bound : ℝ} (hmargin : ∀ (x : α), |margin x| ≤ bound) (slope slope' : ℝ) : clippedError source margin slope ≤ clippedError source margin slope' + |slope - slope'| * bound / 2

A uniform bound on the margins controls the error caused by rounding the slope.

theorem Cslib.Crypto.Pseudoentropy.Boosting.exists_clippedError_le {α : Type u_1} [Fintype α] (source : PMF α) (margin : α → ℝ) {δ gap bound : ℝ} (hδ : 0 < δ) (hδone : δ ≤ 1) (hgap : 0 < gap) (hmargin : ∀ (x : α), margin x ≤ bound) (hdense : ∀ (softSet : α → ℝ), (∀ (x : α), softSet x ∈ Set.Icc 0 1) → δ ≤ ∑ x : α, (source x).toReal * softSet x → (∑ x : α, (source x).toReal * softSet x) * gap ≤ ∑ x : α, (source x).toReal * (softSet x * margin x)) : ∃ (cutoff : ℝ), gap ≤ cutoff ∧ cutoff ≤ bound ∧ clippedError source margin (1 / cutoff) ≤ δ / 2 - δ * gap / (2 * bound)

Positive average margin on every dense soft set gives a clipped predictor beating δ / 2. The cutoff is an analysis witness; this theorem does not supply it as computational advice.

theorem Cslib.Crypto.Pseudoentropy.Boosting.exists_dyadic_clippedError_le {α : Type u_1} [Fintype α] (source : PMF α) (margin : α → ℝ) (precision : ℕ) {δ gap bound : ℝ} (hδ : 0 < δ) (hδone : δ ≤ 1) (hgap : 1 ≤ gap) (hmargin : ∀ (x : α), |margin x| ≤ bound) (hdense : ∀ (softSet : α → ℝ), (∀ (x : α), softSet x ∈ Set.Icc 0 1) → δ ≤ ∑ x : α, (source x).toReal * softSet x → (∑ x : α, (source x).toReal * softSet x) * gap ≤ ∑ x : α, (source x).toReal * (softSet x * margin x)) : ∃ numerator ≤ Probability.dyadicSize precision, clippedError source margin (↑numerator / ↑(Probability.dyadicSize precision)) ≤ δ / 2 - δ * gap / (2 * bound) + bound / (2 * ↑(Probability.dyadicSize precision))

A finite dyadic grid contains a predictor with the lower-tail bound, up to explicit rounding loss. This is an existence guarantee for subsequent empirical selection, not a choice of advice.