OAI/Probability/SKGap/Localization/LocalResidualInduction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.LocalRecipeResidualRule line 22
2. lemma OAI.SKGapCutoff.Recipe.FiniteLocalRecipeControl.local_onsager_multiplier line 29
3. lemma OAI.SKGapCutoff.Recipe.local_residual_rule_base line 38
4. lemma OAI.SKGapCutoff.Recipe.local_residual_rule_step line 50
5. theorem OAI.SKGapCutoff.Recipe.local_uniform_residual_rule line 162
6. theorem OAI.SKGapCutoff.Recipe.uniform_local_weak_residual line 182