OAI/Combinatorics/Permanent/Model.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A robust four-row permanent inequality

Fin 4 labels four sites. A law is represented by real probability masses; IsProbability asserts nonnegativity and total mass one. All row norms use the uniform counting normalization.

  1. abbrev OAI.FourRow.Site line 17

    Also declared: ComparatorChallenges/FourRowPermanent.lean:17 (same declaration text).

  2. abbrev OAI.FourRow.Perm line 18

    Also declared: ComparatorChallenges/FourRowPermanent.lean:18 (same declaration text).

  3. abbrev OAI.FourRow.Law line 19

    Also declared: ComparatorChallenges/FourRowPermanent.lean:19 (same declaration text).

  4. abbrev OAI.FourRow.Functions line 20

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

  5. def OAI.FourRow.IsProbability line 22

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

  6. def OAI.FourRow.UniformMarginals line 25

    Also declared: ComparatorChallenges/FourRowPermanent.lean:25 (same declaration text).

  7. def OAI.FourRow.totalVariation line 28

    Also declared: ComparatorChallenges/FourRowPermanent.lean:28 (same declaration text).

  8. def OAI.FourRow.lpNorm line 31

    Also declared: ComparatorChallenges/FourRowPermanent.lean:31 (same declaration text).

  9. def OAI.FourRow.permanentExpectation line 34

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