OAI/Analysis/Cotype/ChebyshevBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Cotype.chebyshev_abs_le_one line 16
  2. theorem OAI.Cotype.chebyshev_derivative_zero_bound line 21
  3. theorem OAI.Cotype.chebyshev_pairing_bound line 32
  4. theorem OAI.Cotype.chebyshev_pairing line 45
  5. def OAI.Cotype.chebyshevExpansion line 56
  6. theorem OAI.Cotype.chebyshevExpansion_pairing line 59
  7. theorem OAI.Cotype.chebyshevExpansion_coefficient_bound line 70
  8. theorem OAI.Cotype.sum_fin_cast line 82
  9. theorem OAI.Cotype.chebyshevExpansion_derivative_bound line 93
  10. theorem OAI.Cotype.exists_chebyshevExpansion line 114
  11. theorem OAI.Cotype.polynomial_derivative_zero_bound line 132