OAI/Geometry/SmoothYau/Spectrum/BilinearTransverse.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.bilinearTransverse line 10
  2. lemma OAI.YauCounterexamples.bilinearTransverse_apply line 12
  3. lemma OAI.YauCounterexamples.bilinearTransverse_kernel line 15
  4. lemma OAI.YauCounterexamples.bilinearTransverse_orthogonal line 18
  5. lemma OAI.YauCounterexamples.bilinearTransverse_fixed line 23
  6. lemma OAI.YauCounterexamples.bilinearTransverse_selfAdjoint line 26
  7. lemma OAI.YauCounterexamples.bilinearTransverse_pair line 32
  8. lemma OAI.YauCounterexamples.bilinearTransverse_trace line 39
  9. def OAI.YauCounterexamples.bilinearPinning line 47
  10. lemma OAI.YauCounterexamples.bilinearPinning_selfAdjoint line 50
  11. lemma OAI.YauCounterexamples.bilinearPinning_kernel line 57
  12. lemma OAI.YauCounterexamples.bilinearPinning_trace line 64
  13. lemma OAI.YauCounterexamples.bilinearPinning_quadratic line 71