OAI/NumberTheory/Jacobsthal/Probability/StateKernelInvariance.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.OrdinaryKernelInvariance.evenLift line 17
2. def OAI.Erdos970.Erdos970Dependency.OrdinaryKernelInvariance.oddLift line 18
3. theorem OAI.Erdos970.Erdos970Dependency.OrdinaryKernelInvariance.evenLift_measurable line 20
4. theorem OAI.Erdos970.Erdos970Dependency.OrdinaryKernelInvariance.oddLift_measurable line 23
5. def OAI.Erdos970.Erdos970Dependency.OrdinaryKernelInvariance.evenRealKernel line 26
6. def OAI.Erdos970.Erdos970Dependency.OrdinaryKernelInvariance.oddRealKernel line 27
7. instance OAI.Erdos970.Erdos970Dependency.OrdinaryKernelInvariance.evenRealKernel_isMarkovKernel line 29
8. instance OAI.Erdos970.Erdos970Dependency.OrdinaryKernelInvariance.oddRealKernel_isMarkovKernel line 30
9. theorem OAI.Erdos970.Erdos970Dependency.OrdinaryKernelInvariance.even_lifted_product line 32
10. theorem OAI.Erdos970.Erdos970Dependency.OrdinaryKernelInvariance.odd_lifted_product line 41
11. theorem OAI.Erdos970.Erdos970Dependency.OrdinaryKernelInvariance.even_ratio_invariance line 50
12. theorem OAI.Erdos970.Erdos970Dependency.OrdinaryKernelInvariance.odd_ratio_invariance line 70
13. theorem OAI.Erdos970.Erdos970Dependency.StateKernelInvariance.comp_map_input line 102
14. theorem OAI.Erdos970.Erdos970Dependency.StateKernelInvariance.oddLift_ratio line 110
15. theorem OAI.Erdos970.Erdos970Dependency.StateKernelInvariance.evenLift_ratio line 114
16. theorem OAI.Erdos970.Erdos970Dependency.StateKernelInvariance.evenKernel_map_lift line 118
17. theorem OAI.Erdos970.Erdos970Dependency.StateKernelInvariance.oddKernel_map_lift line 122
18. def OAI.Erdos970.Erdos970Dependency.StateKernelInvariance.evenStateMeasure line 126
19. def OAI.Erdos970.Erdos970Dependency.StateKernelInvariance.oddStateMeasure line 127
20. instance OAI.Erdos970.Erdos970Dependency.StateKernelInvariance.evenStateMeasure_isFiniteMeasure line 129
21. instance OAI.Erdos970.Erdos970Dependency.StateKernelInvariance.oddStateMeasure_isFiniteMeasure line 130
22. theorem OAI.Erdos970.Erdos970Dependency.StateKernelInvariance.even_state_invariance line 132
23. theorem OAI.Erdos970.Erdos970Dependency.StateKernelInvariance.odd_state_invariance line 143
24. def OAI.Erdos970.Erdos970Dependency.StateKernelInvariance.stateMeasure line 154
25. instance OAI.Erdos970.Erdos970Dependency.StateKernelInvariance.stateMeasure_isFiniteMeasure line 157
26. theorem OAI.Erdos970.Erdos970Dependency.StateKernelInvariance.state_invariance line 159