OAI/Probability/SKGap/Main.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.FullMain.whp_of_measurable_full line 39
2. lemma OAI.SKGap.FullMain.weighted_accuracy line 48
3. lemma OAI.SKGap.FullMain.exponential_pair_eventually line 60
4. theorem OAI.SKGap.FullMain.quenched_poincare line 75
5. theorem OAI.SKGap.sk_main line 112

   Distinct definitions of this name: ComparatorChallenges/SKHighTemperature.lean:70 (same statement text; different proof or body). Qualify references as OAI.SKGap.sk_main@path.