OAI/Combinatorics/Progressions/Dynamics/ModeThresholdLogBudget.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.add_le_exp_add_one line 13
  2. theorem OAI.Erdos3.sum_le_exp_card_add_sum line 23
  3. theorem OAI.Erdos3.coe_toNNReal_le_exp line 37
  4. def OAI.Erdos3.physicalIdealErrorShare line 50
  5. theorem OAI.Erdos3.physicalIdealErrorShare_pos line 53
  6. theorem OAI.Erdos3.physicalIdealErrorShare_le_one line 56
  7. theorem OAI.Erdos3.physicalIdealErrorShare_inv line 61
  8. theorem OAI.Erdos3.exp_mul_physicalIdealErrorShare line 65
  9. theorem OAI.Erdos3.physicalIdealErrorShare_half_inverse_le line 71
  10. theorem OAI.Erdos3.physicalIdealErrorShare_scale_mesh line 80
  11. theorem OAI.Erdos3.physicalIdeal_three_errors_le line 92
  12. theorem OAI.Erdos3.algebraicMajor_mass_le_exp line 137
  13. theorem OAI.Erdos3.algebraicMajor_denominator_le_exp line 159
  14. theorem OAI.Erdos3.exists_algebraicMajor_output_budget line 171
  15. def OAI.Erdos3.modeProfileBound line 203
  16. def OAI.Erdos3.modeProfileLog line 205
  17. theorem OAI.Erdos3.modeProfileLog_nonneg line 207
  18. theorem OAI.Erdos3.modeRemovalConstants_le_exp line 211
  19. theorem OAI.Erdos3.modeRemovalMesh_inv_le_exp line 238
  20. theorem OAI.Erdos3.modeRemovalRadius_inv_le_exp line 250
  21. def OAI.Erdos3.multiaffineInverseConstant line 276
  22. def OAI.Erdos3.multiaffineInverseExponent line 279
  23. def OAI.Erdos3.finiteLayerInverseConstant line 281
  24. def OAI.Erdos3.finiteLayerInverseExponent line 283
  25. def OAI.Erdos3.finiteLayerInverseLog line 285
  26. theorem OAI.Erdos3.multiaffineBiasBudget_eq_inverse_power line 288
  27. theorem OAI.Erdos3.multiaffineBiasBudget_le_exp line 295
  28. theorem OAI.Erdos3.finiteLayerInverseLog_nonneg line 307
  29. theorem OAI.Erdos3.finiteLayerBiasBudget_le_exp line 310
  30. theorem OAI.Erdos3.modeRemovalBeta_inv_le_exp line 328
  31. theorem OAI.Erdos3.modeRemovalBias_inv_le_exp line 343
  32. def OAI.Erdos3.modeBiasLog line 358
  33. def OAI.Erdos3.modeShrinkLog line 361
  34. def OAI.Erdos3.modeSideLog line 364
  35. theorem OAI.Erdos3.modeBiasLog_nonneg line 367
  36. theorem OAI.Erdos3.modeShrinkLog_nonneg line 370
  37. theorem OAI.Erdos3.modeSideLog_nonneg line 375
  38. theorem OAI.Erdos3.chosenBiasBudget_le_exp line 382
  39. theorem OAI.Erdos3.modeRemovalShrink_le_exp line 388
  40. theorem OAI.Erdos3.modeRemovalSideThreshold_le_exp line 410