OAI/Analysis/DirectCrouzeix/BoundaryKernel.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectCrouzeix.Faber.continuous_circle_integral line 19
  2. theorem OAI.DirectCrouzeix.Faber.continuous_slice_left line 26
  3. theorem OAI.DirectCrouzeix.Faber.continuous_slice_right line 32
  4. theorem OAI.DirectCrouzeix.Faber.fourierCoeff_integral_swap line 38
  5. theorem OAI.DirectCrouzeix.Faber.fourierCoeff_conjugate line 49
  6. def OAI.DirectCrouzeix.Faber.boundary line 57
  7. def OAI.DirectCrouzeix.Faber.boundaryCorrection line 59
  8. def OAI.DirectCrouzeix.Faber.boundaryCoefficient line 62
  9. def OAI.DirectCrouzeix.Faber.boundaryKernel line 65
  10. theorem OAI.DirectCrouzeix.Faber.unitPoint_ne_zero line 68
  11. theorem OAI.DirectCrouzeix.Faber.unitPoint_inv_mem line 71
  12. theorem OAI.DirectCrouzeix.Faber.continuous_boundary line 75
  13. theorem OAI.DirectCrouzeix.Faber.continuous_boundaryCorrection line 81
  14. theorem OAI.DirectCrouzeix.Faber.continuous_boundaryCoefficient line 95
  15. theorem OAI.DirectCrouzeix.Faber.boundaryCorrection_left_coeff line 106
  16. theorem OAI.DirectCrouzeix.Faber.boundaryCorrection_right_coeff line 116
  17. theorem OAI.DirectCrouzeix.Faber.boundaryCoefficient_eq_taylor line 126
  18. theorem OAI.DirectCrouzeix.Faber.boundaryCoefficient_zero line 133
  19. theorem OAI.DirectCrouzeix.Faber.faberBasis_boundary line 139
  20. theorem OAI.DirectCrouzeix.Faber.boundaryCoefficient_no_nonnegative line 149
  21. theorem OAI.DirectCrouzeix.Faber.continuous_boundaryKernel line 174
  22. theorem OAI.DirectCrouzeix.Faber.boundaryCorrection_marginals line 178
  23. theorem OAI.DirectCrouzeix.Faber.boundaryKernel_marginals line 191
  24. theorem OAI.DirectCrouzeix.Faber.boundaryKernel_complex line 213
  25. theorem OAI.DirectCrouzeix.Faber.boundaryKernel_character line 217