OAI/Analysis/DirectCrouzeix/TaylorFourier.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectCrouzeix.Faber.taylorCoeff line 19
  2. theorem OAI.DirectCrouzeix.Faber.taylorCoeff_zero line 22
  3. theorem OAI.DirectCrouzeix.Faber.taylorCoeff_congr line 25
  4. theorem OAI.DirectCrouzeix.Faber.taylorCoeff_add line 29
  5. theorem OAI.DirectCrouzeix.Faber.taylorCoeff_sum line 34
  6. theorem OAI.DirectCrouzeix.Faber.taylorCoeff_smul_const line 40
  7. theorem OAI.DirectCrouzeix.Faber.taylorCoeff_const line 45
  8. theorem OAI.DirectCrouzeix.Faber.taylorCoeff_pow_mul line 51
  9. theorem OAI.DirectCrouzeix.Faber.taylorCoeff_eq_series line 77
  10. abbrev OAI.DirectCrouzeix.Faber.Angle line 88
  11. abbrev OAI.DirectCrouzeix.Faber.angularMeasure line 90
  12. def OAI.DirectCrouzeix.Faber.unitPoint line 92
  13. theorem OAI.DirectCrouzeix.Faber.unitPoint_norm line 94
  14. theorem OAI.DirectCrouzeix.Faber.unitPoint_continuous line 97
  15. theorem OAI.DirectCrouzeix.Faber.unitPoint_pow line 99
  16. theorem OAI.DirectCrouzeix.Faber.integral_character_smul line 103
  17. theorem OAI.DirectCrouzeix.Faber.fourierCoeff_of_powerSeries line 116
  18. theorem OAI.DirectCrouzeix.Faber.fourierCoeff_of_analytic line 147