OAI/Combinatorics/CliqueFree/FiniteCoupling.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CliqueFreeIndependence.FiniteCoupling.Law line 24
  2. def OAI.CliqueFreeIndependence.FiniteCoupling.dist line 25
  3. def OAI.CliqueFreeIndependence.FiniteCoupling.push line 27
  4. def OAI.CliqueFreeIndependence.FiniteCoupling.mix line 29
  5. lemma OAI.CliqueFreeIndependence.FiniteCoupling.sum_push line 31
  6. lemma OAI.CliqueFreeIndependence.FiniteCoupling.law_push line 39
  7. lemma OAI.CliqueFreeIndependence.FiniteCoupling.sum_mix line 44
  8. lemma OAI.CliqueFreeIndependence.FiniteCoupling.law_mix line 49
  9. lemma OAI.CliqueFreeIndependence.FiniteCoupling.law_dirac line 55
  10. lemma OAI.CliqueFreeIndependence.FiniteCoupling.prob_event_le_one line 60
  11. lemma OAI.CliqueFreeIndependence.FiniteCoupling.expected_indicator_push line 67
  12. lemma OAI.CliqueFreeIndependence.FiniteCoupling.expected_indicator_mix line 71
  13. lemma OAI.CliqueFreeIndependence.FiniteCoupling.exists_threshold_law line 77
  14. lemma OAI.CliqueFreeIndependence.FiniteCoupling.joint_of_trials line 132

    Source documentation

    A finite version of the first-accepted-trial construction, with states the set of unfinished rows. The recursion strictly decreases that finite set.

    lemma joint_of_trials [Nonempty J] (p : I → J → ℝ) (hp : ∀ i, Law (p i))
    (t : E → ℝ) (ht : ∀ e, 0 ≤ t e) (A : E → Finset I) (label : E → J)
    (hmarg : ∀ i y, (∑ e, if i ∈ A e ∧ label e = y then t e else 0) = p i y)
    (D : I → I → ℝ)
    (hpair : ∀ i j,
      (∑ e, if Xor (i ∈ A e) (j ∈ A e) then t e else 0) ≤
        D i j * (∑ e, if i ∈ A e ∨ j ∈ A e then t e else 0)) :
    ∃ q : (I → J) → ℝ, Law q ∧
      (∀ i y, (∑ f, if f i = y then q f else 0) = p i y) ∧
      (∀ i j, (∑ f, if f i ≠ f j then q f else 0) ≤ D i j) := by
…

    Mentions: OAI.CliqueFreeIndependence.FiniteCoupling.Law

  15. lemma OAI.CliqueFreeIndependence.FiniteCoupling.sum_abs_eq line 267
  16. lemma OAI.CliqueFreeIndependence.FiniteCoupling.shared_rejection line 273

    Source documentation

    The joint finite law in the shared rejection lemma, with its sharp bound.

    lemma shared_rejection [Nonempty J] (p : I → J → ℝ) (hp : ∀ i, Law (p i)) :
    ∃ q : (I → J) → ℝ, Law q ∧
      (∀ i y, (∑ f, if f i = y then q f else 0) = p i y) ∧
      (∀ i j, (∑ f, if f i ≠ f j then q f else 0) ≤
        2 * dist (p i) (p j) / (1 + dist (p i) (p j))) := by
…

    Mentions: OAI.CliqueFreeIndependence.FiniteCoupling.Law, OAI.CliqueFreeIndependence.FiniteCoupling.dist

  17. lemma OAI.CliqueFreeIndependence.FiniteCoupling.sharp_bound_le line 336
  18. lemma OAI.CliqueFreeIndependence.FiniteCoupling.positive_output line 340
  19. lemma OAI.CliqueFreeIndependence.FiniteCoupling.marginal_expectation line 350
  20. lemma OAI.CliqueFreeIndependence.FiniteCoupling.exists_positive_ge line 356
  21. def OAI.CliqueFreeIndependence.FiniteCoupling.bad line 375
  22. lemma OAI.CliqueFreeIndependence.FiniteCoupling.bad_and line 377