OAI/NumberTheory/Jacobsthal/Probability/TransitionKernels.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos970.NumberTheoryLean.TransitionKernels.EvenState line 17
  2. abbrev OAI.Erdos970.NumberTheoryLean.TransitionKernels.OddState line 18
  3. def OAI.Erdos970.NumberTheoryLean.TransitionKernels.tailDensity line 20
  4. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.tailDensity_nonneg line 23
  5. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.tailDensity_integrable line 31
  6. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.tailDensity_integral line 37
  7. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.phiEven_measurable line 43
  8. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.W_measurable line 58
  9. def OAI.Erdos970.NumberTheoryLean.TransitionKernels.evenDensity line 62
  10. def OAI.Erdos970.NumberTheoryLean.TransitionKernels.oddDensity line 65
  11. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.evenDensity_measurable line 68
  12. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.oddDensity_measurable line 78
  13. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.evenDensity_nonneg line 89
  14. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.oddDensity_nonneg line 95
  15. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.evenDensity_integrable line 101
  16. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.oddDensity_integrable line 104
  17. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.evenDensity_integral line 107
  18. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.oddDensity_integral line 111
  19. def OAI.Erdos970.NumberTheoryLean.TransitionKernels.evenKernel line 114
  20. def OAI.Erdos970.NumberTheoryLean.TransitionKernels.oddKernel line 117
  21. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.evenKernel_apply line 120
  22. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.oddKernel_apply line 126
  23. instance OAI.Erdos970.NumberTheoryLean.TransitionKernels.evenKernel_isMarkovKernel line 132
  24. instance OAI.Erdos970.NumberTheoryLean.TransitionKernels.oddKernel_isMarkovKernel line 141
  25. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.evenKernel_below_support line 150
  26. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.oddKernel_below_support line 160
  27. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.evenKernel_ae_support line 170
  28. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.oddKernel_ae_support line 177
  29. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.evenKernel_ae_odd_domain line 184
  30. theorem OAI.Erdos970.NumberTheoryLean.TransitionKernels.oddKernel_ae_even_domain line 188