OAI/NumberTheory/Jacobsthal/Estimates/SourceSamplePopulation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosInverseSampling.sampleAverage line 14
  2. theorem OAI.Erdos970.ErdosInverseSampling.sample_product_sum_le line 17
  3. theorem OAI.Erdos970.ErdosInverseSampling.sample_product_average_le line 35
  4. theorem OAI.Erdos970.ErdosInverseSampling.normalized_falling_eq_product line 58
  5. theorem OAI.Erdos970.ErdosInverseSampling.normalized_falling_tendsto line 70
  6. theorem OAI.Erdos970.ErdosInverseSampling.sampling_prefactor_tendsto line 82
  7. theorem OAI.Erdos970.ErdosInverseSampling.sampling_prefactor_eventually_le_two line 87
  8. theorem OAI.Erdos970.ErdosInverseSampleCost.sampleAverage_mono line 102
  9. theorem OAI.Erdos970.ErdosInverseSampleCost.sampleAverage_nonneg line 106
  10. theorem OAI.Erdos970.ErdosInverseSampleCost.sampleAverage_add line 110
  11. theorem OAI.Erdos970.ErdosInverseSampleCost.sampleAverage_mul line 115
  12. theorem OAI.Erdos970.ErdosInverseSampleCost.sampleAverage_div line 120
  13. theorem OAI.Erdos970.ErdosInverseSampleCost.sampleAverage_sum line 125
  14. theorem OAI.Erdos970.ErdosInverseSampleCost.sampleAverage_const line 131
  15. theorem OAI.Erdos970.ErdosInverseSampleCost.sampleAverage_product_bound line 139
  16. theorem OAI.Erdos970.ErdosInverseSampleCost.source_sample_population line 159