OAI/Combinatorics/Progressions/Lattices/SharedFreeAffineBudget.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.affineRecoveryLogLoss line 13
  2. theorem OAI.Erdos3.exp_neg_affineRecoveryLogLoss_card_le line 17
  3. def OAI.Erdos3.properAffineRankBound line 65
  4. def OAI.Erdos3.properAffineVolumeLog line 68
  5. def OAI.Erdos3.properAffineScaleLog line 71
  6. def OAI.Erdos3.properAffineRecoveryLogLoss line 74
  7. theorem OAI.Erdos3.affineBoxScale_le_exp line 77
  8. theorem OAI.Erdos3.affineBoxCellCount_le_exp line 119
  9. theorem OAI.Erdos3.properAffineVolume_bound line 134
  10. theorem OAI.Erdos3.properAffineSelection_bounds line 146
  11. theorem OAI.Erdos3.exists_quadratic_affine_budget line 196
  12. theorem OAI.Erdos3.exists_sharedFreeProperAffineSelection_bound line 270
  13. theorem OAI.Erdos3.exists_sharedFreeAffineSelection_bound line 363
  14. theorem OAI.Erdos3.exists_sharedFreeAffineUniform_bound line 411
  15. def OAI.Erdos3.sharedFreeAffineConstant line 434
  16. theorem OAI.Erdos3.sharedFreeAffineConstant_two_le line 438
  17. theorem OAI.Erdos3.sharedFreeAffineConstant_shift_bound line 443
  18. theorem OAI.Erdos3.sharedFreeAffineConstant_spec line 453
  19. theorem OAI.Erdos3.sharedFreeAffineConstant_proper_spec line 470
  20. theorem OAI.Erdos3.sharedFreeRecoveryThreshold_coefficient_bounds line 483