OAI/NumberTheory/Jacobsthal/Probability/SourceCompactCoupling.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.ActualFiniteCoupling.actual_finite_failure line 18
  2. theorem OAI.Erdos970.NumberTheoryLean.ActualFiniteCoupling.source_success_exits line 42
  3. def OAI.Erdos970.NumberTheoryLean.CouplingData.joint line 76
  4. def OAI.Erdos970.NumberTheoryLean.CouplingData.sourceLaw line 82
  5. theorem OAI.Erdos970.NumberTheoryLean.CouplingData.joint_eq line 91
  6. theorem OAI.Erdos970.NumberTheoryLean.CouplingData.sourceLaw_eq line 94
  7. theorem OAI.Erdos970.NumberTheoryLean.CouplingData.source_probability line 99
  8. theorem OAI.Erdos970.NumberTheoryLean.CouplingData.source_prime line 105
  9. theorem OAI.Erdos970.NumberTheoryLean.SourceCouplingRate.source_coupling_rate line 124
  10. theorem OAI.Erdos970.NumberTheoryLean.MarkedSourceSmallness.mark_mesh_smallness line 200
  11. theorem OAI.Erdos970.NumberTheoryLean.MarkedSourceSmallness.moving_compact_gap_small line 216
  12. def OAI.Erdos970.NumberTheoryLean.CompactCouplingError.difference line 245
  13. theorem OAI.Erdos970.NumberTheoryLean.CompactCouplingError.difference_measurable line 249
  14. theorem OAI.Erdos970.NumberTheoryLean.CompactCouplingError.actual_finite_compact_error line 254
  15. theorem OAI.Erdos970.NumberTheoryLean.SourceCompactCoupling.source_compact_coupling line 328