Finite probability setup for the upper bound

This file defines the exact finite sample spaces used in the probabilistic upper-bound argument. It also records the interfaces for the Chernoff and Bernstein inputs. These are propositions, not axioms: later work must prove them or replace them with imported theorems.

@[reducible, inline]

abbrev PebblingLean.Hypercube.CenterSample (n N : ℕ) : Type

A sample of N independent uniform centers in Q_n, represented as a function on Fin N.

Equations

• PebblingLean.Hypercube.CenterSample n N = (Fin N → PebblingLean.HypercubeVertex n)

def PebblingLean.Hypercube.CenterSample.toList {n N : ℕ} (sample : CenterSample n N) : List (HypercubeVertex n)

Convert a center sample into the list used by the deterministic stack construction.

Equations

• sample.toList = List.ofFn sample

def PebblingLean.Hypercube.sampleTotalContribution {n N : ℕ} (rIn rOut : ℕ) (target : HypercubeVertex n) (sample : CenterSample n N) : ℕ

Total annulus contribution of a sampled N-tuple to a fixed target.

Equations

• PebblingLean.Hypercube.sampleTotalContribution rIn rOut target sample = ∑ j : Fin N, PebblingLean.Hypercube.annulusContribution rIn rOut target (sample j)

theorem PebblingLean.Hypercube.annulusTotalContribution_toList {n N rIn rOut : ℕ} (target : HypercubeVertex n) (sample : CenterSample n N) : annulusTotalContribution rIn rOut target sample.toList = sampleTotalContribution rIn rOut target sample

theorem PebblingLean.Hypercube.card_centerSample (n N : ℕ) : Fintype.card (CenterSample n N) = (2 ^ n) ^ N

noncomputable def PebblingLean.Hypercube.oneCenterContributionExpectation {n : ℕ} (rIn rOut : ℕ) (target : HypercubeVertex n) : ℚ

Exact expectation of one random annulus contribution.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PebblingLean.Hypercube.oneCenterContributionExpectationReal {n : ℕ} (rIn rOut : ℕ) (target : HypercubeVertex n) : ℝ

Real-valued version of the one-center annulus contribution expectation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PebblingLean.Hypercube.oneCenterContributionSecondMoment {n : ℕ} (rIn rOut : ℕ) (target : HypercubeVertex n) : ℚ

Exact second moment of one random annulus contribution.

Equations

• One or more equations did not get rendered due to their size.

theorem PebblingLean.Hypercube.oneCenterContributionExpectation_eq_sum {n rIn rOut : ℕ} (target : HypercubeVertex n) : oneCenterContributionExpectation rIn rOut target = (∑ center : HypercubeVertex n, ↑(annulusContribution rIn rOut target center)) / 2 ^ n

theorem PebblingLean.Hypercube.oneCenterContributionExpectationReal_eq_sum {n rIn rOut : ℕ} (target : HypercubeVertex n) : oneCenterContributionExpectationReal rIn rOut target = (∑ center : HypercubeVertex n, ↑(annulusContribution rIn rOut target center)) / 2 ^ n

theorem PebblingLean.Hypercube.oneCenterContributionSecondMoment_eq_sum {n rIn rOut : ℕ} (target : HypercubeVertex n) : oneCenterContributionSecondMoment rIn rOut target = (∑ center : HypercubeVertex n, ↑(annulusContribution rIn rOut target center) ^ 2) / 2 ^ n

theorem PebblingLean.Hypercube.oneCenterContributionSecondMoment_le_width_mul_expectation {n rIn rOut : ℕ} (target : HypercubeVertex n) : oneCenterContributionSecondMoment rIn rOut target ≤ 2 ^ (rOut - rIn) * oneCenterContributionExpectation rIn rOut target

Expectation-level version of Z^2 ≤ B_0 Z for one random annulus contribution.

theorem PebblingLean.Hypercube.card_filter_dist_eq {n i : ℕ} (target : HypercubeVertex n) : {center : HypercubeVertex n | dist target center = i}.card = n.choose i

Cardinality of a Hamming sphere, written as a filtered finite sum.

theorem PebblingLean.Hypercube.sum_filter_dist_eq_annulusContribution {n rIn rOut i : ℕ} (target : HypercubeVertex n) : ∑ center : HypercubeVertex n with dist target center = i, annulusContribution rIn rOut target center = n.choose i * if rIn ≤ i ∧ i ≤ rOut then 2 ^ (rOut - i) else 0

Sum of the annulus contribution over one Hamming sphere.

theorem PebblingLean.Hypercube.sum_annulusContribution_eq_sum_range {n rIn rOut : ℕ} (target : HypercubeVertex n) : ∑ center : HypercubeVertex n, annulusContribution rIn rOut target center = ∑ i ∈ Finset.range (n + 1), n.choose i * if rIn ≤ i ∧ i ≤ rOut then 2 ^ (rOut - i) else 0

Exact one-center annulus contribution, grouped by Hamming distance.

theorem PebblingLean.Hypercube.oneCenterContributionExpectation_eq_distance_sum {n rIn rOut : ℕ} (target : HypercubeVertex n) : oneCenterContributionExpectation rIn rOut target = (∑ i ∈ Finset.range (n + 1), ↑(n.choose i * if rIn ≤ i ∧ i ≤ rOut then 2 ^ (rOut - i) else 0)) / 2 ^ n

Exact one-center expectation as a binomial sphere sum.

def PebblingLean.Hypercube.annulusMeanNumerator (n rIn rOut : ℕ) : ℕ

Numerator of the expected contribution of one random stack. This is target-independent by symmetry of the cube.

Equations

• PebblingLean.Hypercube.annulusMeanNumerator n rIn rOut = ∑ i ∈ Finset.range (n + 1), n.choose i * if rIn ≤ i ∧ i ≤ rOut then 2 ^ (rOut - i) else 0

noncomputable def PebblingLean.Hypercube.annulusMean (n rIn rOut : ℕ) : ℚ

Expected contribution of one uniformly random annulus center.

Equations

• PebblingLean.Hypercube.annulusMean n rIn rOut = ↑(PebblingLean.Hypercube.annulusMeanNumerator n rIn rOut) / 2 ^ n

