OAI/Computability/MinUncut/Analysis/GaussianPacking.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncut.GaussianBudget.productLaw line 13
2. def OAI.MinUncut.GaussianBudget.packEquiv line 17
3. lemma OAI.MinUncut.GaussianBudget.pack_preserving line 22
4. lemma OAI.MinUncut.GaussianBudget.score_packed line 27
5. lemma OAI.MinUncut.GaussianBudget.integral_pack_sign line 36
6. lemma OAI.MinUncut.GaussianBudget.first_triple_bound line 53
7. lemma OAI.MinUncut.GaussianBudget.second_triple_bound line 62