OAI/Combinatorics/GraphThreshold/Main.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The second Kahn–Kalai graph-threshold bounds

The graph-to-orbit bridge counts actual unlabelled subgraphs. The hierarchy is constructed from the constraints at the attained expectation threshold, and covering one of its paths yields a copy of the original graph.

  1. def OAI.LeanBlast.SecondKahnKalai.FullStatement line 23
  2. theorem OAI.LeanBlast.SecondKahnKalai.secondKahnKalaiBounds line 25

    Distinct definitions of this name: ComparatorChallenges/SecondKahnKalai.lean:65 (same statement text; different proof or body). Qualify references as OAI.LeanBlast.SecondKahnKalai.secondKahnKalaiBounds@path.

  3. theorem OAI.LeanBlast.SecondKahnKalai.secondKahnKalai line 67