theorem PebblingLean.Hypercube.annulusMean_nonneg (n rIn rOut : ℕ) : 0 ≤ ↑(annulusMean n rIn rOut)

theorem PebblingLean.Hypercube.weightedSphereSum_half_eq (n : ℕ) : ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * (1 / 2) ^ i = (3 / 2) ^ n

Binomial evaluation of the full weighted Hamming-sphere sum.

theorem PebblingLean.Hypercube.pow_two_sub_eq_mul_half_pow {rOut i : ℕ} (hi : i ≤ rOut) : 2 ^ (rOut - i) = 2 ^ rOut * (1 / 2) ^ i

theorem PebblingLean.Hypercube.annulusMean_eq_real_sum (n rIn rOut : ℕ) : ↑(annulusMean n rIn rOut) = (∑ i ∈ Finset.range (n + 1), ↑(n.choose i * if rIn ≤ i ∧ i ≤ rOut then 2 ^ (rOut - i) else 0)) / 2 ^ n

theorem PebblingLean.Hypercube.annulusMean_le_fullWeightedMean (n rIn rOut : ℕ) : ↑(annulusMean n rIn rOut) ≤ 2 ^ rOut * (3 / 4) ^ n

Truncating to an annulus can only decrease the full weighted expectation 2^rOut (3/4)^n.

noncomputable def PebblingLean.Hypercube.binomialWindowProbThird (n rIn rOut : ℕ) : ℝ

The probability that a Binomial(n, 1/3) random variable lies in the annulus window [rIn, rOut]. This is the normalized form of the weighted annulus mean.

Equations

• PebblingLean.Hypercube.binomialWindowProbThird n rIn rOut = ∑ i ∈ Finset.range (n + 1), if rIn ≤ i ∧ i ≤ rOut then ↑(n.choose i) * (1 / 3) ^ i * (2 / 3) ^ (n - i) else 0

theorem PebblingLean.Hypercube.annulusWeightedTerm_eq_fullFactor_mul_binomialTerm {n rOut i : ℕ} (hin : i ≤ n) (hr : i ≤ rOut) : 2 ^ (rOut - i) / 2 ^ n = 2 ^ rOut * (3 / 4) ^ n * ((1 / 3) ^ i * (2 / 3) ^ (n - i))

Termwise conversion between the annulus contribution weight and the Binomial(1/3) mass after factoring out the full weighted mean 2^rOut (3/4)^n.

theorem PebblingLean.Hypercube.annulusMean_eq_fullWeightedMean_mul_binomialWindowProbThird (n rIn rOut : ℕ) : ↑(annulusMean n rIn rOut) = 2 ^ rOut * (3 / 4) ^ n * binomialWindowProbThird n rIn rOut

Exact normalization of the annulus mean: it is the full weighted mean 2^rOut (3/4)^n times a Binomial(n,1/3) window probability.

noncomputable def PebblingLean.Hypercube.binomialMassThird (n i : ℕ) : ℝ

Point mass of a Binomial(n,1/3) random variable at i.

Equations

• PebblingLean.Hypercube.binomialMassThird n i = ↑(n.choose i) * (1 / 3) ^ i * (2 / 3) ^ (n - i)

noncomputable def PebblingLean.Hypercube.binomialLeftTailProbThird (n rIn : ℕ) : ℝ

Left tail below the inner annulus radius for Binomial(n,1/3).

Equations

• PebblingLean.Hypercube.binomialLeftTailProbThird n rIn = ∑ i ∈ Finset.range (n + 1), if i < rIn then PebblingLean.Hypercube.binomialMassThird n i else 0

noncomputable def PebblingLean.Hypercube.binomialRightTailProbThird (n rOut : ℕ) : ℝ

Right tail above the outer annulus radius for Binomial(n,1/3).

Equations

• PebblingLean.Hypercube.binomialRightTailProbThird n rOut = ∑ i ∈ Finset.range (n + 1), if rOut < i then PebblingLean.Hypercube.binomialMassThird n i else 0

theorem PebblingLean.Hypercube.binomialMassThird_nonneg (n i : ℕ) : 0 ≤ binomialMassThird n i

theorem PebblingLean.Hypercube.binomialTotalProbThird_eq_one (n : ℕ) : ∑ i ∈ Finset.range (n + 1), binomialMassThird n i = 1

theorem PebblingLean.Hypercube.binomialWindow_tail_partition_term {n rIn rOut i : ℕ} (hr : rIn ≤ rOut) : (((if rIn ≤ i ∧ i ≤ rOut then binomialMassThird n i else 0) + if i < rIn then binomialMassThird n i else 0) + if rOut < i then binomialMassThird n i else 0) = binomialMassThird n i

For a valid annulus, every binomial mass is either inside the window, in the left tail, or in the right tail.

theorem PebblingLean.Hypercube.binomialWindowProbThird_add_tails_eq_one (n rIn rOut : ℕ) (hr : rIn ≤ rOut) : binomialWindowProbThird n rIn rOut + binomialLeftTailProbThird n rIn + binomialRightTailProbThird n rOut = 1

Window probability plus the two outside tails equals one.

theorem PebblingLean.Hypercube.binomialWindowProbThird_lower_of_tails_le {n rIn rOut : ℕ} {eps : ℝ} (hr : rIn ≤ rOut) (htails : binomialLeftTailProbThird n rIn + binomialRightTailProbThird n rOut ≤ eps) : 1 - eps ≤ binomialWindowProbThird n rIn rOut

If the two binomial tails outside the annulus have total mass at most eps, then the annulus window has mass at least 1-eps.

theorem PebblingLean.Hypercube.binomialExpNegMomentThird_eq (n : ℕ) (lam : ℝ) : ∑ i ∈ Finset.range (n + 1), binomialMassThird n i * Real.exp (-lam) ^ i = (1 / 3 * Real.exp (-lam) + 2 / 3) ^ n

Exact negative exponential moment of Binomial(n,1/3).

theorem PebblingLean.Hypercube.binomialExpMomentThird_eq (n : ℕ) (lam : ℝ) : ∑ i ∈ Finset.range (n + 1), binomialMassThird n i * Real.exp lam ^ i = (1 / 3 * Real.exp lam + 2 / 3) ^ n

