OAI/Combinatorics/GraphThreshold/ThresholdBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Explicit constants in the threshold conclusion

The tree argument first gives a logarithm of an edge capacity. These elementary bounds turn that quantity into the two constants stated for graphs.

  1. theorem OAI.LeanBlast.SecondKahnKalai.logTwo_eq_logb line 18
  2. theorem OAI.LeanBlast.SecondKahnKalai.logTwo_nonneg line 20
  3. theorem OAI.LeanBlast.SecondKahnKalai.logTwo_mono line 24
  4. theorem OAI.LeanBlast.SecondKahnKalai.edgeCount_le_sq line 30
  5. theorem OAI.LeanBlast.SecondKahnKalai.one_add_logTwo_le_three_logTwo line 41
  6. theorem OAI.LeanBlast.SecondKahnKalai.graph_one_add_logTwo_le_three_logTwo line 64
  7. theorem OAI.LeanBlast.SecondKahnKalai.graphThresholdParameter_mem_unitInterval line 71
  8. theorem OAI.LeanBlast.SecondKahnKalai.treeSamplingParameter_mem_unitInterval line 80
  9. theorem OAI.LeanBlast.SecondKahnKalai.treeSamplingParameter_le_graphParameter line 88
  10. theorem OAI.LeanBlast.SecondKahnKalai.graphThresholdParameter_le_vertexBound line 104