OAI/Probability/GammaPassage/BKForcing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.ForcesBits line 10

   Source documentation

   Fixing every bit in c to its value in x forces the event A.

   Also declared: OAI/Probability/FirstPassage/BKForcing.lean:9 (same declaration text).

   def ForcesBits (s : Finset α) (A : Finset (Finset α)) (x c : Finset α) : Prop :=
   …

2. lemma OAI.PlanarFPP.ForcesBits.positive_certificate line 13

   Also declared: OAI/Probability/FirstPassage/BKForcing.lean:12 (same declaration text).

3. theorem OAI.PlanarFPP.forcing_certificates_mem line 19

   Also declared: OAI/Probability/FirstPassage/BKForcing.lean:18 (same declaration text).

4. theorem OAI.PlanarFPP.finite_fair_BK_forcing line 34

   Also declared: OAI/Probability/FirstPassage/BKForcing.lean:33 (same declaration text).