Exact positive exponential moment of Binomial(n,1/3).

theorem PebblingLean.Hypercube.binomialLeftTailProbThird_le_chernoff (n rIn : ℕ) {lam : ℝ} (hlam : 0 ≤ lam) : binomialLeftTailProbThird n rIn ≤ Real.exp (lam * ↑rIn) * (1 / 3 * Real.exp (-lam) + 2 / 3) ^ n

Chernoff bound for the left tail of Binomial(n,1/3), with arbitrary nonnegative parameter lam.

theorem PebblingLean.Hypercube.binomialRightTailProbThird_le_chernoff (n rOut : ℕ) {lam : ℝ} (hlam : 0 ≤ lam) : binomialRightTailProbThird n rOut ≤ Real.exp (-(lam * ↑rOut)) * (1 / 3 * Real.exp lam + 2 / 3) ^ n

Chernoff bound for the right tail of Binomial(n,1/3), with arbitrary nonnegative parameter lam.

theorem PebblingLean.Hypercube.oneCenterContributionExpectation_eq_annulusMean {n rIn rOut : ℕ} (target : HypercubeVertex n) : oneCenterContributionExpectation rIn rOut target = annulusMean n rIn rOut

theorem PebblingLean.Hypercube.oneCenterContributionExpectationReal_eq_coe {n rIn rOut : ℕ} (target : HypercubeVertex n) : oneCenterContributionExpectationReal rIn rOut target = ↑(oneCenterContributionExpectation rIn rOut target)

theorem PebblingLean.Hypercube.oneCenterContributionExpectationReal_eq_annulusMean {n rIn rOut : ℕ} (target : HypercubeVertex n) : oneCenterContributionExpectationReal rIn rOut target = ↑(annulusMean n rIn rOut)

noncomputable def PebblingLean.Hypercube.sampleContributionExpectation {n N : ℕ} (rIn rOut : ℕ) (target : HypercubeVertex n) : ℚ

Exact expectation of the total annulus contribution from an N-tuple of uniform centers.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PebblingLean.Hypercube.sampleContributionSecondMomentProxy {n N : ℕ} (rIn rOut : ℕ) (target : HypercubeVertex n) : ℚ

Sum of the second moments of the N independent one-center contributions. This is the variance proxy used by Bernstein; the actual variance is bounded by this quantity.

Equations

• PebblingLean.Hypercube.sampleContributionSecondMomentProxy rIn rOut target = ↑N * PebblingLean.Hypercube.oneCenterContributionSecondMoment rIn rOut target

theorem PebblingLean.Hypercube.sampleContributionExpectation_eq_sum {n N rIn rOut : ℕ} (target : HypercubeVertex n) : sampleContributionExpectation rIn rOut target = (∑ sample : CenterSample n N, ↑(sampleTotalContribution rIn rOut target sample)) / ↑(Fintype.card (CenterSample n N))

theorem PebblingLean.Hypercube.sum_centerSample_eval {n N : ℕ} (j : Fin N) (f : HypercubeVertex n → ℕ) : ∑ sample : CenterSample n N, ↑(f (sample j)) = (2 ^ n) ^ (N - 1) * ∑ center : HypercubeVertex n, ↑(f center)

For a fixed coordinate of the random center tuple, summing over all samples is the one-center sum multiplied by the number of choices for the remaining coordinates.

theorem PebblingLean.Hypercube.sum_sampleTotalContribution_eq {n N rIn rOut : ℕ} (target : HypercubeVertex n) : ∑ sample : CenterSample n N, ↑(sampleTotalContribution rIn rOut target sample) = ↑N * (2 ^ n) ^ (N - 1) * ∑ center : HypercubeVertex n, ↑(annulusContribution rIn rOut target center)

Numerator of the N-center expectation, written as N copies of the one-coordinate sum.

theorem PebblingLean.Hypercube.sampleContributionExpectation_eq_nat_mul_oneCenter {n N rIn rOut : ℕ} (target : HypercubeVertex n) : sampleContributionExpectation rIn rOut target = ↑N * oneCenterContributionExpectation rIn rOut target

Linearity of expectation for the independent uniform center tuple used here: the expected total contribution is N times the one-center expectation.

theorem PebblingLean.Hypercube.sampleContributionExpectation_eq_nat_mul_annulusMean {n N rIn rOut : ℕ} (target : HypercubeVertex n) : sampleContributionExpectation rIn rOut target = ↑N * annulusMean n rIn rOut

theorem PebblingLean.Hypercube.sampleContributionSecondMomentProxy_le_width_mul_expectation {n N rIn rOut : ℕ} (target : HypercubeVertex n) : sampleContributionSecondMomentProxy rIn rOut target ≤ 2 ^ (rOut - rIn) * sampleContributionExpectation rIn rOut target

Bernstein variance-proxy bound: the sum of one-center second moments is at most the annulus width factor times the mean total contribution.

theorem PebblingLean.Hypercube.sampleContributionSecondMomentProxy_le_two_width_mul_T {n N rIn rOut T : ℕ} (target : HypercubeVertex n) (hmean_upper : sampleContributionExpectation rIn rOut target ≤ 2 * ↑T) : sampleContributionSecondMomentProxy rIn rOut target ≤ 2 * 2 ^ (rOut - rIn) * ↑T

Paper-facing variance-proxy corollary: once the expected total contribution is at most 2T, the Bernstein variance proxy is at most 2 B_0 T.

def PebblingLean.Hypercube.sampleTargetFails {n N : ℕ} (rIn rOut T : ℕ) (target : HypercubeVertex n) (sample : CenterSample n N) : Prop

The event that a particular target receives less than demand T.

Equations

• PebblingLean.Hypercube.sampleTargetFails rIn rOut T target sample = (PebblingLean.Hypercube.sampleTotalContribution rIn rOut target sample < T)

@[implicit_reducible]

instance PebblingLean.Hypercube.instDecidableSampleTargetFails {n N rIn rOut T : ℕ} (target : HypercubeVertex n) (sample : CenterSample n N) : Decidable (sampleTargetFails rIn rOut T target sample)

