OAI/Geometry/SmoothYau/Spectrum/ThreeCoupledNormedSpace.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.YauCounterexamples.productAxis line 13
  2. lemma OAI.YauCounterexamples.productAxis_inner line 14
  3. lemma OAI.YauCounterexamples.productAxis_coord line 16
  4. lemma OAI.YauCounterexamples.productAxis_norm line 18
  5. def OAI.YauCounterexamples.productA line 19
  6. def OAI.YauCounterexamples.productB line 20
  7. lemma OAI.YauCounterexamples.productA_re line 21
  8. lemma OAI.YauCounterexamples.productA_im line 22
  9. lemma OAI.YauCounterexamples.productB_re line 23
  10. lemma OAI.YauCounterexamples.productB_im line 24
  11. lemma OAI.YauCounterexamples.productAB_nonzero line 25
  12. def OAI.YauCounterexamples.threeCoupledComplex line 36
  13. def OAI.YauCounterexamples.threeCoupled line 38
  14. lemma OAI.YauCounterexamples.threeCoupled_eq line 39
  15. lemma OAI.YauCounterexamples.threeCoupled_smooth line 44
  16. lemma OAI.YauCounterexamples.product_laplace_const_mul line 48
  17. lemma OAI.YauCounterexamples.product_laplace_linear_eigen line 57
  18. lemma OAI.YauCounterexamples.threeCoupled_eigen line 69
  19. lemma OAI.YauCounterexamples.threeCoupled_chart_smooth line 82
  20. lemma OAI.YauCounterexamples.threeCoupled_chart_first line 89