OAI/Combinatorics/ContingencyTables/Dense/CheegerPositive.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy bound for functions supported on half the mass

  1. lemma OAI.ContingencyTables.CheegerProof.weighted_cauchy line 11
  2. lemma OAI.ContingencyTables.CheegerProof.sum_pair_squares line 26
  3. lemma OAI.ContingencyTables.CheegerProof.sum_pair_add_square_le line 37
  4. theorem OAI.ContingencyTables.CheegerProof.positive_energy line 50