Equations

• PebblingLean.Hypercube.instDecidableSampleTargetFails target sample = id inferInstance

@[implicit_reducible]

instance PebblingLean.Hypercube.instDecidablePredSampleTargetFails {n N rIn rOut T : ℕ} (target : HypercubeVertex n) : DecidablePred (sampleTargetFails rIn rOut T target)

Equations

• PebblingLean.Hypercube.instDecidablePredSampleTargetFails target sample = PebblingLean.Hypercube.instDecidableSampleTargetFails target sample

def PebblingLean.Hypercube.sampleFailsSomeTarget {n N : ℕ} (rIn rOut T : ℕ) (sample : CenterSample n N) : Prop

The event that some target receives less than demand T.

Equations

• PebblingLean.Hypercube.sampleFailsSomeTarget rIn rOut T sample = ∃ (target : PebblingLean.HypercubeVertex n), PebblingLean.Hypercube.sampleTargetFails rIn rOut T target sample

@[implicit_reducible]

instance PebblingLean.Hypercube.instDecidableSampleFailsSomeTarget {n N rIn rOut T : ℕ} (sample : CenterSample n N) : Decidable (sampleFailsSomeTarget rIn rOut T sample)

Equations

• PebblingLean.Hypercube.instDecidableSampleFailsSomeTarget sample = id inferInstance

@[implicit_reducible]

instance PebblingLean.Hypercube.instDecidablePredSampleFailsSomeTarget {n N rIn rOut T : ℕ} : DecidablePred (sampleFailsSomeTarget rIn rOut T)

Equations

• PebblingLean.Hypercube.instDecidablePredSampleFailsSomeTarget sample = PebblingLean.Hypercube.instDecidableSampleFailsSomeTarget sample

noncomputable def PebblingLean.Hypercube.targetFailureProbability {n N : ℕ} (rIn rOut T : ℕ) (target : HypercubeVertex n) : ℚ

Failure probability for one fixed target. This is the quantity controlled by Bernstein in the proof.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PebblingLean.Hypercube.targetFailureProbabilityReal {n N : ℕ} (rIn rOut T : ℕ) (target : HypercubeVertex n) : ℝ

Real-valued form of the fixed-target failure probability, used for exponential tail estimates.

Equations

• One or more equations did not get rendered due to their size.

theorem PebblingLean.Hypercube.targetFailureProbabilityReal_eq_coe {n N rIn rOut T : ℕ} (target : HypercubeVertex n) : targetFailureProbabilityReal rIn rOut T target = ↑(targetFailureProbability rIn rOut T target)

noncomputable def PebblingLean.Hypercube.targetLowerTailExponentialMoment {n N : ℕ} (rIn rOut T : ℕ) (target : HypercubeVertex n) (lam : ℝ) : ℝ

Exponential moment used by the Chernoff/Markov lower-tail argument for a fixed target.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PebblingLean.Hypercube.oneCenterNegativeExponentialMoment {n : ℕ} (rIn rOut : ℕ) (target : HypercubeVertex n) (lam : ℝ) : ℝ

One-center exponential moment appearing after independence factorization of the lower-tail Chernoff bound.

Equations

• One or more equations did not get rendered due to their size.

theorem PebblingLean.Hypercube.oneCenterNegativeExponentialMoment_nonneg {n rIn rOut : ℕ} (target : HypercubeVertex n) (lam : ℝ) : 0 ≤ oneCenterNegativeExponentialMoment rIn rOut target lam

theorem PebblingLean.Hypercube.oneCenterNegativeExponentialMoment_le_chord {n rIn rOut : ℕ} (target : HypercubeVertex n) (lam : ℝ) : oneCenterNegativeExponentialMoment rIn rOut target lam ≤ 1 - (1 - Real.exp (-(lam * 2 ^ (rOut - rIn)))) * (oneCenterContributionExpectationReal rIn rOut target / 2 ^ (rOut - rIn))

One-center bounded-nonnegative Chernoff estimate: the negative exponential moment is bounded by the chord estimate in terms of the one-center mean and the annulus width B_0 = 2^(rOut-rIn).

theorem PebblingLean.Hypercube.sum_filter_dist_eq_exp_annulusContribution {n rIn rOut i : ℕ} (target : HypercubeVertex n) (lam : ℝ) : ∑ center : HypercubeVertex n with dist target center = i, Real.exp (-(lam * ↑(annulusContribution rIn rOut target center))) = ↑(n.choose i) * Real.exp (-(lam * ↑(if rIn ≤ i ∧ i ≤ rOut then 2 ^ (rOut - i) else 0)))

Sum of the one-center negative exponential factor over one Hamming sphere.

theorem PebblingLean.Hypercube.sum_exp_annulusContribution_eq_sum_range {n rIn rOut : ℕ} (target : HypercubeVertex n) (lam : ℝ) : ∑ center : HypercubeVertex n, Real.exp (-(lam * ↑(annulusContribution rIn rOut target center))) = ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * Real.exp (-(lam * ↑(if rIn ≤ i ∧ i ≤ rOut then 2 ^ (rOut - i) else 0)))

Exact one-center negative exponential moment numerator, grouped by Hamming distance.

theorem PebblingLean.Hypercube.oneCenterNegativeExponentialMoment_eq_distance_sum {n rIn rOut : ℕ} (target : HypercubeVertex n) (lam : ℝ) : oneCenterNegativeExponentialMoment rIn rOut target lam = (∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * Real.exp (-(lam * ↑(if rIn ≤ i ∧ i ≤ rOut then 2 ^ (rOut - i) else 0)))) / 2 ^ n

Exact one-center negative exponential moment as a binomial Hamming-sphere sum.

