OAI/Probability/SignedSweeps/SweepCoefficients.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.coefficientAction_layer line 9
  2. lemma OAI.SignedSweeps.coefficientPush_list line 27
  3. lemma OAI.SignedSweeps.productCoefficient_list line 34
  4. def OAI.SignedSweeps.sweepCoefficient line 49
  5. lemma OAI.SignedSweeps.sweepCoefficient_action line 53
  6. def OAI.SignedSweeps.sweepPowerCoefficient line 58
  7. lemma OAI.SignedSweeps.sweepPowerCoefficient_positive line 63
  8. lemma OAI.SignedSweeps.sweepPowerCoefficient_trace line 79
  9. def OAI.SignedSweeps.columnSweepCoefficient line 93
  10. def OAI.SignedSweeps.rowSweepCoefficient line 97
  11. lemma OAI.SignedSweeps.columnSweepCoefficient_layers line 101
  12. lemma OAI.SignedSweeps.rowSweepCoefficient_layers line 109
  13. lemma OAI.SignedSweeps.columnSweepCoefficient_action line 117
  14. lemma OAI.SignedSweeps.rowSweepCoefficient_action line 123
  15. def OAI.SignedSweeps.columnPowerCoefficient line 129
  16. def OAI.SignedSweeps.rowPowerCoefficient line 133
  17. lemma OAI.SignedSweeps.columnPowerCoefficient_formula line 137
  18. lemma OAI.SignedSweeps.rowPowerCoefficient_formula line 144
  19. lemma OAI.SignedSweeps.columnPowerCoefficient_action line 151
  20. lemma OAI.SignedSweeps.rowPowerCoefficient_action line 157
  21. lemma OAI.SignedSweeps.columnPowerCoefficient_positive line 163
  22. lemma OAI.SignedSweeps.rowPowerCoefficient_positive line 171
  23. lemma OAI.SignedSweeps.columnPowerCoefficient_support line 177
  24. lemma OAI.SignedSweeps.rowPowerCoefficient_support line 185