OAI/Probability/SKGap/Localization/SmoothSelection.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.Recipe.residualScalarCutoff line 14
  2. lemma OAI.SKGapCutoff.Recipe.residualScalarCutoff_bounds line 17
  3. lemma OAI.SKGapCutoff.Recipe.residualScalarCutoff_one line 23
  4. lemma OAI.SKGapCutoff.Recipe.residualScalarCutoff_zero line 28
  5. lemma OAI.SKGapCutoff.Recipe.residualScalarCutoff_smooth line 31
  6. lemma OAI.SKGapCutoff.Recipe.residualScalarCutoff_lipschitz line 35
  7. lemma OAI.SKGapCutoff.Recipe.norm_derivativeVector_sq line 45
  8. lemma OAI.SKGapCutoff.Recipe.derivativeVector_norm_mono line 49
  9. lemma OAI.SKGapCutoff.Recipe.derivativeVector_comp_lipschitz line 58
  10. lemma OAI.SKGapCutoff.Recipe.derivativeVector_scale line 67
  11. lemma OAI.SKGapCutoff.Recipe.residualEnergy_as_pair line 73
  12. lemma OAI.SKGapCutoff.Recipe.residualEnergy_gradient line 79
  13. def OAI.SKGapCutoff.Recipe.residualStepCutoff line 103
  14. def OAI.SKGapCutoff.Recipe.residualCutoff line 106
  15. lemma OAI.SKGapCutoff.Recipe.residualStepCutoff_bounds line 109
  16. lemma OAI.SKGapCutoff.Recipe.residualCutoff_bounds line 111
  17. lemma OAI.SKGapCutoff.Recipe.residualStepCutoff_support line 117
  18. lemma OAI.SKGapCutoff.Recipe.residualCutoff_support line 129
  19. lemma OAI.SKGapCutoff.Recipe.residualStepCutoff_one line 137
  20. lemma OAI.SKGapCutoff.Recipe.residualCutoff_one line 148
  21. lemma OAI.SKGapCutoff.Recipe.derivativeVector_mul_bound line 156
  22. lemma OAI.SKGapCutoff.Recipe.residualStepCutoff_gradient line 180
  23. lemma OAI.SKGapCutoff.Recipe.residualCutoff_gradient line 193