OAI/Analysis/Commutator/FejerTest.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Kadison.FejerTest.sum_fin_val line 15
  2. lemma OAI.Kadison.FejerTest.hankel_average line 24
  3. lemma OAI.Kadison.FejerTest.triangular_count line 34
  4. def OAI.Kadison.FejerTest.powerAverage line 51
  5. def OAI.Kadison.FejerTest.testPolynomial line 54
  6. lemma OAI.Kadison.FejerTest.norm_powerAverage_le line 57
  7. lemma OAI.Kadison.FejerTest.testPolynomial_selfAdjoint line 76
  8. lemma OAI.Kadison.FejerTest.norm_testPolynomial_le line 82
  9. def OAI.Kadison.FejerTest.HaarMoments line 104
  10. lemma OAI.Kadison.FejerTest.moment_power line 112
  11. lemma OAI.Kadison.FejerTest.moment_square_shift line 116
  12. lemma OAI.Kadison.FejerTest.moment_square line 128
  13. lemma OAI.Kadison.FejerTest.moment_testPolynomial line 134
  14. lemma OAI.Kadison.FejerTest.positive_coefficient line 139
  15. lemma OAI.Kadison.FejerTest.preGNS_mul_norm_le line 150
  16. lemma OAI.Kadison.FejerTest.norm_preGNS_one line 158
  17. lemma OAI.Kadison.FejerTest.norm_preGNS_powerAverage line 161
  18. lemma OAI.Kadison.FejerTest.norm_preGNS_testPolynomial line 169