OAI/Combinatorics/IndependentSets/Repetition/KernelSampling.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.pushforward_eq_of_agree_on_support line 13
2. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.product_pushforward line 28
3. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.table_row_weight_ne_zero line 45
4. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.table_repair_pushforward line 55
5. abbrev OAI.IndependentSetsGames.Foundations.Games.KernelSampling.Seed line 72
6. def OAI.IndependentSetsGames.Foundations.Games.KernelSampling.readLeft line 74
7. def OAI.IndependentSetsGames.Foundations.Games.KernelSampling.readRight line 75
8. def OAI.IndependentSetsGames.Foundations.Games.KernelSampling.seedLaw line 77
9. theorem OAI.IndependentSetsGames.Foundations.Games.KernelSampling.read_joint_pushforward line 84
10. theorem OAI.IndependentSetsGames.Foundations.Games.KernelSampling.repaired_joint_pushforward line 97
11. def OAI.IndependentSetsGames.Foundations.Games.KernelSampling.completedLeft line 117
12. def OAI.IndependentSetsGames.Foundations.Games.KernelSampling.completedRight line 121
13. theorem OAI.IndependentSetsGames.Foundations.Games.KernelSampling.completedLeft_coordinate line 125
14. theorem OAI.IndependentSetsGames.Foundations.Games.KernelSampling.completedRight_coordinate line 129
15. theorem OAI.IndependentSetsGames.Foundations.Games.KernelSampling.update_eq_of_coordinate line 133
16. theorem OAI.IndependentSetsGames.Foundations.Games.KernelSampling.completed_joint_pushforward line 138