OAI/Probability/BenjaminiSchramm/PairedSprinkling.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.BernoulliProduct.pairedParameters line 15
  2. def OAI.CriticalPercolation.BernoulliProduct.whiteProjection line 18
  3. def OAI.CriticalPercolation.BernoulliProduct.blueProjection line 21
  4. def OAI.CriticalPercolation.BernoulliProduct.pairedUnion line 24
  5. lemma OAI.CriticalPercolation.BernoulliProduct.measurable_whiteProjection line 26
  6. lemma OAI.CriticalPercolation.BernoulliProduct.measurable_blueProjection line 29
  7. lemma OAI.CriticalPercolation.BernoulliProduct.measurable_pairedUnion line 32
  8. lemma OAI.CriticalPercolation.BernoulliProduct.pairedUnion_eq line 37
  9. lemma OAI.CriticalPercolation.BernoulliProduct.paired_white_law line 42
  10. lemma OAI.CriticalPercolation.BernoulliProduct.paired_blue_law line 49
  11. lemma OAI.CriticalPercolation.BernoulliProduct.paired_union_law line 56
  12. def OAI.CriticalPercolation.BernoulliProduct.whiteBlock line 76
  13. def OAI.CriticalPercolation.BernoulliProduct.erasedWhiteParameters line 78
  14. lemma OAI.CriticalPercolation.BernoulliProduct.pinned_white_parameters line 81
  15. lemma OAI.CriticalPercolation.BernoulliProduct.fresh_paired_union_law line 90
  16. def OAI.CriticalPercolation.BernoulliProduct.atParameters line 97
  17. lemma OAI.CriticalPercolation.BernoulliProduct.measurable_atParameters line 99
  18. lemma OAI.CriticalPercolation.BernoulliProduct.markLaw_map_atParameters line 102
  19. lemma OAI.CriticalPercolation.BernoulliProduct.law_mono_pointwise line 110