Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite stationary Markov operators contract in weighted L2

Statement

Let (X,P,π) be a finite reversible chain and let f:X→C. Define ∥f∥2,π2:=∑xπx∣fx∣2 and (Pf)x:=∑yPxyfy. Then

∥Pf∥2,π2≤∥f∥2,π2,

so P is a contraction on the finite weighted inner-product space L2(X,π). Detailed balance is not needed for this inequality beyond the stated stationary-law hypotheses.

Facts & Assumptions

Given: A finite reversible chain (X,P,π), where πx>0, ∑xπx=1, πP=π, and Pxy≥0 with ∑yPxy=1, and a function f:X→C.

[F1]

Finite reversible Markov chain with positive stationary law: P is row-stochastic and πP=π with every πx>0.

Proof

1.1givenF1algebra

For each x, set mx:=∑yPxyfy. Expanding the nonnegative sum gives ∑yPxy∣fy−mx∣2=∑yPxy∣fy∣2−∣mx∣2≥0, because the row weights sum to one. Thus ∣mx∣2≤∑yPxy∣fy∣2.

2.1F1step 1.1algebra

Multiply the inequality in step 1.1 by πx and sum over x. All sums are finite, so reindexing gives ∑xπx∣mx∣2≤∑y(∑xπxPxy)∣fy∣2=∑yπy∣fy∣2 by stationarity.

3.1F1step 2.1algebra∎

The left and right sides in step 2.1 are ∥Pf∥2,π2 and ∥f∥2,π2 by definition; taking nonnegative square roots proves the contraction claim. Positivity of every πx makes the weighted form positive definite.

Depends on

Used by

Dependency tree · two levels

9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources