OAI/Combinatorics/IndependentSets/Reduction/PairEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LargeIndependentSets.ProductAveraging.pair_energy_eq line 10
2. lemma OAI.LargeIndependentSets.ProductAveraging.average_depends line 35
3. lemma OAI.LargeIndependentSets.ProductAveraging.average_update_of_notMem line 47
4. lemma OAI.LargeIndependentSets.ProductAveraging.junta_variance_bound line 54
5. lemma OAI.LargeIndependentSets.ProductAveraging.exists_influence_of_junta line 106
6. lemma OAI.LargeIndependentSets.ProductAveraging.influential_card_le line 137