theorem PebblingLean.Hypercube.oneCenterNegativeExponentialMoment_eq_of_targets {n rIn rOut : ℕ} (target target' : HypercubeVertex n) (lam : ℝ) : oneCenterNegativeExponentialMoment rIn rOut target lam = oneCenterNegativeExponentialMoment rIn rOut target' lam

The one-center exponential moment is independent of the target, by hypercube symmetry and the Hamming-sphere count.

theorem PebblingLean.Hypercube.exp_neg_sampleTotalContribution_eq_prod {n N rIn rOut : ℕ} (target : HypercubeVertex n) (lam : ℝ) (sample : CenterSample n N) : Real.exp (-(lam * ↑(sampleTotalContribution rIn rOut target sample))) = ∏ j : Fin N, Real.exp (-(lam * ↑(annulusContribution rIn rOut target (sample j))))

theorem PebblingLean.Hypercube.sum_prod_oneCenterNegativeExponentialMoment {n N rIn rOut : ℕ} (target : HypercubeVertex n) (lam : ℝ) : ∑ sample : CenterSample n N, ∏ j : Fin N, Real.exp (-(lam * ↑(annulusContribution rIn rOut target (sample j)))) = (∑ center : HypercubeVertex n, Real.exp (-(lam * ↑(annulusContribution rIn rOut target center)))) ^ N

The product-space sum of independent one-center exponential factors factors as the Nth power of the one-center sum.

theorem PebblingLean.Hypercube.sum_exp_neg_sampleTotalContribution_eq_pow {n N rIn rOut : ℕ} (target : HypercubeVertex n) (lam : ℝ) : ∑ sample : CenterSample n N, Real.exp (-(lam * ↑(sampleTotalContribution rIn rOut target sample))) = (∑ center : HypercubeVertex n, Real.exp (-(lam * ↑(annulusContribution rIn rOut target center)))) ^ N

theorem PebblingLean.Hypercube.exp_target_sub_sampleTotalContribution {n N rIn rOut T : ℕ} (target : HypercubeVertex n) (lam : ℝ) (sample : CenterSample n N) : Real.exp (lam * (↑T - ↑(sampleTotalContribution rIn rOut target sample))) = Real.exp (lam * ↑T) * Real.exp (-(lam * ↑(sampleTotalContribution rIn rOut target sample)))

theorem PebblingLean.Hypercube.targetLowerTailExponentialMoment_eq {n N rIn rOut T : ℕ} (target : HypercubeVertex n) (lam : ℝ) : targetLowerTailExponentialMoment rIn rOut T target lam = Real.exp (lam * ↑T) * oneCenterNegativeExponentialMoment rIn rOut target lam ^ N

Independence factorization for the lower-tail exponential moment.

theorem PebblingLean.Hypercube.targetLowerTailExponentialMoment_le_exp_chord {n N rIn rOut T : ℕ} (target : HypercubeVertex n) {lam : ℝ} (hlam_nonneg : 0 ≤ lam) : targetLowerTailExponentialMoment rIn rOut T target lam ≤ Real.exp (lam * ↑T - ↑N * ((1 - Real.exp (-(lam * 2 ^ (rOut - rIn)))) * (oneCenterContributionExpectationReal rIn rOut target / 2 ^ (rOut - rIn))))

Chord-based lower-tail exponential-moment bound before optimizing the Chernoff parameter. Here B = 2^(rOut-rIn) and the parenthesized term is the one-center chord drop.

theorem PebblingLean.Hypercube.targetLowerTailExponentialMoment_le_exp_optimized_chord {n N rIn rOut T : ℕ} (target : HypercubeVertex n) {gap : ℝ} (hgap : 0 ≤ gap) (hmu_pos : 0 < ↑N * oneCenterContributionExpectationReal rIn rOut target) (hmean : ↑T + gap ≤ ↑N * oneCenterContributionExpectationReal rIn rOut target) : targetLowerTailExponentialMoment rIn rOut T target (gap / (2 * 2 ^ (rOut - rIn) * (↑N * oneCenterContributionExpectationReal rIn rOut target))) ≤ Real.exp (-(gap ^ 2 / (4 * 2 ^ (rOut - rIn) * (↑N * oneCenterContributionExpectationReal rIn rOut target))))

Optimized chord-based Chernoff bound for one fixed target. This is the analytic gap-closing statement: if the expected annulus contribution mu exceeds the threshold by gap, then the optimized exponential moment is bounded by exp(-gap^2/(4 B mu)), where B = 2^(rOut-rIn).

def PebblingLean.Hypercube.OneCenterExponentialMomentBound (n N rIn rOut T : ℕ) (lam eps : ℝ) : Prop

A target-independent one-center exponential-moment bound for a fixed Chernoff parameter. The default target is arbitrary; the preceding target-independence theorem shows that it represents every target.

Equations

• One or more equations did not get rendered due to their size.

def PebblingLean.Hypercube.OneCenterDistanceSumExponentialMomentBound (n N rIn rOut T : ℕ) (lam eps : ℝ) : Prop

The same one-center exponential-moment bound, with the one-center moment expanded as the explicit binomial Hamming-sphere sum. This is the exact analytic expression that a Bernstein estimate must bound.

Equations

• One or more equations did not get rendered due to their size.

theorem PebblingLean.Hypercube.oneCenterExponentialMomentBound_of_distanceSum {n N rIn rOut T : ℕ} {lam eps : ℝ} (hbound : OneCenterDistanceSumExponentialMomentBound n N rIn rOut T lam eps) : OneCenterExponentialMomentBound n N rIn rOut T lam eps

theorem PebblingLean.Hypercube.targetFailureProbabilityReal_le_exponentialMoment {n N rIn rOut T : ℕ} (target : HypercubeVertex n) {lam : ℝ} (hlam : 0 < lam) : targetFailureProbabilityReal rIn rOut T target ≤ targetLowerTailExponentialMoment rIn rOut T target lam

theorem PebblingLean.Hypercube.targetFailureProbability_le_of_exponentialMoment_le {n N rIn rOut T : ℕ} (target : HypercubeVertex n) {lam : ℝ} {eps : ℚ} (hlam : 0 < lam) (hmoment : targetLowerTailExponentialMoment rIn rOut T target lam ≤ ↑eps) : targetFailureProbability rIn rOut T target ≤ eps

theorem PebblingLean.Hypercube.targetFailureProbability_le_exp_neg_of_exponentialMoment_le {n N rIn rOut T : ℕ} (target : HypercubeVertex n) {lam exponent : ℝ} {eps : ℚ} (hlam : 0 < lam) (hmoment : targetLowerTailExponentialMoment rIn rOut T target lam ≤ Real.exp (-exponent)) (hexp : Real.exp (-exponent) ≤ ↑eps) : targetFailureProbability rIn rOut T target ≤ eps

theorem PebblingLean.Hypercube.targetFailureProbability_le_exp_optimized_chord {n N rIn rOut T : ℕ} (target : HypercubeVertex n) {gap : ℝ} {eps : ℚ} (hgap_pos : 0 < gap) (hmu_pos : 0 < ↑N * oneCenterContributionExpectationReal rIn rOut target) (hmean : ↑T + gap ≤ ↑N * oneCenterContributionExpectationReal rIn rOut target) (hexp : Real.exp (-(gap ^ 2 / (4 * 2 ^ (rOut - rIn) * (↑N * oneCenterContributionExpectationReal rIn rOut target)))) ≤ ↑eps) : targetFailureProbability rIn rOut T target ≤ eps

Fixed-target failure bound obtained from the optimized chord Chernoff estimate.

noncomputable def PebblingLean.Hypercube.globalFailureProbability {n N : ℕ} (rIn rOut T : ℕ) : ℚ

Probability that some target fails.

Equations

• One or more equations did not get rendered due to their size.

theorem PebblingLean.Hypercube.globalFailureProbability_le_sum_targetFailureProbability {n N rIn rOut T : ℕ} : globalFailureProbability rIn rOut T ≤ ∑ target : HypercubeVertex n, targetFailureProbability rIn rOut T target

Union bound over all targets.

theorem PebblingLean.Hypercube.exists_goodCenterSample_of_globalFailureProbability_lt_one {n N rIn rOut T : ℕ} (hprob : globalFailureProbability rIn rOut T < 1) : ∃ (sample : CenterSample n N), IsGoodCenterList n rIn rOut T sample.toList

Probabilistic-method extraction: if the probability that some target fails is less than one, then a good center sample exists.

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_of_globalFailureProbability_lt_one {n N rIn rOut T : ℕ} (hprob : globalFailureProbability rIn rOut T < 1) : Pebbling.HasSolvableAtMostSize (graph n) T (N * 2 ^ rOut)

Costed high-demand conclusion from a global failure-probability bound.

theorem PebblingLean.Hypercube.hasHighDemandDistribution_of_globalFailureProbability_lt_one {n N rIn rOut T : ℕ} (hprob : globalFailureProbability rIn rOut T < 1) : HasHighDemandDistribution n T (N * 2 ^ rOut) (2 ^ rOut)

High-demand version of the probabilistic-method extraction. The selected stack-list distribution has occupied piles of size at least 2^rOut.

def PebblingLean.Hypercube.ChernoffMeanLowerBound (n N rIn rOut T : ℕ) : Prop

The Chernoff input used in this project: the annulus captures enough expected contribution for every target.

Equations

• PebblingLean.Hypercube.ChernoffMeanLowerBound n N rIn rOut T = ∀ (target : PebblingLean.HypercubeVertex n), ↑T ≤ PebblingLean.Hypercube.sampleContributionExpectation rIn rOut target

theorem PebblingLean.Hypercube.chernoffMeanLowerBound_iff_annulusMean {n N rIn rOut T : ℕ} : ChernoffMeanLowerBound n N rIn rOut T ↔ ↑T ≤ ↑N * annulusMean n rIn rOut

theorem PebblingLean.Hypercube.chernoffMeanLowerBound_of_annulusMean {n N rIn rOut T : ℕ} (hmean : ↑T ≤ ↑N * annulusMean n rIn rOut) : ChernoffMeanLowerBound n N rIn rOut T

def PebblingLean.Hypercube.BernsteinTargetFailureBound (n N rIn rOut T : ℕ) (eps : ℚ) : Prop

The Bernstein input used in this project: every fixed target has small lower tail probability.

Equations

• PebblingLean.Hypercube.BernsteinTargetFailureBound n N rIn rOut T eps = ∀ (target : PebblingLean.HypercubeVertex n), PebblingLean.Hypercube.targetFailureProbability rIn rOut T target ≤ eps

theorem PebblingLean.Hypercube.bernsteinTargetFailureBound_of_optimized_chord_annulusMean {n N rIn rOut T : ℕ} {gap : ℝ} {eps : ℚ} (hgap_pos : 0 < gap) (hmu_pos : 0 < ↑N * ↑(annulusMean n rIn rOut)) (hmean : ↑T + gap ≤ ↑N * ↑(annulusMean n rIn rOut)) (hexp : Real.exp (-(gap ^ 2 / (4 * 2 ^ (rOut - rIn) * (↑N * ↑(annulusMean n rIn rOut))))) ≤ ↑eps) : BernsteinTargetFailureBound n N rIn rOut T eps

Target-failure bound with the target-independent real annulus mean substituted for the fixed-target mean.

def PebblingLean.Hypercube.ChernoffExponentialMomentBound (n N rIn rOut T : ℕ) (eps : ℝ) : Prop

Chernoff-style exponential moment input: for each fixed target, there is a positive exponential parameter whose lower-tail moment is at most eps.

Equations

• One or more equations did not get rendered due to their size.

theorem PebblingLean.Hypercube.chernoffExponentialMomentBound_of_oneCenterExponentialMomentBound {n N rIn rOut T : ℕ} {lam eps : ℝ} (hbound : OneCenterExponentialMomentBound n N rIn rOut T lam eps) : ChernoffExponentialMomentBound n N rIn rOut T eps

theorem PebblingLean.Hypercube.bernsteinTargetFailureBound_of_chernoffExponentialMomentBound {n N rIn rOut T : ℕ} {epsReal : ℝ} {eps : ℚ} (hmoment : ChernoffExponentialMomentBound n N rIn rOut T epsReal) (heps : epsReal ≤ ↑eps) : BernsteinTargetFailureBound n N rIn rOut T eps

noncomputable def PebblingLean.Hypercube.bernsteinExponent (variance scale gap : ℝ) : ℝ

The usual Bernstein lower-tail exponent, parameterized by a variance proxy, a per-summand scale, and the gap between the mean and threshold.

Equations

• PebblingLean.Hypercube.bernsteinExponent variance scale gap = gap ^ 2 / (2 * (variance + scale * gap / 3))

theorem PebblingLean.Hypercube.bernsteinExponent_two_width_mul_T_ge {delta T B : ℝ} (hdelta_nonneg : 0 ≤ delta) (hdelta_le : delta ≤ 1 / 2) (hT_pos : 0 < T) (hB_pos : 0 < B) : delta ^ 2 * T / (96 * B) ≤ bernsteinExponent (2 * B * T) B (delta * T / 4)

The constant calculation used in the paper after Bernstein is applied with variance proxy 2 * B * T, scale B, and gap delta*T/4.

def PebblingLean.Hypercube.BernsteinExponentialMomentBound (n N rIn rOut T : ℕ) (variance scale gap : ℝ) : Prop

Bernstein-style exponential moment input. The analytic Bernstein argument must prove this proposition for the parameters chosen in the upper-bound proof.

Equations

• One or more equations did not get rendered due to their size.

theorem PebblingLean.Hypercube.bernsteinExponentialMomentBound_of_oneCenterDistanceSum {n N rIn rOut T : ℕ} {lam variance scale gap : ℝ} (hbound : OneCenterDistanceSumExponentialMomentBound n N rIn rOut T lam (Real.exp (-bernsteinExponent variance scale gap))) : BernsteinExponentialMomentBound n N rIn rOut T variance scale gap

theorem PebblingLean.Hypercube.bernsteinTargetFailureBound_of_bernsteinExponentialMomentBound {n N rIn rOut T : ℕ} {variance scale gap : ℝ} {eps : ℚ} (hmoment : BernsteinExponentialMomentBound n N rIn rOut T variance scale gap) (hexp : Real.exp (-bernsteinExponent variance scale gap) ≤ ↑eps) : BernsteinTargetFailureBound n N rIn rOut T eps

theorem PebblingLean.Hypercube.exists_goodCenterSample_of_bernstein_bound {n N rIn rOut T : ℕ} {eps : ℚ} (hbernstein : BernsteinTargetFailureBound n N rIn rOut T eps) (hunion : ↑(Fintype.card (HypercubeVertex n)) * eps < 1) : ∃ (sample : CenterSample n N), IsGoodCenterList n rIn rOut T sample.toList

The usual union-bound finish from a Bernstein fixed-target estimate.

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_of_bernstein_bound {n N rIn rOut T : ℕ} {eps : ℚ} (hbernstein : BernsteinTargetFailureBound n N rIn rOut T eps) (hunion : ↑(Fintype.card (HypercubeVertex n)) * eps < 1) : Pebbling.HasSolvableAtMostSize (graph n) T (N * 2 ^ rOut)

Costed high-demand conclusion from the Bernstein fixed-target estimate.

theorem PebblingLean.Hypercube.hypercube_card_mul_inv_two_pow_succ_lt_one (n : ℕ) : ↑(Fintype.card (HypercubeVertex n)) * (1 / 2 ^ (n + 1)) < 1

theorem PebblingLean.Hypercube.exists_goodCenterSample_of_optimized_chord_annulusMean {n N rIn rOut T : ℕ} {gap : ℝ} {eps : ℚ} (hgap_pos : 0 < gap) (hmu_pos : 0 < ↑N * ↑(annulusMean n rIn rOut)) (hmean : ↑T + gap ≤ ↑N * ↑(annulusMean n rIn rOut)) (hexp : Real.exp (-(gap ^ 2 / (4 * 2 ^ (rOut - rIn) * (↑N * ↑(annulusMean n rIn rOut))))) ≤ ↑eps) (hunion : ↑(Fintype.card (HypercubeVertex n)) * eps < 1) : ∃ (sample : CenterSample n N), IsGoodCenterList n rIn rOut T sample.toList

Probabilistic-method finish from the optimized chord Chernoff estimate, using the target-independent annulus mean.

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_of_optimized_chord_annulusMean {n N rIn rOut T : ℕ} {gap : ℝ} {eps : ℚ} (hgap_pos : 0 < gap) (hmu_pos : 0 < ↑N * ↑(annulusMean n rIn rOut)) (hmean : ↑T + gap ≤ ↑N * ↑(annulusMean n rIn rOut)) (hexp : Real.exp (-(gap ^ 2 / (4 * 2 ^ (rOut - rIn) * (↑N * ↑(annulusMean n rIn rOut))))) ≤ ↑eps) (hunion : ↑(Fintype.card (HypercubeVertex n)) * eps < 1) : Pebbling.HasSolvableAtMostSize (graph n) T (N * 2 ^ rOut)

Costed high-demand conclusion from the optimized chord Chernoff estimate.

theorem PebblingLean.Hypercube.exists_goodCenterSample_of_optimized_chord_annulusMean_inv_two {n N rIn rOut T : ℕ} {gap : ℝ} (hgap_pos : 0 < gap) (hmu_pos : 0 < ↑N * ↑(annulusMean n rIn rOut)) (hmean : ↑T + gap ≤ ↑N * ↑(annulusMean n rIn rOut)) (hexp : Real.exp (-(gap ^ 2 / (4 * 2 ^ (rOut - rIn) * (↑N * ↑(annulusMean n rIn rOut))))) ≤ ↑(1 / 2 ^ (n + 1))) : ∃ (sample : CenterSample n N), IsGoodCenterList n rIn rOut T sample.toList

Optimized chord Chernoff finish with the standard fixed-target failure budget 2^-(n+1), which is strong enough for the union bound over Q_n.

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_of_optimized_chord_annulusMean_inv_two {n N rIn rOut T : ℕ} {gap : ℝ} (hgap_pos : 0 < gap) (hmu_pos : 0 < ↑N * ↑(annulusMean n rIn rOut)) (hmean : ↑T + gap ≤ ↑N * ↑(annulusMean n rIn rOut)) (hexp : Real.exp (-(gap ^ 2 / (4 * 2 ^ (rOut - rIn) * (↑N * ↑(annulusMean n rIn rOut))))) ≤ ↑(1 / 2 ^ (n + 1))) : Pebbling.HasSolvableAtMostSize (graph n) T (N * 2 ^ rOut)

Costed high-demand conclusion with fixed-target failure budget 2^-(n+1).

theorem PebblingLean.Hypercube.exists_goodCenterSample_of_optimized_chord_annulusMean_log {n N rIn rOut T : ℕ} {gap : ℝ} (hgap_pos : 0 < gap) (hmu_pos : 0 < ↑N * ↑(annulusMean n rIn rOut)) (hmean : ↑T + gap ≤ ↑N * ↑(annulusMean n rIn rOut)) (hlog : ↑(n + 1) * Real.log 2 ≤ gap ^ 2 / (4 * 2 ^ (rOut - rIn) * (↑N * ↑(annulusMean n rIn rOut)))) : ∃ (sample : CenterSample n N), IsGoodCenterList n rIn rOut T sample.toList

Version of the optimized chord finish where the union-bound comparison is discharged by the exponent inequality exponent ≥ (n+1) log 2.

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_of_optimized_chord_annulusMean_log {n N rIn rOut T : ℕ} {gap : ℝ} (hgap_pos : 0 < gap) (hmu_pos : 0 < ↑N * ↑(annulusMean n rIn rOut)) (hmean : ↑T + gap ≤ ↑N * ↑(annulusMean n rIn rOut)) (hlog : ↑(n + 1) * Real.log 2 ≤ gap ^ 2 / (4 * 2 ^ (rOut - rIn) * (↑N * ↑(annulusMean n rIn rOut)))) : Pebbling.HasSolvableAtMostSize (graph n) T (N * 2 ^ rOut)

Costed high-demand conclusion from the optimized chord estimate and the exponent condition gap^2/(4 B_0 mu) ≥ (n+1) log 2.

theorem PebblingLean.Hypercube.exists_goodCenterSample_of_optimized_chord_annulusMean_log_of_mean_gap {n N rIn rOut T : ℕ} {gap : ℝ} (hgap_pos : 0 < gap) (hmean : ↑T + gap ≤ ↑N * ↑(annulusMean n rIn rOut)) (hlog : ↑(n + 1) * Real.log 2 ≤ gap ^ 2 / (4 * 2 ^ (rOut - rIn) * (↑N * ↑(annulusMean n rIn rOut)))) : ∃ (sample : CenterSample n N), IsGoodCenterList n rIn rOut T sample.toList

The same log-threshold finish, deriving positivity of the mean from the positive gap and the inequality T + gap ≤ mean.

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_of_optimized_chord_annulusMean_log_of_mean_gap {n N rIn rOut T : ℕ} {gap : ℝ} (hgap_pos : 0 < gap) (hmean : ↑T + gap ≤ ↑N * ↑(annulusMean n rIn rOut)) (hlog : ↑(n + 1) * Real.log 2 ≤ gap ^ 2 / (4 * 2 ^ (rOut - rIn) * (↑N * ↑(annulusMean n rIn rOut)))) : Pebbling.HasSolvableAtMostSize (graph n) T (N * 2 ^ rOut)

Costed high-demand conclusion with positivity of the mean derived from the mean-gap hypothesis.

theorem PebblingLean.Hypercube.hasHighDemandDistribution_of_optimized_chord_annulusMean_log_of_mean_gap {n N rIn rOut T : ℕ} {gap : ℝ} (hgap_pos : 0 < gap) (hmean : ↑T + gap ≤ ↑N * ↑(annulusMean n rIn rOut)) (hlog : ↑(n + 1) * Real.log 2 ≤ gap ^ 2 / (4 * 2 ^ (rOut - rIn) * (↑N * ↑(annulusMean n rIn rOut)))) : HasHighDemandDistribution n T (N * 2 ^ rOut) (2 ^ rOut)

High-demand conclusion from the optimized chord estimate and logarithmic union-bound criterion.

theorem PebblingLean.Hypercube.exists_goodCenterSample_of_bernsteinExponentialMomentBound {n N rIn rOut T : ℕ} {variance scale gap : ℝ} {eps : ℚ} (hmoment : BernsteinExponentialMomentBound n N rIn rOut T variance scale gap) (hexp : Real.exp (-bernsteinExponent variance scale gap) ≤ ↑eps) (hunion : ↑(Fintype.card (HypercubeVertex n)) * eps < 1) : ∃ (sample : CenterSample n N), IsGoodCenterList n rIn rOut T sample.toList

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_of_bernsteinExponentialMomentBound {n N rIn rOut T : ℕ} {variance scale gap : ℝ} {eps : ℚ} (hmoment : BernsteinExponentialMomentBound n N rIn rOut T variance scale gap) (hexp : Real.exp (-bernsteinExponent variance scale gap) ≤ ↑eps) (hunion : ↑(Fintype.card (HypercubeVertex n)) * eps < 1) : Pebbling.HasSolvableAtMostSize (graph n) T (N * 2 ^ rOut)

theorem PebblingLean.Hypercube.exists_goodCenterSample_of_oneCenterDistanceSum {n N rIn rOut T : ℕ} {lam variance scale gap : ℝ} {eps : ℚ} (hbound : OneCenterDistanceSumExponentialMomentBound n N rIn rOut T lam (Real.exp (-bernsteinExponent variance scale gap))) (hexp : Real.exp (-bernsteinExponent variance scale gap) ≤ ↑eps) (hunion : ↑(Fintype.card (HypercubeVertex n)) * eps < 1) : ∃ (sample : CenterSample n N), IsGoodCenterList n rIn rOut T sample.toList

theorem PebblingLean.Hypercube.hasSolvableAtMostSize_of_oneCenterDistanceSum {n N rIn rOut T : ℕ} {lam variance scale gap : ℝ} {eps : ℚ} (hbound : OneCenterDistanceSumExponentialMomentBound n N rIn rOut T lam (Real.exp (-bernsteinExponent variance scale gap))) (hexp : Real.exp (-bernsteinExponent variance scale gap) ≤ ↑eps) (hunion : ↑(Fintype.card (HypercubeVertex n)) * eps < 1) : Pebbling.HasSolvableAtMostSize (graph n) T (N * 2 ^ rOut)