OAI/Probability/SKGap/Localization/LiteralConstruction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.literalBudget_exists line 14
2. lemma OAI.SKGapCutoff.Recipe.literal_system_extension line 35
3. theorem OAI.SKGapCutoff.Recipe.literal_implicit_construction line 60
4. lemma OAI.SKGapCutoff.Recipe.initialU_size line 94
5. lemma OAI.SKGapCutoff.Recipe.initialP_size line 100
6. def OAI.SKGapCutoff.Recipe.literalSizeBudget line 112
7. lemma OAI.SKGapCutoff.Recipe.literal_initial_size line 118