Lemma 3.2 — contraction of total variation
ProvedInducedExpanderTest989.Structural.lemma_3_2graph-theorymarkov-chainp2o-batch-stoc27ap2o-gran-per-chapterp2o-plan-paperp2o-v1property-testing
Let K be a stochastic matrix on a finite state space and let a be any real row vector, with total variation norm half its ℓ¹ norm. Then
No positivity or normalization of a is assumed. This transfers endpoint comparisons through a common transition kernel.
Differences from the source:
- encoding: finite stochastic matrix and row-vector total variation → Mathlib rowStochastic, Matrix powers and MarkovChain.tvDist; reason: the existing finite-chain definitions use the same row convention and add no irreducibility assumption
Preamble
import Mathlib import Definitions.Def_InducedExpanderTest989_Structural_Algorithm set_option autoImplicit false open scoped BigOperators ENNReal NNReal noncomputable section
Formal statement
namespace InducedExpanderTest989.Structural
theorem lemma_3_2 {X : Type} [Fintype X] [DecidableEq X]
(K : Matrix X X ℝ) (hK : Stochastic K) (a : X → ℝ) :
tvNorm (Matrix.vecMul a K) ≤ tvNorm a := by sorry
end InducedExpanderTest989.Structural
Source
Pan Peng, Ranran Shen, Testing for a Large Induced Expander: Sublinear Algorithms and Query Lower Bounds, STOC 2027 submission #989 (October 2026), source.pdf SHA-256 98b4035a0ac121d1c1bfb6abdeb3cdb6cf3304ef3cb21b2cd58c97e4bbce6334, p.14 (PDF p.16), Lemma 3.2; https://github.com/sigact-stoc/stoc2027/releases/download/papers-2/989.pdf
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.