OAI/Combinatorics/Progressions/Estimates/JointBooleanRegularization.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.sigmaAxisOperatorMap line 16
  2. theorem OAI.Erdos3.sigmaAxisOperatorMap_apply line 33
  3. theorem OAI.Erdos3.sigmaAxisOperatorMap_norm_le_one line 36
  4. theorem OAI.Erdos3.sigmaAxisFamily_fderiv_norm_le line 43
  5. theorem OAI.Erdos3.sigmaAxisOperatorFamily_fderiv_norm_le line 62
  6. theorem OAI.Erdos3.sigmaAxisSampler_selected_fderiv_norm_le line 84
  7. theorem OAI.Erdos3.jointBoolean_selected_inverse_bound line 113
  8. theorem OAI.Erdos3.jointBoolean_selected_derivative_bound line 144
  9. theorem OAI.Erdos3.regularizedImageMap_mappedTest line 171
  10. theorem OAI.Erdos3.regularizedImageMap_error line 181
  11. theorem OAI.Erdos3.regularizedImageDensity_test_error line 211
  12. theorem OAI.Erdos3.jointBoolean_selected_inverse_perturbation line 238
  13. theorem OAI.Erdos3.jointBoolean_divergence_bound line 278
  14. theorem OAI.Erdos3.cutoff_translation_error line 335
  15. theorem OAI.Erdos3.regularizedImageDensity_cutoff_error line 354
  16. theorem OAI.Erdos3.regularizedImageDensity_test_integral line 376
  17. theorem OAI.Erdos3.regularizedImageDensity_translate_test line 386
  18. theorem OAI.Erdos3.regularizedImageDensity_translate_error line 396
  19. theorem OAI.Erdos3.jointBooleanGoodWeight_translation_bound line 422
  20. def OAI.Erdos3.jointBooleanTranslationBudget line 490
  21. theorem OAI.Erdos3.jointBooleanGoodWeight_translation_budget line 500
  22. theorem OAI.Erdos3.jointBooleanCutoff_loss line 528
  23. theorem OAI.Erdos3.jointBoolean_regularization_error line 557