OAI/Geometry/NodalSets/Elliptic/SphericalSeed.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Yau.Target.SeedAmbient line 12
  2. def OAI.Yau.Target.seedCoordinate line 15
  3. def OAI.Yau.Target.seedZ1 line 18
  4. def OAI.Yau.Target.seedZ2 line 20
  5. def OAI.Yau.Target.seedQuadratic line 22
  6. def OAI.Yau.Target.ambientComplexSeed line 24
  7. def OAI.Yau.Target.ambientRealSeed line 26
  8. def OAI.Yau.Target.sphericalSeed line 28
  9. def OAI.Yau.Target.seedEigenvalue line 30
  10. lemma OAI.Yau.Target.seedZ1_apply line 32
  11. lemma OAI.Yau.Target.seedZ2_apply line 33
  12. lemma OAI.Yau.Target.sphericalSeed_literal line 35
  13. lemma OAI.Yau.Target.seedQuadratic_contDiff line 39
  14. lemma OAI.Yau.Target.ambientComplexSeed_contDiff line 42
  15. lemma OAI.Yau.Target.ambientRealSeed_contDiff line 45
  16. lemma OAI.Yau.Target.sphericalSeed_smooth line 48
  17. lemma OAI.Yau.Target.ambientComplexSeed_homogeneous line 51
  18. lemma OAI.Yau.Target.ambientRealSeed_homogeneous line 57
  19. lemma OAI.Yau.Target.seedEigenvalue_degree line 61
  20. lemma OAI.Yau.Target.seedEigenvalue_pos line 64