OAI/NumberTheory/Jacobsthal/Estimates/SourceExtensionScale.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosInverseSampleCost.sourceW_log_bounds line 16
  2. theorem OAI.Erdos970.ErdosInverseSampleCost.sourceW_le_power line 36
  3. theorem OAI.Erdos970.ErdosInverseSampleCost.source_inverse_power_log_tendsto line 45
  4. theorem OAI.Erdos970.ErdosVarianceSmallModel.source_model_population line 79
  5. theorem OAI.Erdos970.ErdosInverseSampleCost.source_rounding_log_tendsto line 107
  6. theorem OAI.Erdos970.ErdosInverseSampleCost.source_cost_budget line 170
  7. theorem OAI.Erdos970.ErdosVarianceSmallModel.atomWeight_totient line 219
  8. theorem OAI.Erdos970.ErdosVarianceSmallModel.prime_bound_le_atom line 227
  9. theorem OAI.Erdos970.ErdosVarianceSmallModel.finite_model_domination line 257
  10. theorem OAI.Erdos970.ErdosVarianceSmallModel.source_prime_model_domination line 297
  11. theorem OAI.Erdos970.ErdosVarianceEffective.badPrimeProduct_extension_dvd line 359
  12. theorem OAI.Erdos970.ErdosVarianceEffective.effectiveModulus_extension_le line 373
  13. theorem OAI.Erdos970.ErdosVarianceEffective.effectiveModulus_height_of_extension line 380
  14. theorem OAI.Erdos970.ErdosVarianceEffective.sourceW_power_subpower line 402
  15. theorem OAI.Erdos970.ErdosVarianceEffective.extension_le_parent_power line 417
  16. theorem OAI.Erdos970.ErdosVarianceEffective.source_extension_le_Z line 429