OAI/Combinatorics/Permanent/Stability.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FourRow.rowSq line 10

    Source comment

    Quantitative exponent-two stability estimates.
    def rowSq (a : Site → ℝ) : ℝ := ∑ j, a j ^ 2

    Mentions: OAI.FourRow.Site

  2. def OAI.FourRow.rowDist line 12
  3. def OAI.FourRow.rowDot line 14
  4. def OAI.FourRow.pairEntries line 16
  5. def OAI.FourRow.pairSq line 24
  6. theorem OAI.FourRow.rowSq_nonneg line 26
  7. theorem OAI.FourRow.rowDist_nonneg line 29
  8. theorem OAI.FourRow.pairSq_nonneg line 32
  9. theorem OAI.FourRow.pairSq_identity line 35
  10. theorem OAI.FourRow.pairSq_comm line 43
  11. theorem OAI.FourRow.rowDot_sq_le line 46
  12. theorem OAI.FourRow.rowDot_sq_le_four line 50
  13. theorem OAI.FourRow.pair_stability_one line 56
  14. theorem OAI.FourRow.pair_stability line 110
  15. theorem OAI.FourRow.sum_perm_succ line 120
  16. theorem OAI.FourRow.decompose4_two line 126
  17. theorem OAI.FourRow.decompose4_three line 130
  18. theorem OAI.FourRow.decompose3_two line 134
  19. theorem OAI.FourRow.permanent_pair_identity line 138
  20. def OAI.FourRow.uniformLaw line 150
  21. def OAI.FourRow.totalDist line 152
  22. theorem OAI.FourRow.totalDist_nonneg line 154
  23. theorem OAI.FourRow.pairSq_le line 157
  24. theorem OAI.FourRow.uniform_expectation_eq line 164
  25. theorem OAI.FourRow.normalized_uniform_stability line 169