OAI/Combinatorics/ContingencyTables/Dense/FiniteCheegerProof.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Discharging the finite-chain Cheeger input by coarea and a weighted median

  1. lemma OAI.ContingencyTables.CheegerProof.split_square line 12
  2. lemma OAI.ContingencyTables.CheegerProof.split_difference line 19
  3. theorem OAI.ContingencyTables.CheegerProof.finiteCheeger line 42

    Source documentation

    Levin–Peres Theorem 13.10 lower bound, in the exact finite Poincaré form used here.

    theorem finiteCheeger : PublishedInputs.FiniteCheeger X := by
…

    Mentions: OAI.ContingencyTables.PublishedInputs.FiniteCheeger