OAI/Combinatorics/ProgressionColoring/FairOuterColoring.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Coloring a finite family of literal supports

The sample space is the actual set of all Boolean assignments to labels. The events test quarter-balancing on their named supports. Independence is derived from disjoint supports of the product law, rather than postulated for the tests.

  1. theorem OAI.QuantitativeVanDerWaerden.outer_avoid_depends line 24

    Source documentation

    Avoidance of tests depends only on the union of their literal supports.

    theorem outer_avoid_depends {I : Type uI} {Label : Type uLabel} [Fintype I] [DecidableEq I]
    [Fintype Label] [DecidableEq Label]
    (support : I → Finset Label) (T : Finset I) :
    FiniteProbability.DependsOn (T.biUnion support)
      (FiniteLocalLemma.avoid (fun i => fairBalancingBad (support i)) T) := by
…

    Mentions: OAI.QuantitativeVanDerWaerden.FiniteProbability.DependsOn, OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.avoid, OAI.QuantitativeVanDerWaerden.fairBalancingBad

  2. theorem OAI.QuantitativeVanDerWaerden.outer_nonneighbor_supports_disjoint line 42
  3. theorem OAI.QuantitativeVanDerWaerden.exists_fair_balancing_coloring line 61