OAI/NumberTheory/Jacobsthal/Probability/FiniteHistoryPairLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.FiniteHistoryPairLaw.adjacentPair line 15
  2. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryPairLaw.adjacentPair_measurable line 18
  3. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryPairLaw.lintegral_adjacent_pair line 21
  4. def OAI.Erdos970.NumberTheoryLean.FiniteHistoryPairLaw.pairProbability line 47
  5. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryPairLaw.pairProbability_integral line 50
  6. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryPairLaw.pairProbability_measurable line 55
  7. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryPairLaw.adjacent_pair_probability line 62