OAI/Geometry/NodalSets/Elliptic/SeedLogarithmicBranch.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Target.seedLogDomain line 12
  2. def OAI.Yau.Target.seedLog line 14
  3. def OAI.Yau.Target.seedLogReal line 16
  4. def OAI.Yau.Target.seedLogImag line 18
  5. def OAI.Yau.Target.sphereSeedLogReal line 20
  6. def OAI.Yau.Target.sphereSeedLogImag line 22
  7. lemma OAI.Yau.Target.seedLogDomain_open line 24
  8. lemma OAI.Yau.Target.seedPoint_mem_logDomain line 27
  9. lemma OAI.Yau.Target.seedLog_contDiffAt line 29
  10. lemma OAI.Yau.Target.seedLog_hasFDerivAt line 33
  11. lemma OAI.Yau.Target.seedLog_fderiv line 38
  12. lemma OAI.Yau.Target.seedLogReal_hasFDerivAt line 43
  13. lemma OAI.Yau.Target.seedLogImag_hasFDerivAt line 48
  14. lemma OAI.Yau.Target.sphereSeedLogReal_smoothAt line 53
  15. lemma OAI.Yau.Target.sphereSeedLogImag_smoothAt line 58
  16. lemma OAI.Yau.Target.ambientSeed_exp_log line 63
  17. lemma OAI.Yau.Target.ambientSeed_log_trigonometric line 68
  18. lemma OAI.Yau.Target.sphericalSeed_log_trigonometric line 73