OAI/Combinatorics/ExpectationThreshold/SelectorDefinitions.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Actual moves and profiles for the simultaneous selector

We retain all colorings of minimum total movement for at least one original family member. This avoids an arbitrary tie-breaking order; each retained coloring still has the member-specific minimality used in reconstruction.

  1. structure OAI.TalagrandThreshold.Selector.MassFamily line 26

    Source documentation

    A probability mass for each actual member of the family.

    structure MassFamily (F : Family α) where
…

    Mentions: OAI.TalagrandThreshold.Family

  2. def OAI.TalagrandThreshold.Selector.prefixSet line 33

    Source documentation

    Colors have zero-based indices; the actual color level is one larger.

    def prefixSet {s : ℕ} (z : Coloring α s) (i : Fin s) : Finset α :=
…

    Mentions: OAI.TalagrandThreshold.Coloring

  3. def OAI.TalagrandThreshold.Selector.dscale line 36
  4. def OAI.TalagrandThreshold.Selector.Earlier line 39

    Source documentation

    Earlier a z means that the move from a to z only lowers colors.

    def Earlier {s : ℕ} (a z : Coloring α s) : Prop := ∀ x, z x ≤ a x

    Mentions: OAI.TalagrandThreshold.Coloring

  5. def OAI.TalagrandThreshold.Selector.changes line 41
  6. def OAI.TalagrandThreshold.Selector.crossings line 44
  7. def OAI.TalagrandThreshold.Selector.movement line 47
  8. def OAI.TalagrandThreshold.Selector.movedRow line 50
  9. abbrev OAI.TalagrandThreshold.Selector.Profile line 54

    Source documentation

    The full profile retains both final and original colors.

    abbrev Profile (s : ℕ) := Fin s → Color s → ℕ

    Mentions: OAI.TalagrandThreshold.Color

  10. def OAI.TalagrandThreshold.Selector.profile line 56
  11. def OAI.TalagrandThreshold.Selector.rowCount line 60
  12. def OAI.TalagrandThreshold.Selector.profileSize line 62
  13. def OAI.TalagrandThreshold.Selector.profileCrossings line 64
  14. def OAI.TalagrandThreshold.Selector.FeasibleFor line 68
  15. def OAI.TalagrandThreshold.Selector.Feasible line 73
  16. def OAI.TalagrandThreshold.Selector.BoundedFeasible line 77
  17. def OAI.TalagrandThreshold.Selector.IsMinimalMove line 81
  18. def OAI.TalagrandThreshold.Selector.Selected line 86
  19. def OAI.TalagrandThreshold.Selector.selectedMoves line 89
  20. def OAI.TalagrandThreshold.Selector.Captured line 95

    Source documentation

    An actual bad original coloring, its selected endpoint, and its full profile.

    def Captured {F : Family α} (mu : MassFamily F) {s : ℕ}
    (a : Coloring α s) : Prop :=
…

    Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.Selector.MassFamily, OAI.TalagrandThreshold.Coloring

  21. def OAI.TalagrandThreshold.Selector.Bad line 100
  22. def OAI.TalagrandThreshold.Selector.groupOriginals line 103
  23. def OAI.TalagrandThreshold.Selector.meanColor line 108