OAI/NumberTheory/Jacobsthal/Probability/SourceThresholdCoupling.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.ReconstructedParentCoupling.primeNearThreshold line 17
  2. theorem OAI.Erdos970.NumberTheoryLean.ReconstructedParentCoupling.node_parent_reconstruction line 20
  3. theorem OAI.Erdos970.NumberTheoryLean.ReconstructedParentCoupling.node_near_reconstruction line 31
  4. theorem OAI.Erdos970.NumberTheoryLean.ReconstructedParentCoupling.log_reconstructed_parent line 39
  5. theorem OAI.Erdos970.NumberTheoryLean.ReconstructedParentCoupling.reconstructed_log_stability line 45
  6. theorem OAI.Erdos970.NumberTheoryLean.ReconstructedParentCoupling.good_prime_near_thick line 56
  7. def OAI.Erdos970.NumberTheoryLean.SourceThresholdCoupling.nearPrimeNode line 104
  8. def OAI.Erdos970.NumberTheoryLean.SourceThresholdCoupling.primeThresholdOccurs line 108
  9. theorem OAI.Erdos970.NumberTheoryLean.SourceThresholdCoupling.primeThresholdOccurs_measurable line 111
  10. def OAI.Erdos970.NumberTheoryLean.SourceThresholdCoupling.thresholdPerturbation line 120
  11. theorem OAI.Erdos970.NumberTheoryLean.SourceThresholdCoupling.thresholdPerturbation_nonneg line 123
  12. theorem OAI.Erdos970.NumberTheoryLean.SourceThresholdCoupling.thickArrival_mono line 129
  13. theorem OAI.Erdos970.NumberTheoryLean.SourceThresholdCoupling.sourceHistory_threshold_transfer line 137
  14. theorem OAI.Erdos970.NumberTheoryLean.SourceThresholdCoupling.source_threshold_probability line 175