OAI/Analysis/DirectCrouzeix/FaberCalculus.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectCrouzeix.Faber.analyticAt_ringInverse line 23
  2. theorem OAI.DirectCrouzeix.Faber.ringInverse_smul line 28
  3. theorem OAI.DirectCrouzeix.Faber.ringInverse_geometric line 41
  4. theorem OAI.DirectCrouzeix.Faber.taylorCoeff_pow_smul_zero line 48
  5. def OAI.DirectCrouzeix.Faber.algebraDenominator line 65
  6. def OAI.DirectCrouzeix.Faber.algebraGenerating line 68
  7. theorem OAI.DirectCrouzeix.Faber.analyticAt_algebraDenominator line 71
  8. theorem OAI.DirectCrouzeix.Faber.analyticAt_algebraGenerating line 77
  9. theorem OAI.DirectCrouzeix.Faber.algebraGenerating_local line 83
  10. theorem OAI.DirectCrouzeix.Faber.algebraGenerating_coefficient line 94
  11. theorem OAI.DirectCrouzeix.Faber.algebraGenerating_fourier line 139
  12. theorem OAI.DirectCrouzeix.Faber.algebraDenominator_exterior line 165
  13. theorem OAI.DirectCrouzeix.Faber.algebraGenerating_exterior line 174