OAI/NumberTheory/Jacobsthal/Estimates/ActualModelTargets.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosVarianceCommon.relative_deviation_iff line 15
  2. theorem OAI.Erdos970.ErdosVarianceCommon.common_deviation_transfer line 20
  3. def OAI.Erdos970.ErdosVarianceMoments.modelSurvives line 43
  4. def OAI.Erdos970.ErdosVarianceMoments.modelIndicator line 49
  5. def OAI.Erdos970.ErdosVarianceMoments.jointCondition line 53
  6. def OAI.Erdos970.ErdosVarianceMoments.jointIndicator line 57
  7. theorem OAI.Erdos970.ErdosVarianceMoments.modelIndicator_binary line 61
  8. theorem OAI.Erdos970.ErdosVarianceMoments.jointCondition_split line 67
  9. theorem OAI.Erdos970.ErdosVarianceMoments.jointIndicator_singleton line 79
  10. theorem OAI.Erdos970.ErdosVarianceMoments.jointIndicator_pair line 84
  11. theorem OAI.Erdos970.ErdosVarianceMoments.jointIndicator_empty line 92
  12. def OAI.Erdos970.ErdosVarianceCommon.referenceCount line 105
  13. def OAI.Erdos970.ErdosVarianceCommon.commonReference line 108
  14. theorem OAI.Erdos970.ErdosVarianceCommon.reference_above_common line 111
  15. theorem OAI.Erdos970.ErdosVarianceCommon.common_reference_error line 118
  16. def OAI.Erdos970.ErdosVarianceCommon.commonSurvivors line 145
  17. theorem OAI.Erdos970.ErdosVarianceCommon.effectiveSurvivors_eq_progression line 149
  18. theorem OAI.Erdos970.ErdosVarianceCommon.mem_commonSurvivors line 165
  19. theorem OAI.Erdos970.ErdosVarianceCommon.hypothetical_count_eq_full_common_card line 181
  20. theorem OAI.Erdos970.ErdosVarianceCommon.source_common_interval_slack line 201
  21. theorem OAI.Erdos970.ErdosVarianceCommon.commonLength_comparable line 237
  22. theorem OAI.Erdos970.ErdosVarianceCommon.large_prime_not_cutoff line 269
  23. theorem OAI.Erdos970.ErdosVarianceCommon.effective_step_coprime_small line 276
  24. theorem OAI.Erdos970.ErdosVarianceCommon.source_common_count_errors line 287
  25. theorem OAI.Erdos970.ErdosVarianceCommon.source_actual_bad_to_common line 344
  26. def OAI.Erdos970.ErdosVarianceMoments.actualDivisorTarget line 394
  27. def OAI.Erdos970.ErdosVarianceMoments.actualCoprimeTarget line 397
  28. def OAI.Erdos970.ErdosVarianceMoments.actualModelSurvives line 400
  29. def OAI.Erdos970.ErdosVarianceMoments.actualModelIndicator line 405
  30. theorem OAI.Erdos970.ErdosVarianceMoments.aligned_isolated_coprime_effective line 410
  31. theorem OAI.Erdos970.ErdosVarianceMoments.aligned_coefficient_coprime_small line 419