OAI/NumberTheory/Jacobsthal/Probability/EvenThresholdEvent.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosEvenThreshold.stripDensityBound line 13
  2. def OAI.Erdos970.ErdosEvenThreshold.stripConstant line 14
  3. theorem OAI.Erdos970.ErdosEvenThreshold.stripDensityBound_pos line 16
  4. theorem OAI.Erdos970.ErdosEvenThreshold.stripConstant_pos line 22
  5. theorem OAI.Erdos970.ErdosEvenThreshold.oddDensity_compact_bound line 26
  6. theorem OAI.Erdos970.ErdosEvenThreshold.oddKernel_strip_bound line 51
  7. theorem OAI.Erdos970.ErdosEvenThreshold.oddToEven_strip_bound line 70
  8. theorem OAI.Erdos970.ErdosEvenThreshold.exists_uniform_strip_bound line 78
  9. def OAI.Erdos970.ErdosEvenThreshold.nearThreshold line 93
  10. theorem OAI.Erdos970.ErdosEvenThreshold.thresholdStrip_eq_near line 96
  11. theorem OAI.Erdos970.ErdosEvenThreshold.nearThreshold_measurable line 111
  12. theorem OAI.Erdos970.ErdosEvenThreshold.conditional_even_near_threshold line 115
  13. theorem OAI.Erdos970.ErdosEvenThreshold.conditional_even_near_threshold_real line 122
  14. theorem OAI.Erdos970.ErdosEvenThreshold.exists_conditional_even_bound line 129