OAI/Probability/FreeIsing/Spectral/ChebyshevRecurrence.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.power_recurrence_of_quadratic line 12
  2. theorem OAI.Problem367.pow_eq_chebyshev_of_quadratic line 23
  3. theorem OAI.Problem367.abs_sin_nat_mul_le line 44
  4. theorem OAI.Problem367.chebyshev_U_abs_le line 63
  5. theorem OAI.Problem367.chebyshev_T_abs_le line 83
  6. theorem OAI.Problem367.norm_pow_le_of_chebyshev_bound line 93
  7. theorem OAI.Problem367.norm_aeval_chebyshev_U_le line 119
  8. theorem OAI.Problem367.norm_aeval_chebyshev_T_le line 129
  9. theorem OAI.Problem367.norm_pow_le_of_selfAdjoint_quadratic line 139
  10. theorem OAI.Problem367.norm_pow_le_linear_of_selfAdjoint_quadratic line 146
  11. theorem OAI.Problem367.norm_scaled_pow_le_of_selfAdjoint_quadratic line 157
  12. theorem OAI.Problem367.summable_norm_scaled_pow_of_selfAdjoint_quadratic line 168