OAI/Analysis/DirectCrouzeix/FaberPolynomials.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectCrouzeix.Faber.localL line 19
  2. def OAI.DirectCrouzeix.Faber.localW line 21
  3. def OAI.DirectCrouzeix.Faber.localN line 23
  4. def OAI.DirectCrouzeix.Faber.faberBasis line 25
  5. theorem OAI.DirectCrouzeix.Faber.analyticAt_localL line 29
  6. theorem OAI.DirectCrouzeix.Faber.analyticAt_localW line 34
  7. theorem OAI.DirectCrouzeix.Faber.analyticAt_localN line 37
  8. theorem OAI.DirectCrouzeix.Faber.localL_zero line 41
  9. theorem OAI.DirectCrouzeix.Faber.localW_zero line 43
  10. theorem OAI.DirectCrouzeix.Faber.localN_zero line 45
  11. theorem OAI.DirectCrouzeix.Faber.faberBasis_coeff line 48
  12. theorem OAI.DirectCrouzeix.Faber.faberBasis_zero line 54
  13. theorem OAI.DirectCrouzeix.Faber.faberBasis_top_coeff line 57
  14. theorem OAI.DirectCrouzeix.Faber.faberBasis_degree line 66
  15. theorem OAI.DirectCrouzeix.Faber.faberBasis_eval line 75
  16. def OAI.DirectCrouzeix.Faber.scalarGenerating line 80
  17. theorem OAI.DirectCrouzeix.Faber.analyticAt_scalarGenerating line 83
  18. theorem OAI.DirectCrouzeix.Faber.scalarGenerating_eq_local line 89
  19. theorem OAI.DirectCrouzeix.Faber.scalarGenerating_coefficient line 95
  20. theorem OAI.DirectCrouzeix.Faber.taylorCoeff_geometric line 141
  21. theorem OAI.DirectCrouzeix.Faber.faberBasis_exterior line 158
  22. theorem OAI.DirectCrouzeix.Faber.unitPoint_neg line 179
  23. theorem OAI.DirectCrouzeix.Faber.fourierCoeff_comp_neg line 182
  24. theorem OAI.DirectCrouzeix.Faber.fourierCoeff_of_antianalytic line 191