OAI/Analysis/DirectCrouzeix/BoundaryEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectCrouzeix.matrix_energy_split line 17
  2. theorem OAI.DirectCrouzeix.hsSq_zero line 29
  3. theorem OAI.DirectCrouzeix.hsSq_add_self line 32
  4. theorem OAI.DirectCrouzeix.fourierCoeff_add_star line 37
  5. theorem OAI.DirectCrouzeix.anti_matrix_energy line 48
  6. theorem OAI.DirectCrouzeix.anti_diagonal_energy line 57
  7. theorem OAI.DirectCrouzeix.anti_cross_energy line 72
  8. theorem OAI.DirectCrouzeix.finite_negative_bessel line 90
  9. def OAI.DirectCrouzeix.faberWeight line 106
  10. theorem OAI.DirectCrouzeix.faberWeight_pos line 108
  11. theorem OAI.DirectCrouzeix.weighted_sequence_dual line 112