Upper-bound scaffolding #

This file records the definitions and elementary lemmas used by the probabilistic high-demand part of the upper bound. The probabilistic estimates themselves are not asserted here; they will be formalized as separate lemmas.

source

def PebblingLean.Hypercube.annulus (n rIn rOut : ℕ) (target : HypercubeVertex n) :

Finset (HypercubeVertex n)

Centers whose distance from target lies between the inner and outer radii.

Equations

PebblingLean.Hypercube.annulus n rIn rOut target = {center : PebblingLean.HypercubeVertex n | rIn ≤ PebblingLean.Hypercube.dist center target ∧ PebblingLean.Hypercube.dist center target ≤ rOut}

Instances For

source

@[simp]

theorem PebblingLean.Hypercube.mem_annulus {n rIn rOut : ℕ} {target center : HypercubeVertex n} :

center ∈ annulus n rIn rOut target ↔ rIn ≤ dist center target ∧ dist center target ≤ rOut

source

def PebblingLean.Hypercube.annulusContribution {n : ℕ} (rIn rOut : ℕ) (target center : HypercubeVertex n) :

ℕ

Contribution of one stack of size 2^rOut at center toward target, counting only centers in the annulus.

Equations

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

Instances For

source

theorem PebblingLean.Hypercube.annulusContribution_eq_of_mem {n rIn rOut : ℕ} {target center : HypercubeVertex n} (hmem : center ∈ annulus n rIn rOut target) :

annulusContribution rIn rOut target center = 2 ^ (rOut - dist center target)

source

theorem PebblingLean.Hypercube.annulusContribution_eq_zero_of_notMem {n rIn rOut : ℕ} {target center : HypercubeVertex n} (hmem : center ∉ annulus n rIn rOut target) :

annulusContribution rIn rOut target center = 0

source

theorem PebblingLean.Hypercube.annulusContribution_le_stackSize {n rIn rOut : ℕ} (target center : HypercubeVertex n) :

annulusContribution rIn rOut target center ≤ 2 ^ rOut

One annulus contribution is bounded by the stack size 2^rOut.

source

theorem PebblingLean.Hypercube.annulusContribution_le_width {n rIn rOut : ℕ} (target center : HypercubeVertex n) :

annulusContribution rIn rOut target center ≤ 2 ^ (rOut - rIn)

If the center is counted, the annulus contribution is bounded by the width of the annulus rather than by the full stack size.

source

theorem PebblingLean.Hypercube.annulusContribution_sq_le_width_mul {n rIn rOut : ℕ} (target center : HypercubeVertex n) :

annulusContribution rIn rOut target center ^ 2 ≤ 2 ^ (rOut - rIn) * annulusContribution rIn rOut target center

The square bound used in the Bernstein step: Z^2 ≤ B_0 Z, where B_0 = 2^(rOut-rIn) is the annulus-width contribution bound.

source

def PebblingLean.Hypercube.annulusTotalContribution {n : ℕ} (rIn rOut : ℕ) (target : HypercubeVertex n) (centers : List (HypercubeVertex n)) :

ℕ

The total annulus contribution of a finite list of centers to a fixed target. This is the Lean version of X_t in the proof.

Equations

PebblingLean.Hypercube.annulusTotalContribution rIn rOut target centers = (List.map (PebblingLean.Hypercube.annulusContribution rIn rOut target) centers).sum

Instances For

source

def PebblingLean.Hypercube.HasHighDemandDistribution (n T costBound minPile : ℕ) :

Prop

The high-demand conclusion used as a target for the probabilistic lemma: a T-solvable distribution whose size is bounded and whose occupied piles are large.

Equations

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

Instances For

source

theorem PebblingLean.Hypercube.HasHighDemandDistribution.to_hasSolvableAtMostSize {n T costBound minPile : ℕ} (h : HasHighDemandDistribution n T costBound minPile) :

Pebbling.HasSolvableAtMostSize (graph n) T costBound

source

theorem PebblingLean.Hypercube.HasHighDemandDistribution.to_ordinary_hasSolvableAtMostSize {n T costBound minPile : ℕ} (hT : 1 ≤ T) (h : HasHighDemandDistribution n T costBound minPile) :

Pebbling.HasSolvableAtMostSize (graph n) 1 costBound

source

theorem PebblingLean.Hypercube.HasHighDemandDistribution.mono_cost {n T costBound costBound' minPile : ℕ} (hcost : costBound ≤ costBound') (h : HasHighDemandDistribution n T costBound minPile) :

HasHighDemandDistribution n T costBound' minPile

source

theorem PebblingLean.Hypercube.HasHighDemandDistribution.mono_minPile {n T costBound minPile minPile' : ℕ} (hminPile : minPile' ≤ minPile) (h : HasHighDemandDistribution n T costBound minPile) :

HasHighDemandDistribution n T costBound minPile'

source

theorem PebblingLean.Hypercube.HasHighDemandDistribution.mono {n T costBound costBound' minPile minPile' : ℕ} (hcost : costBound ≤ costBound') (hminPile : minPile' ≤ minPile) (h : HasHighDemandDistribution n T costBound minPile) :

HasHighDemandDistribution n T costBound' minPile'

source

def PebblingLean.Hypercube.constantDistribution (n S : ℕ) :

Pebbling (HypercubeVertex n)

The constant distribution with S pebbles on every vertex.

Equations