OAI/NumberTheory/Jacobsthal/Probability/CouplingLabelEvents.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.CoupledBoundaryEvents.lowerA line 21
  2. def OAI.Erdos970.NumberTheoryLean.CoupledBoundaryEvents.lowerB line 22
  3. def OAI.Erdos970.NumberTheoryLean.CoupledBoundaryEvents.upperA line 23
  4. def OAI.Erdos970.NumberTheoryLean.CoupledBoundaryEvents.upperB line 24
  5. def OAI.Erdos970.NumberTheoryLean.CoupledBoundaryEvents.primeBadCells line 28
  6. def OAI.Erdos970.NumberTheoryLean.CoupledBoundaryEvents.continuousBadCells line 33
  7. theorem OAI.Erdos970.NumberTheoryLean.CoupledBoundaryEvents.packet_widths line 38
  8. theorem OAI.Erdos970.NumberTheoryLean.CoupledBoundaryEvents.point_in_clipped_packets line 48
  9. theorem OAI.Erdos970.NumberTheoryLean.CoupledBoundaryEvents.prime_bad_cell_packets line 55
  10. theorem OAI.Erdos970.NumberTheoryLean.CoupledBoundaryEvents.continuous_bad_cell_packets line 77
  11. def OAI.Erdos970.NumberTheoryLean.CouplingLabelEvents.interiorLabels line 112
  12. def OAI.Erdos970.NumberTheoryLean.CouplingLabelEvents.boundaryLabels line 116
  13. theorem OAI.Erdos970.NumberTheoryLean.CouplingLabelEvents.prime_boundary_event line 122
  14. theorem OAI.Erdos970.NumberTheoryLean.CouplingLabelEvents.continuous_boundary_event_mass line 137
  15. theorem OAI.Erdos970.NumberTheoryLean.CouplingLabelEvents.prime_boundary_mass line 155
  16. theorem OAI.Erdos970.NumberTheoryLean.CouplingLabelEvents.continuous_boundary_mass line 162
  17. theorem OAI.Erdos970.NumberTheoryLean.CouplingLabelEvents.actual_label_budget line 168