OAI/Analysis/Crouzeix/DiskCalculus.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Disk Calculus.

  1. abbrev OAI.CrouzeixHilbert.Disk.CircleSpace line 18
  2. abbrev OAI.CrouzeixHilbert.Disk.σ line 22
  3. theorem OAI.CrouzeixHilbert.Disk.inverse_one_sub_of_summable line 29
  4. lemma OAI.CrouzeixHilbert.Disk.norm_fourier line 37
  5. lemma OAI.CrouzeixHilbert.Disk.fourier_one_pow line 39
  6. lemma OAI.CrouzeixHilbert.Disk.inverse_fourier_pow line 45
  7. lemma OAI.CrouzeixHilbert.Disk.summable_diskPowers line 49
  8. lemma OAI.CrouzeixHilbert.Disk.disk_inverse_series line 56
  9. lemma OAI.CrouzeixHilbert.Disk.continuous_diskInverse line 62
  10. lemma OAI.CrouzeixHilbert.Disk.integral_fourier line 70
  11. lemma OAI.CrouzeixHilbert.Disk.integral_fourier_smul line 75
  12. lemma OAI.CrouzeixHilbert.Disk.integral_fourier_series line 80
  13. def OAI.CrouzeixHilbert.Disk.phi line 96
  14. theorem OAI.CrouzeixHilbert.Disk.continuous_phi line 100
  15. theorem OAI.CrouzeixHilbert.Disk.integrable_phi line 103
  16. lemma OAI.CrouzeixHilbert.Disk.phi_series line 106
  17. theorem OAI.CrouzeixHilbert.Disk.integral_moment line 112
  18. theorem OAI.CrouzeixHilbert.Disk.integral_phi line 152
  19. theorem OAI.CrouzeixHilbert.Disk.phi_isPositive line 163