OAI/Combinatorics/GraphThreshold/Model.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LeanBlast.SecondKahnKalai.bernoulliWeight line 15

   Also declared: ComparatorChallenges/SecondKahnKalai.lean:15 (same declaration text).

2. def OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation line 19

   Also declared: ComparatorChallenges/SecondKahnKalai.lean:19 (same declaration text).

3. def OAI.LeanBlast.SecondKahnKalai.bernoulliProbability line 23

   Also declared: ComparatorChallenges/SecondKahnKalai.lean:23 (same declaration text).

4. abbrev OAI.LeanBlast.SecondKahnKalai.Edge line 29

   Source documentation

   The unordered non-loop edges of the complete graph on n vertices.

   Also declared: ComparatorChallenges/SecondKahnKalai.lean:29 (same declaration text).

   abbrev Edge (n : ℕ) := {e : Sym2 (Fin n) // ¬e.IsDiag}

5. def OAI.LeanBlast.SecondKahnKalai.graphOfEdges line 32

   Source documentation

   A set of edges, interpreted as an ordinary graph on all n vertices.

   Also declared: ComparatorChallenges/SecondKahnKalai.lean:32 (same declaration text).

   def graphOfEdges {n : ℕ} (W : Finset (Edge n)) : SimpleGraph (Fin n) :=
   …

   Mentions: OAI.LeanBlast.SecondKahnKalai.Edge

6. def OAI.LeanBlast.SecondKahnKalai.edgeCount line 36

   Source documentation

   The number of unordered edges, each counted once.

   Also declared: ComparatorChallenges/SecondKahnKalai.lean:36 (same declaration text).

   def edgeCount {V : Type u} (H : SimpleGraph V) : ℕ := Nat.card H.edgeSet

7. def OAI.LeanBlast.SecondKahnKalai.expectedCopies line 39

   Source documentation

   Expected number of actual unlabelled non-induced copies in G(n,p).

   Also declared: ComparatorChallenges/SecondKahnKalai.lean:39 (same declaration text).

   def expectedCopies {V : Type u} (n : ℕ) (p : ℝ) (H : SimpleGraph V) : ℝ :=
   …

8. def OAI.LeanBlast.SecondKahnKalai.containmentProbability line 44

   Source documentation

   Probability that G(n,p) contains at least one non-induced copy.

   Also declared: ComparatorChallenges/SecondKahnKalai.lean:44 (same declaration text).

   def containmentProbability {V : Type u} (n : ℕ) (p : ℝ)
       (H : SimpleGraph V) : ℝ :=
   …

9. def OAI.LeanBlast.SecondKahnKalai.criticalThreshold line 49

   Also declared: ComparatorChallenges/SecondKahnKalai.lean:49 (same declaration text).

10. def OAI.LeanBlast.SecondKahnKalai.expectationThreshold line 52

    Also declared: ComparatorChallenges/SecondKahnKalai.lean:52 (same declaration text).

11. def OAI.LeanBlast.SecondKahnKalai.logTwo line 56

    Also declared: ComparatorChallenges/SecondKahnKalai.lean:56 (same declaration text).

12. def OAI.LeanBlast.SecondKahnKalai.SecondKahnKalaiBounds line 58

    Also declared: ComparatorChallenges/SecondKahnKalai.lean:58 (same declaration text).