Weight functions

The lower-bound argument is organized around the standard pebbling weight function: a pebble at distance d from a target contributes 2^{-d}.

noncomputable def PebblingLean.Pebbling.unitWeight {V : Type u} (dist : V → V → ℕ) (target u : V) : ℚ

Contribution of a single pebble at u to the weight with target target.

Equations

• PebblingLean.Pebbling.unitWeight dist target u = 1 / 2 ^ dist u target

noncomputable def PebblingLean.Pebbling.weight {V : Type u} [Fintype V] (dist : V → V → ℕ) (D : Pebbling V) (target : V) : ℚ

Weight of a pebbling distribution with respect to a target, using a supplied distance function.

Equations

• PebblingLean.Pebbling.weight dist D target = ∑ u : V, ↑(D u) * PebblingLean.Pebbling.unitWeight dist target u

@[simp]

theorem PebblingLean.Pebbling.weight_zero {V : Type u} [Fintype V] (dist : V → V → ℕ) (target : V) : weight dist (fun (x : V) => 0) target = 0

theorem PebblingLean.Pebbling.sum_moveDistribution_mul {V : Type u} [Fintype V] [DecidableEq V] (D : Pebbling V) (w : V → ℚ) {u v : V} (huv : u ≠ v) (hD : 2 ≤ D u) : ∑ x : V, ↑(D.moveDistribution u v x) * w x = ∑ x : V, ↑(D x) * w x - 2 * w u + w v

Algebraic effect of one legal move on a weighted sum.

theorem PebblingLean.Pebbling.weight_moveDistribution {V : Type u} [Fintype V] [DecidableEq V] (dist : V → V → ℕ) (D : Pebbling V) {u v target : V} (huv : u ≠ v) (hD : 2 ≤ D u) : weight dist (D.moveDistribution u v) target = weight dist D target - 2 * unitWeight dist target u + unitWeight dist target v

Exact change in target weight under one legal move.

theorem PebblingLean.Pebbling.unitWeight_le_two_mul_of_dist_le_succ {V : Type u} (dist : V → V → ℕ) {u v target : V} (h : dist u target ≤ dist v target + 1) : unitWeight dist target v ≤ 2 * unitWeight dist target u

If moving from u to v moves at most one step closer to the target, then the new pebble at v contributes no more weight than the two pebbles removed from u.

theorem PebblingLean.Pebbling.weight_moveDistribution_le {V : Type u} [Fintype V] [DecidableEq V] (dist : V → V → ℕ) (D : Pebbling V) {u v target : V} (huv : u ≠ v) (hD : 2 ≤ D u) (hdist : dist u target ≤ dist v target + 1) : weight dist (D.moveDistribution u v) target ≤ weight dist D target

A single legal move cannot increase target weight, provided the supplied distance function changes by at most one along graph edges.

theorem PebblingLean.Pebbling.weight_move_le_of_dist {V : Type u} [Fintype V] [DecidableEq V] (G : Graph V) (dist : V → V → ℕ) {D E : Pebbling V} {target : V} (hmove : Move G D E) (hdist : ∀ {u v : V}, G.Adj u v → dist u target ≤ dist v target + 1) : weight dist E target ≤ weight dist D target

Relational version of weight_moveDistribution_le for Move.

theorem PebblingLean.Pebbling.weight_reaches_le_of_dist {V : Type u} [Fintype V] [DecidableEq V] (G : Graph V) (dist : V → V → ℕ) {D E : Pebbling V} {target : V} (hreach : Reaches G D E) (hdist : ∀ {u v : V}, G.Adj u v → dist u target ≤ dist v target + 1) : weight dist E target ≤ weight dist D target

A sequence of legal moves cannot increase target weight.

theorem PebblingLean.Pebbling.one_le_weight_of_canReach {V : Type u} [Fintype V] [DecidableEq V] (G : Graph V) (dist : V → V → ℕ) {D : Pebbling V} {target : V} (hcan : CanReach G D target) (hdist_self : dist target target = 0) (hdist_edge : ∀ {u v : V}, G.Adj u v → dist u target ≤ dist v target + 1) : 1 ≤ weight dist D target

If a reachable distribution has a pebble on the target, then its target weight is at least one.