OAI/Geometry/NodalSets/Elliptic/SeedAmbientHarmonic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Yau.Target.seed_second_eq_iterated line 13
  2. lemma OAI.Yau.Target.seedZ1_basis line 21
  3. lemma OAI.Yau.Target.seedZ2_basis line 25
  4. lemma OAI.Yau.Target.seedQuadratic_isotropic line 29
  5. lemma OAI.Yau.Target.seedQuadratic_trace line 35
  6. lemma OAI.Yau.Target.ambientComplexSeed_laplacian line 43
  7. lemma OAI.Yau.Target.ambientRealSeed_laplacian line 53
  8. lemma OAI.Yau.Target.ambientRealSeed_harmonic line 61