OAI/Combinatorics/GraphThreshold/ResamplingEvents.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LeanBlast.SecondKahnKalai.LocalSuccess line 17

   Source documentation

   The denominator is large enough and the retained fragment fits in the halved integral capacity.

   def LocalSuccess (ν : FiniteLaw B) (A : B → Finset X) (ρ : ℝ) (m : ℕ)
       (W : Finset X) (c b : B) : Prop :=
   …

   Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw

2. def OAI.LeanBlast.SecondKahnKalai.LocalFailure line 23

   Source documentation

   A local failure is the complement of the actual local success event.

   def LocalFailure (ν : FiniteLaw B) (A : B → Finset X) (ρ : ℝ) (m : ℕ)
       (W : Finset X) (c b : B) : Prop :=
   …

   Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw

3. theorem OAI.LeanBlast.SecondKahnKalai.localFailure_iff line 27
4. theorem OAI.LeanBlast.SecondKahnKalai.localFailure_iff_twice line 34