OAI/Probability/SKGap/Localization/PrimaryLocalInput.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.Primary.averageBudget line 14
  2. lemma OAI.SKGapCutoff.Primary.averageBudget_nonneg line 18
  3. def OAI.SKGapCutoff.Primary.localPrimaryBudget line 24
  4. lemma OAI.SKGapCutoff.Primary.localPrimaryBudget_nonneg line 26
  5. lemma OAI.SKGapCutoff.Primary.localPrimaryBudget_bounds line 30
  6. lemma OAI.SKGapCutoff.Primary.onsager_derivative_bound line 40
  7. lemma OAI.SKGapCutoff.Primary.derivativeVector_mul_sub line 59
  8. theorem OAI.SKGapCutoff.Primary.primary_local_input line 66
  9. lemma OAI.SKGapCutoff.Recipe.FiniteRecipeControl.onsager_multiplier line 111
  10. lemma OAI.SKGapCutoff.Recipe.uniform_normalized_pair line 120
  11. lemma OAI.SKGapCutoff.Recipe.uniform_prev_zero line 128
  12. def OAI.SKGapCutoff.Recipe.RecipeResidualRule line 150
  13. lemma OAI.SKGapCutoff.Recipe.residual_rule_base line 156
  14. lemma OAI.SKGapCutoff.Recipe.residual_rule_step line 168