OAI/Analysis/DirectCrouzeix/FaberEnergy.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectCrouzeix.Faber.faberBoundarySeries line 23
  2. def OAI.DirectCrouzeix.Faber.boundaryRemainder line 26
  3. def OAI.DirectCrouzeix.Faber.nonconstantCoefficients line 29
  4. theorem OAI.DirectCrouzeix.Faber.continuous_boundaryRemainder line 32
  5. theorem OAI.DirectCrouzeix.Faber.faberBoundarySeries_decomp line 37
  6. theorem OAI.DirectCrouzeix.Faber.boundaryRemainder_no_nonnegative line 46
  7. theorem OAI.DirectCrouzeix.Faber.boundaryKernel_action line 56
  8. theorem OAI.DirectCrouzeix.Faber.faber_hilbert_coefficient_bounds line 77
  9. theorem OAI.DirectCrouzeix.Faber.re_circle_fraction line 114
  10. def OAI.DirectCrouzeix.Faber.boundaryNormal line 129
  11. theorem OAI.DirectCrouzeix.Faber.scalarGenerating_exterior line 132
  12. theorem OAI.DirectCrouzeix.Faber.reciprocal_fraction line 140
  13. theorem OAI.DirectCrouzeix.Faber.unitPoint_injective line 147
  14. theorem OAI.DirectCrouzeix.Faber.boundaryCorrection_identity line 153
  15. theorem OAI.DirectCrouzeix.Faber.boundaryKernel_nonneg_off_diagonal line 171
  16. theorem OAI.DirectCrouzeix.Faber.circle_nonneg_of_off_point line 185
  17. theorem OAI.DirectCrouzeix.Faber.boundaryKernel_nonnegative line 199