Progress of hard-core boosting

We average the scalar potential inequalities over a finite source. A predictor with weighted correlation at least γ decreases the average potential by γδ / 2 when the weight density is at least δ. Moving the threshold costs slightly less than δ + γδ / 2 under the loop guards. Together these give progress of at least γδ² / 8 per iteration after charging for the shift.

The statements allow any finite source distribution. The write-up uses a uniform source. Margins and votes are real-valued in this analysis; integer vote counts and their efficient representation are separate implementation obligations.

Main definitions

• Cslib.Crypto.Pseudoentropy.Boosting.density: source-averaged soft weight.
• Cslib.Crypto.Pseudoentropy.Boosting.averagePotential: source-averaged scalar potential.

Main results

• Cslib.Crypto.Pseudoentropy.Boosting.step_progress: amortized progress of one valid round.
• Cslib.Crypto.Pseudoentropy.Boosting.dense_margin_of_iterations: a dense-set guarantee at the finite clock boundary, including equality.
• Cslib.Crypto.Pseudoentropy.Boosting.clock_sufficient: a polynomial clock from inverse bounds.

References

The hard-core boosting argument of Holenstein, Section 2.2, Figure 2, Claims 2.7 and 2.10–2.13, and Lemma 2.14. Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, with arbitrary finite sources and soft dense sets.

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

The total mass of the soft weights under the source distribution.

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

The expected potential of an example drawn from the source.

theorem Cslib.Crypto.Pseudoentropy.Boosting.density_mem_Icc {α : Type u_1} [Fintype α] (source : PMF α) (rate : ℝ) (margin : α → ℝ) : density source rate margin ∈ Set.Icc 0 1

Soft weights have density between zero and one.

theorem Cslib.Crypto.Pseudoentropy.Boosting.density_antitone {α : Type u_1} [Fintype α] (source : PMF α) {rate : ℝ} (hrate : 0 ≤ rate) {margin margin' : α → ℝ} (hmargin : ∀ (x : α), margin' x ≤ margin x) : density source rate margin ≤ density source rate margin'

Decreasing every margin cannot decrease the density.

theorem Cslib.Crypto.Pseudoentropy.Boosting.density_vote_shift_ge {α : Type u_1} [Fintype α] (source : PMF α) {rate : ℝ} (hrate : 0 ≤ rate) (margin step : α → ℝ) (hstep : ∀ (x : α), step x ≤ 1) : density source rate margin ≤ density source rate fun (x : α) => margin x + step x - 1

Increasing the threshold restores the density present before the preceding vote. Together with the no-shift guard, this proves the density invariant of Claim 2.7.

@[simp]

theorem Cslib.Crypto.Pseudoentropy.Boosting.density_zero {α : Type u_1} [Fintype α] (source : PMF α) (rate : ℝ) : (density source rate fun (x : α) => 0) = 1

Before any votes, all examples have full weight.

@[simp]

theorem Cslib.Crypto.Pseudoentropy.Boosting.averagePotential_zero {α : Type u_1} [Fintype α] (source : PMF α) (rate : ℝ) : (averagePotential source rate fun (x : α) => 0) = 1 / (2 * rate)

The initial average potential is the area of the triangular weight curve.

theorem Cslib.Crypto.Pseudoentropy.Boosting.averagePotential_add_le {α : Type u_1} [Fintype α] (source : PMF α) {rate : ℝ} (hrate : 0 < rate) (margin step : α → ℝ) (hstep : ∀ (x : α), |step x| ≤ 1) : (averagePotential source rate fun (x : α) => margin x + step x) ≤ averagePotential source rate margin - ∑ x : α, (source x).toReal * (weight rate (margin x) * step x) + rate / 2

Bounded signed votes cost at most their negative weighted correlation plus rate / 2.

theorem Cslib.Crypto.Pseudoentropy.Boosting.add_predictor_progress {α : Type u_1} [Fintype α] (source : PMF α) {γ δ : ℝ} (hγ : 0 < γ) (hδ : 0 < δ) (margin step : α → ℝ) (hstep : ∀ (x : α), |step x| ≤ 1) (hdensity : δ ≤ density source (γ * δ) margin) (hcorrelation : γ * density source (γ * δ) margin ≤ ∑ x : α, (source x).toReal * (weight (γ * δ) (margin x) * step x)) : (averagePotential source (γ * δ) fun (x : α) => margin x + step x) ≤ averagePotential source (γ * δ) margin - γ * δ / 2

A predictor with correlation γ on a δ-dense measure gives the decrease in Claim 2.10. The correlation hypothesis is unnormalized, so it remains meaningful without division by density.

theorem Cslib.Crypto.Pseudoentropy.Boosting.averagePotential_shift_le {α : Type u_1} [Fintype α] (source : PMF α) {rate : ℝ} (hrate : 0 < rate) (margin : α → ℝ) : (averagePotential source rate fun (x : α) => margin x - 1) ≤ averagePotential source rate margin + density source rate margin + (1 - (source.toOuterMeasure {x : α | margin x ≤ 0}).toReal) * rate / 2

Moving the threshold by one has no quadratic cost on examples already below it.

theorem Cslib.Crypto.Pseudoentropy.Boosting.shift_progress {α : Type u_1} [Fintype α] (source : PMF α) {γ δ : ℝ} (hγ : 0 < γ) (hδ : 0 < δ) (margin : α → ℝ) (hguard : density source (γ * δ) margin ≤ δ * (1 + γ * δ / 16)) (hbelow : 3 * δ / 8 ≤ (source.toOuterMeasure {x : α | margin x ≤ 0}).toReal) : (averagePotential source (γ * δ) fun (x : α) => margin x - 1) ≤ averagePotential source (γ * δ) margin + δ + γ * δ / 2 - γ * δ ^ 2 / 8

