OAI/Combinatorics/Progressions/Estimates/ScalarDominatedSlack.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_comm line 17
  2. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_sum line 29
  3. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_sub line 36
  4. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_mul_const line 40
  5. theorem OAI.Erdos3.productMean_coordinateSwap line 49
  6. theorem OAI.Erdos3.productMean_coordinateMix line 67
  7. theorem OAI.Erdos3.FiniteProbabilityWeights.exists_code_fiber_mass line 84
  8. theorem OAI.Erdos3.FiniteProbabilityWeights.retain_simultaneous_mean_error line 106
  9. theorem OAI.Erdos3.FiniteProbabilityWeights.retain_simultaneous_small_mean_error line 137
  10. theorem OAI.Erdos3.exists_weighted_exponential_constant_fiber line 157
  11. theorem OAI.Erdos3.exists_linear_model_partner line 210
  12. theorem OAI.Erdos3.exists_fixed_linear_model_partners line 229
  13. theorem OAI.Erdos3.fixedParameter_observed_tail_of_tests line 286
  14. theorem OAI.Erdos3.fixedParameter_observed_tail_exp line 312
  15. theorem OAI.Erdos3.fixedParameter_observed_tail_dominated line 329
  16. theorem OAI.Erdos3.FiniteProbabilityWeights.uniform_injective_mean_le line 358
  17. theorem OAI.Erdos3.FiniteProbabilityWeights.uniform_base_reweight_test_le line 373
  18. theorem OAI.Erdos3.FiniteProbabilityWeights.siteLaw_excessMass_le_of_test_bound line 403
  19. theorem OAI.Erdos3.fixedParameter_scalar_tail_mono_slack line 431
  20. theorem OAI.Erdos3.fixedParameter_scalar_tail_dominated_slack line 455