OAI/Combinatorics/ExpectationThreshold/Model.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Containment covers and expectation thresholds

Both costs use budget one half. Fractional coefficients are indexed by every subset of the ground set, without a support-size bound. The empty subset is included, and ordinary natural powers give p^0 = 1, including at zero. The thresholds are real suprema of feasible densities in the closed unit interval.

  1. abbrev OAI.TalagrandThreshold.Family line 23

    Also declared: ComparatorChallenges/TalagrandExpectationThreshold.lean:14 (same declaration text).

  2. def OAI.TalagrandThreshold.cost line 29

    Also declared: ComparatorChallenges/TalagrandExpectationThreshold.lean:20 (same declaration text).

  3. def OAI.TalagrandThreshold.Covers line 31

    Also declared: ComparatorChallenges/TalagrandExpectationThreshold.lean:22 (same declaration text).

  4. def OAI.TalagrandThreshold.Small line 33

    Also declared: ComparatorChallenges/TalagrandExpectationThreshold.lean:24 (same declaration text).

  5. def OAI.TalagrandThreshold.fracCost line 36

    Also declared: ComparatorChallenges/TalagrandExpectationThreshold.lean:27 (same declaration text).

  6. def OAI.TalagrandThreshold.FractionalCover line 39

    Also declared: ComparatorChallenges/TalagrandExpectationThreshold.lean:30 (same declaration text).

  7. def OAI.TalagrandThreshold.FractionalSmall line 43

    Also declared: ComparatorChallenges/TalagrandExpectationThreshold.lean:34 (same declaration text).

  8. def OAI.TalagrandThreshold.Increasing line 46

    Also declared: ComparatorChallenges/TalagrandExpectationThreshold.lean:37 (same declaration text).

  9. def OAI.TalagrandThreshold.integralFeasible line 49

    Also declared: ComparatorChallenges/TalagrandExpectationThreshold.lean:40 (same declaration text).

  10. def OAI.TalagrandThreshold.fractionalFeasible line 52

    Also declared: ComparatorChallenges/TalagrandExpectationThreshold.lean:43 (same declaration text).

  11. def OAI.TalagrandThreshold.q line 56

    Source documentation

    The integral expectation threshold.

    Also declared: ComparatorChallenges/TalagrandExpectationThreshold.lean:46 (same declaration text).

    def q (F : Family α) : ℝ := sSup (integralFeasible F)

    Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.integralFeasible

  12. def OAI.TalagrandThreshold.qf line 59

    Source documentation

    The fractional expectation threshold.

    Distinct definitions of this name: ComparatorChallenges/TalagrandExpectationThreshold.lean:48 (same statement text; different proof or body). Qualify references as OAI.TalagrandThreshold.qf@path.

    def qf (F : Family α) : ℝ := sSup (fractionalFeasible F)
…

    Mentions: OAI.TalagrandThreshold.Family, OAI.TalagrandThreshold.fractionalFeasible

  13. theorem OAI.TalagrandThreshold.mem_integralFeasible line 62
  14. theorem OAI.TalagrandThreshold.mem_fractionalFeasible line 66