The AHL weighted AM–GM and the degree convexity — nodes W6–W8 #
This file lands nodes W6–W8 of the Alon–Hoory–Linial irregular-Moore walk-count proof, the
analytic heart of the ladder. Building on the exact weighted marginals of AHL.AHLMarginals
(nbWeightTotal_eq = D, nbEndWeight_eq_degree = deg v) and the walk-weight vocabulary of
AHL.AHLStationary, it packages the three moves that turn the degree-bias identity into the
average-degree walk-count lower bound.
Contents #
- W6 — the entropy recursion.
nbEntropy G k = ∑_{walks} wt·log wt⁻¹. Its exact one-step recursionnbEntropy_succ(T_{k+1} = T_k + ∑_v deg v · log(deg v − 1)) collapses via the end marginal (W4) to the closed formnbEntropy_eq : nbEntropy G ℓ = (ℓ − 1)·∑_v deg v·log(deg v − 1). - W7 — the single AM–GM (
nb_amgm). One application ofReal.geom_mean_le_arith_mean_weightedwith weightswt/Dand valuesD/wtgivesD·exp(nbEntropy G k / D) ≤ mₖ, the geometric-mean lower bound on the walk count. Repackaged in the sharpΛ-formnb_amgm_lambda(D·Λ^(ℓ−1) ≤ mₗ,Λ = ∏_v (deg v − 1)^(deg v/D), AHL Note 3). - W8 — the degree convexity (
sum_deg_mul_log_ge,lambda_ge). The functionx ↦ x·log(x − 1)is convex on[2, ∞)(convexOn_deg_mul_log,f'' = (x−2)/(x−1)² ≥ 0); Jensen with uniform weights1/nat the degrees yieldsD·log((D − n)/n) ≤ ∑_v deg v·log(deg v − 1), i.e.Λ ≥ (D − n)/n = d_avg − 1.
W8 — the degree convexity #
The AHL convexity (W8 core). The function φ(x) = x·log(x − 1) is convex on [2, ∞).
Its second derivative is φ''(x) = (x − 2)/(x − 1)² ≥ 0 there; we feed the explicit first and
second
derivatives to convexOn_of_hasDerivWithinAt2_nonneg.
W8 — the degree-log Jensen bound. Under δ ≥ 2, the average d_avg = D/n satisfies
D·log((D − n)/n) ≤ ∑_v deg v·log(deg v − 1). Jensen's inequality (ConvexOn.map_sum_le) for the
convex φ(x) = x·log(x − 1) with uniform weights 1/n at the degrees d_v ∈ [2, ∞) and center
d_avg ∈ [2, ∞); multiplying through by n. This is the Λ ≥ d_avg − 1 step
in logarithmic form.
W6 — the entropy recursion #
The AHL walk entropy (W6). T_k = ∑_{length-k walks} wt·log wt⁻¹, the finite-sum stand-in
for the entropy of the non-returning walk distribution. Its exact one-step recursion is the engine
of the AM–GM lower bound.
Equations
- ACMax.nbEntropy G k = ∑ t ∈ ACMax.nbAll k, ACMax.nbWeight t.snd * Real.log (ACMax.nbWeight t.snd)⁻¹
Instances For
The weight of a one-edge extension. Every non-backtracking extension s of a non-nil
prefix
s' has weight wt(s') · (deg (end s') − 1)⁻¹ — the new intermediate vertex is the old endpoint.
Immediate from nbWeight_concat.
The entropy as a sum over starts. nbEntropy regroups Finset.sum_sigma'-style as the
double sum over the start x and the length-k non-backtracking walks from x.
Base case (W6). T₁ = 0: every length-1 walk has weight 1 and log 1⁻¹ = 0.
The per-prefix entropy fiber. Summing wt·log wt⁻¹ over the deg (end s') − 1
extensions of
a non-nil prefix s' gives wt(s')·log wt(s')⁻¹ + wt(s')·log(deg (end s') − 1): each extension has
the same weight wt(s')·(deg − 1)⁻¹, and the mass cancels the multiplicity, leaving the prefix mass
scaled by the log-of-degree increment.
The degree-log marginal collapse. Summing wt·log(deg (end) − 1) over all length-k
non-backtracking walks partitions by the endpoint and applies the end marginal nbEndWeight = deg v
(W4), giving ∑_v deg v · log(deg v − 1).
The entropy recursion (W6, II′). T_{k+1} = T_k + ∑_v deg v · log(deg v − 1) for k ≥ 1.
Each length-k walk spawns deg (end) − 1 extensions whose fiber contributes its own entropy plus
the degree-log increment (fiber_entropy); the increment collapses to the degree sum
(sum_weight_log_deg).
The entropy closed form (W6). For ℓ ≥ 1, T_ℓ = (ℓ − 1)·∑_v deg v · log(deg v − 1) —
telescoping the recursion nbEntropy_succ from the T₁ = 0 base.
W7 — the single AM–GM #
The walk finset cardinality. |nbAll k| = mₖ, the total length-k non-backtracking walk
count (Finset.card_sigma + card_nbWalksFrom).
W7 — the AM–GM lower bound (IV′). Under δ ≥ 2 (and V nonempty), the total walk count
dominates the geometric mean: D·exp(T_k / D) ≤ mₖ. One application of
Real.geom_mean_le_arith_mean_weighted with weights wt/D (summing to 1 by nbWeightTotal_eq)
and values D/wt: the arithmetic side telescopes to ∑ 1 = mₖ, and the geometric side is
∏ (D/wt)^{wt/D} = exp(log D + T_k / D) = D·exp(T_k / D).
The sharp Λ-form (AHL Note 3) #
The AHL spectral constant Λ = ∏_v (deg v − 1)^(deg v / D) (Real.rpow), the geometric
mean
of deg v − 1 weighted by the stationary degree measure deg v / D. Keeping this form exposed (as
AHL Note 3 recommends) gives the sharper Moore rung n ≥ n₀(Λ + 1, g).
Instances For
Λ > 0. Each factor (deg v − 1)^{…} is positive under δ ≥ 2.
log Λ in closed form. log Λ = (∑_v deg v · log(deg v − 1)) / D — the exponent collapse
log((deg v − 1)^{deg v / D}) = (deg v / D)·log(deg v − 1).
W7 (sharp Λ-form). Under δ ≥ 2 (and V nonempty), D·Λ^(ℓ−1) ≤ mₗ for ℓ ≥ 1.
Repackaging nb_amgm via Λ^(ℓ−1) = exp((ℓ−1)·log Λ) = exp(T_ℓ / D) (nbEntropy_eq, log_Lambda,
Real.rpow_def_of_pos).
W8 (sharp Λ-form). Under δ ≥ 2, Λ ≥ (D − n)/n = d_avg − 1. Exponentiating the
logarithmic
Jensen bound sum_deg_mul_log_ge: log((D − n)/n) ≤ (∑_v deg v · log(deg v − 1))/D = log Λ.