OAI/NumberTheory/Jacobsthal/Probability/SubMarkovFlagPowers.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Erdos970.NumberTheoryLean.SubMarkovFlagPowers.marked_sfinite line 18
2. theorem OAI.Erdos970.NumberTheoryLean.SubMarkovFlagPowers.marked_eq_map_sfinite line 23
3. theorem OAI.Erdos970.NumberTheoryLean.SubMarkovFlagPowers.marked_map_sfinite line 35
4. def OAI.Erdos970.NumberTheoryLean.SubMarkovFlagPowers.goodSelect line 42
5. theorem OAI.Erdos970.NumberTheoryLean.SubMarkovFlagPowers.goodSelect_measurable line 44
6. def OAI.Erdos970.NumberTheoryLean.SubMarkovFlagPowers.goodKernel line 47
7. instance OAI.Erdos970.NumberTheoryLean.SubMarkovFlagPowers.goodKernel_sfinite line 50
8. theorem OAI.Erdos970.NumberTheoryLean.SubMarkovFlagPowers.good_row_lift line 55
9. theorem OAI.Erdos970.NumberTheoryLean.SubMarkovFlagPowers.good_power_lift line 72
10. theorem OAI.Erdos970.NumberTheoryLean.SubMarkovFlagPowers.finite_integral_partition line 101