OAI/Probability/CriticalPercolation/ProductMeasure/ProductConditioning.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BernoulliProduct.mem_forceOn line 16
2. lemma OAI.CriticalPercolation.BernoulliProduct.measurable_forceOn_joint line 19
3. lemma OAI.CriticalPercolation.BernoulliProduct.measurable_forceOn_joint_block line 28
4. lemma OAI.CriticalPercolation.BernoulliProduct.forceOn_resample_law line 43
5. def OAI.CriticalPercolation.BernoulliProduct.pinnedParameters line 73
6. lemma OAI.CriticalPercolation.BernoulliProduct.forceOn_map_law line 76
7. def OAI.CriticalPercolation.BernoulliProduct.blockProbability line 92
8. lemma OAI.CriticalPercolation.BernoulliProduct.blockProbability_eq_lintegral line 95
9. lemma OAI.CriticalPercolation.BernoulliProduct.blockProbability_le_one line 102
10. lemma OAI.CriticalPercolation.BernoulliProduct.measurable_blockProbability line 105
11. lemma OAI.CriticalPercolation.BernoulliProduct.blockProbability_monotone line 120
12. lemma OAI.CriticalPercolation.BernoulliProduct.lintegral_blockProbability line 132
13. lemma OAI.CriticalPercolation.BernoulliProduct.blockSigma_eq_comap line 144
14. lemma OAI.CriticalPercolation.BernoulliProduct.block_event_forceOn line 156
15. lemma OAI.CriticalPercolation.BernoulliProduct.blockProbability_inter_block line 167
16. lemma OAI.CriticalPercolation.BernoulliProduct.setLIntegral_blockProbability line 183
17. lemma OAI.CriticalPercolation.BernoulliProduct.forceOn_absorb line 191
18. lemma OAI.CriticalPercolation.BernoulliProduct.blockProbability_pin_smaller line 201
19. lemma OAI.CriticalPercolation.BernoulliProduct.lintegral_blockProbability_tower line 208