OAI/NumberTheory/Jacobsthal/Estimates/SourceRootReference.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosOmissionBindings.thirdInner_integral line 18
  2. theorem OAI.Erdos970.ErdosOmissionBindings.thirdKernel_integral line 44
  3. theorem OAI.Erdos970.ErdosOmissionBindings.third_loss_ordered_integral line 69
  4. theorem OAI.Erdos970.ErdosOmissionBindings.third_inner_rectangle_swap line 89
  5. theorem OAI.Erdos970.ErdosOmissionBindings.third_ordered_reversal line 100
  6. theorem OAI.Erdos970.ErdosOmissionBindings.actual_third_loss_eq_L3 line 146
  7. theorem OAI.Erdos970.ErdosOmissionTail.terminal_mass_affine_bound line 159
  8. theorem OAI.Erdos970.ErdosOmissionBindings.actual_second_loss_value line 232
  9. theorem OAI.Erdos970.ErdosOmissionBindings.actual_third_loss_value line 235
  10. theorem OAI.Erdos970.ErdosOmissionBindings.actual_first_three_loss_lt line 238
  11. theorem OAI.Erdos970.ErdosOmissionBindings.actual_first_three_partial_sum_lt line 242
  12. theorem OAI.Erdos970.ErdosOmissionTail.scalarTailMass_affine_bound line 256
  13. theorem OAI.Erdos970.ErdosOmissionTail.actual_omission_factorial_bound line 313
  14. theorem OAI.Erdos970.ErdosOmissionTail.actual_omission_tail_lt line 329
  15. theorem OAI.Erdos970.ErdosOmissionTail.actual_omission_tail_indicator_lt line 337
  16. theorem OAI.Erdos970.ErdosPositiveReference.actual_I_gt_eleven_seventyfive line 367
  17. theorem OAI.Erdos970.ErdosPositiveReference.actual_I_gt_source_margin line 374
  18. theorem OAI.Erdos970.ErdosPositiveReference.exp_gamma_lt_two line 377
  19. theorem OAI.Erdos970.ErdosPositiveReference.costMass_lt_eight line 383
  20. theorem OAI.Erdos970.ErdosPositiveReference.source_reference_coefficient_margin line 388
  21. theorem OAI.Erdos970.ErdosSourceReferenceMargin.actual_reference_limit_positive line 408
  22. theorem OAI.Erdos970.ErdosSourceReferenceMargin.actual_source_reference_lower_bound line 414
  23. theorem OAI.Erdos970.ErdosSourceReferenceMargin.actual_source_reference_eventually_positive line 439
  24. theorem OAI.Erdos970.NumberTheoryLean.SourceRootReference.source_primes_eq_root_set line 462
  25. theorem OAI.Erdos970.NumberTheoryLean.SourceRootReference.source_reference_root_polynomial line 469
  26. theorem OAI.Erdos970.NumberTheoryLean.SourceRootReference.source_root_polynomial_margin line 477
  27. theorem OAI.Erdos970.NumberTheoryLean.SourceRootReference.source_root_eventually_data line 486