The threshold guard and the failure of the stopping test give the cost in Claim 2.11.

theorem Cslib.Crypto.Pseudoentropy.Boosting.step_progress {α : Type u_1} [Fintype α] (source : PMF α) {γ δ : ℝ} (hγ : 0 < γ) (hδ : 0 < δ) (hδone : δ ≤ 1) (margin step : α → ℝ) (hstep : ∀ (x : α), |step x| ≤ 1) (shift : Bool) (hguard : shift = true → density source (γ * δ) margin ≤ δ * (1 + γ * δ / 16)) (hbelow : shift = true → 3 * δ / 8 ≤ (source.toOuterMeasure {x : α | margin x ≤ 0}).toReal) (hdensity : δ ≤ density source (γ * δ) fun (x : α) => margin x - if shift = true then 1 else 0) (hcorrelation : (γ * density source (γ * δ) fun (x : α) => margin x - if shift = true then 1 else 0) ≤ ∑ x : α, (source x).toReal * (weight (γ * δ) (margin x - if shift = true then 1 else 0) * step x)) : (averagePotential source (γ * δ) fun (x : α) => (margin x - if shift = true then 1 else 0) + step x) ≤ (averagePotential source (γ * δ) margin + if shift = true then δ else 0) - γ * δ ^ 2 / 8

One loop iteration decreases the potential after charging δ for an optional threshold increase. The guard allows either decision when the estimates' tolerance intervals overlap.

theorem Cslib.Crypto.Pseudoentropy.Boosting.dense_margin_lower_bound {α : Type u_1} [Fintype α] (source : PMF α) {rate : ℝ} (hrate : 0 < rate) (margin : α → ℝ) (threshold : ℝ) (softSet : α → ℝ) (hsoftSet : ∀ (x : α), softSet x ∈ Set.Icc 0 1) : (∑ x : α, (source x).toReal * softSet x) * (1 / (2 * rate) + threshold) ≤ ∑ x : α, (source x).toReal * (softSet x * margin x) + averagePotential source rate fun (x : α) => margin x - threshold

A low potential forces a large signed margin on every dense soft set. This form of Claim 2.13 uses soft sets and arbitrary finite sources, avoiding any rounding of set sizes.

theorem Cslib.Crypto.Pseudoentropy.Boosting.dense_margin_of_budget {α : Type u_1} [Fintype α] (source : PMF α) {rate δ threshold budget : ℝ} (hrate : 0 < rate) (hthreshold : 0 ≤ threshold) (margin softSet : α → ℝ) (hsoftSet : ∀ (x : α), softSet x ∈ Set.Icc 0 1) (hdensity : δ ≤ ∑ x : α, (source x).toReal * softSet x) (hbudget : 1 / (2 * rate) ≤ budget) (hprogress : (averagePotential source rate fun (x : α) => margin x - threshold) ≤ 1 / (2 * rate) + δ * threshold - budget) : (∑ x : α, (source x).toReal * softSet x) * budget ≤ ∑ x : α, (source x).toReal * (softSet x * margin x)

Once the accumulated decrease pays for the initial potential, every δ-dense soft set has average signed margin at least that decrease. At steps rounds with decrease γδ² / 8, this gives average correctness at least 1 / 2 + γδ² / 16, sufficient for the stopping test. Unlike a strict negativity argument, this includes an exact equality at the clock boundary.

theorem Cslib.Crypto.Pseudoentropy.Boosting.dense_margin_of_iterations {α : Type u_1} [Fintype α] (source : PMF α) {γ δ : ℝ} (hγ : 0 < γ) (hδ : 0 < δ) (margin : ℕ → α → ℝ) (threshold : ℕ → ℝ) (steps : ℕ) (hmargin : margin 0 = fun (x : α) => 0) (hthreshold : threshold 0 = 0) (hthreshold_nonneg : 0 ≤ threshold steps) (hstep : ∀ i < steps, (averagePotential source (γ * δ) fun (x : α) => margin (i + 1) x - threshold (i + 1)) ≤ (averagePotential source (γ * δ) fun (x : α) => margin i x - threshold i) + δ * (threshold (i + 1) - threshold i) - γ * δ ^ 2 / 8) (hclock : 4 ≤ ↑steps * γ ^ 2 * δ ^ 3) (softSet : α → ℝ) (hsoftSet : ∀ (x : α), softSet x ∈ Set.Icc 0 1) (hdensity : δ ≤ ∑ x : α, (source x).toReal * softSet x) : (∑ x : α, (source x).toReal * softSet x) * (↑steps * (γ * δ ^ 2 / 8)) ≤ ∑ x : α, (source x).toReal * (softSet x * margin steps x)

A clocked sequence of valid progress steps has a positive average margin on every dense soft set. The hypotheses describe the analysis of a run; they do not assume that its choices or stopping tests have already been implemented efficiently.

The clock condition is steps * γ² * δ³ ≥ 4. For positive integer inverse bounds, a sufficient clock is 4 * inverseGamma² * inverseDelta³ when γ ≥ 1 / inverseGamma and δ ≥ 1 / inverseDelta. At the clock boundary the average correctness over the predictors is at least 1 / 2 + γδ² / 16, once signed vote counts are divided by the number of steps.

theorem Cslib.Crypto.Pseudoentropy.Boosting.clock_sufficient (inverseGamma inverseDelta : ℕ) {γ δ : ℝ} (hγ : 1 ≤ ↑inverseGamma * γ) (hδ : 1 ≤ ↑inverseDelta * δ) : 4 ≤ ↑(4 * inverseGamma ^ 2 * inverseDelta ^ 3) * γ ^ 2 * δ ^ 3

Integer upper bounds on the inverse advantage and density give a polynomial round count.