PublishedCheeger.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The published finite-chain Cheeger input

Levin and Peres, Markov Chains and Mixing Times, second edition (2017), Theorem 13.10, equation (13.6), lower bound, together with the variational characterization in Lemma 13.7. The theorem is attributed there to Sinclair and Jerrum (1989) and Lawler and Sokal (1988). Source: https://pages.uoregon.edu/dlevin/MARKOV/markovmixing.pdf

The finite reversible lazy-chain Poincaré consequence is expressed using stationary cut flow and the symmetric Dirichlet energy.

def OAI.ContingencyTables.PublishedInputs.FiniteCheeger line 30
Source documentation
The smallest Cheeger consequence needed here. The cut inequality uses unnormalized stationary flow across each cut once; energy includes the usual factor one half in its symmetric pair-sum formula.
```
def FiniteCheeger : Prop :=
…
```