Potential

Global harmonic-potential bookkeeping

This file lifts the one-coordinate identity from FD1D.Drift to all nonroot nodes of a finite dyadic tree. The stochastic input is deliberately minimal: at a node, deletion and arrival are independent Bernoulli events with probabilities q and p. Linearity then gives the global identity; no independence between different tree nodes is needed.

One-node deletion/arrival experiment

def FD1D.bernoulliMass (r : ℝ) (outcome : Bool) : ℝ

Probability mass of a Bernoulli outcome.

Equations

• FD1D.bernoulliMass r outcome = if outcome = true then r else 1 - r

def FD1D.updateCount (N : ℕ) (deleted arrived : Bool) : ℕ

The new count after a deletion followed by an arrival. The hypotheses used below ensure that deletion has probability zero when the old count is zero.

Equations

• FD1D.updateCount N deleted arrived = if deleted = true then if arrived = true then N else N - 1 else if arrived = true then N + 1 else N

noncomputable def FD1D.expectedNodePotentialChange (a : ℝ) (N : ℕ) (p q : ℝ) : ℝ

Expected change of one harmonic potential under independent Bernoulli events.

Equations

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

theorem FD1D.expectedNodePotentialChange_eq {a p q : ℝ} {N : ℕ} (hzero : N = 0 → q = 0) : expectedNodePotentialChange a N p q = p * (1 - q) / (↑N + a + 1) - q * (1 - p) / (↑N + a)

Global potential, drift, and remainder

noncomputable def FD1D.globalHarmonicPotential (L : ℕ) (a : ℝ) (N : (d : ℕ) → DyadicNode d → ℕ) : ℝ

Phi = sum_{v ≠ root} p_v² phi(N_v).

Equations

• FD1D.globalHarmonicPotential L a N = ∑ d ∈ Finset.range L, ∑ v : FD1D.DyadicNode (d + 1), FD1D.nodeMass (d + 1) v ^ 2 * FD1D.harmonicPotential a (N (d + 1) v)

noncomputable def FD1D.potentialDrift (L : ℕ) (a : ℝ) (N : (d : ℕ) → DyadicNode d → ℕ) (q : (d : ℕ) → DyadicNode d → ℝ) : ℝ

D, with natural inventory counts coerced to reals.

Equations

• FD1D.potentialDrift L a N q = FD1D.bellmanDrift L a (fun (d : ℕ) (v : FD1D.DyadicNode d) => ↑(N d v)) q

noncomputable def FD1D.potentialRemainder (L : ℕ) (a : ℝ) (N : (d : ℕ) → DyadicNode d → ℕ) (q : (d : ℕ) → DyadicNode d → ℝ) : ℝ

The nonnegative remainder R in the exact harmonic-potential drift.

Equations

• FD1D.potentialRemainder L a N q = ∑ d ∈ Finset.range L, ∑ v : FD1D.DyadicNode (d + 1), FD1D.nodeMass (d + 1) v ^ 3 * (1 - q (d + 1) v) / ((↑(N (d + 1) v) + a) * (↑(N (d + 1) v) + a + 1))

noncomputable def FD1D.expectedGlobalPotentialChange (L : ℕ) (a : ℝ) (N : (d : ℕ) → DyadicNode d → ℕ) (q : (d : ℕ) → DyadicNode d → ℝ) : ℝ

The conditional expected global change, obtained by summing the independent one-node deletion/arrival experiment. Correlations between distinct nodes do not enter this expression.

Equations

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

theorem FD1D.expectedGlobalPotentialChange_eq_drift_sub_remainder {L : ℕ} {a : ℝ} {N : (d : ℕ) → DyadicNode d → ℕ} {q : (d : ℕ) → DyadicNode d → ℝ} (ha : 0 < a) (hzero : ∀ (d : ℕ) (v : DyadicNode d), N d v = 0 → q d v = 0) : expectedGlobalPotentialChange L a N q = potentialDrift L a N q - potentialRemainder L a N q

Exact global identity E[Delta Phi | state] = D - R.

Remainder estimates

theorem FD1D.potentialRemainder_nonneg {L : ℕ} {a : ℝ} {N : (d : ℕ) → DyadicNode d → ℕ} {q : (d : ℕ) → DyadicNode d → ℝ} (ha : 0 < a) (hq : ∀ (d : ℕ) (v : DyadicNode d), q d v ≤ 1) : 0 ≤ potentialRemainder L a N q

theorem FD1D.potentialRemainder_summand_le {a N q h p : ℝ} (hp : 0 ≤ p) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) (haN : 0 < N + a) (hmajor : p ≤ (N + a) * h) : p ^ 3 * (1 - q) / ((N + a) * (N + a + 1)) ≤ p * h ^ 2

Every summand of R is at most p_v h_v².

theorem FD1D.potentialRemainder_le_sum_hazardEnergy {L : ℕ} {a : ℝ} {N : (d : ℕ) → DyadicNode d → ℕ} {q h : (d : ℕ) → DyadicNode d → ℝ} (ha : 0 < a) (hq0 : ∀ (d : ℕ) (v : DyadicNode d), 0 ≤ q d v) (hq1 : ∀ (d : ℕ) (v : DyadicNode d), q d v ≤ 1) (hmajor : ∀ (d : ℕ) (v : DyadicNode d), nodeMass d v ≤ (↑(N d v) + a) * h d v) : potentialRemainder L a N q ≤ ∑ d ∈ Finset.range L, hazardEnergy h (d + 1)

R ≤ sum_{ell=1}^L H_ell.

theorem FD1D.sum_hazardEnergy_le_depth_mul {L : ℕ} {h : (d : ℕ) → DyadicNode d → ℝ} (hmono : Monotone (hazardEnergy h)) : ∑ d ∈ Finset.range L, hazardEnergy h (d + 1) ≤ ↑L * hazardEnergy h L

A nondecreasing hazard energy gives sum_{ell=1}^L H_ell ≤ L H_L.

theorem FD1D.potentialRemainder_bounds {L : ℕ} {a : ℝ} {N : (d : ℕ) → DyadicNode d → ℕ} {q h : (d : ℕ) → DyadicNode d → ℝ} (ha : 0 < a) (hq0 : ∀ (d : ℕ) (v : DyadicNode d), 0 ≤ q d v) (hq1 : ∀ (d : ℕ) (v : DyadicNode d), q d v ≤ 1) (hmajor : ∀ (d : ℕ) (v : DyadicNode d), nodeMass d v ≤ (↑(N d v) + a) * h d v) (hmono : Monotone (hazardEnergy h)) : 0 ≤ potentialRemainder L a N q ∧ potentialRemainder L a N q ≤ ∑ d ∈ Finset.range L, hazardEnergy h (d + 1) ∧ ∑ d ∈ Finset.range L, hazardEnergy h (d + 1) ≤ ↑L * hazardEnergy h L

Equation (10): 0 ≤ R ≤ sum H_ell ≤ L H_L.

Stationary finite laws

theorem FD1D.stationary_expect_drift_eq_remainder {α : Type u_1} [Fintype α] (μ : FiniteLaw α) (K : α → α → ℝ) (Phi D R : α → ℝ) (hrow : ∀ (x : α), ∑ y : α, K x y = 1) (hstationary : ∀ (y : α), ∑ x : α, μ.mass x * K x y = μ.mass y) (hdrift : ∀ (x : α), ∑ y : α, K x y * (Phi y - Phi x) = D x - R x) : μ.expect D = μ.expect R

Explicit finite-state stationarity: K has row sum one, mu K = mu, and its conditional potential drift is D-R. Then E_mu D = E_mu R.

Finite-time telescope

theorem FD1D.finite_time_drift_telescope (T : ℕ) (Phi D R : ℕ → ℝ) (hdrift : ∀ t < T, Phi (t + 1) - Phi t = D t - R t) : ∑ t ∈ Finset.range T, D t = ∑ t ∈ Finset.range T, R t + Phi T - Phi 0

Exact summation of the one-step expected drift identities.

theorem FD1D.finite_time_hazard_drift_inequality {T : ℕ} {a L c B : ℝ} (Phi D R H : ℕ → ℝ) (hT : 0 < T) (hdrift : ∀ t < T, Phi (t + 1) - Phi t = D t - R t) (hD : ∀ t < T, a * (H t / 100 - c) ≤ D t) (hR : ∀ t < T, R t ≤ L * H t) (hPhi0 : 0 ≤ Phi 0) (hPhiT : Phi T ≤ B) : (a / 100 - L) * ((∑ t ∈ Finset.range T, H t) / ↑T) ≤ a * c + B / ↑T

The finite-T inequality used in Section 5. Here Phi, D, R, and H are already expectations at time t; the preceding theorem supplies their telescoped drift equation.