OAI/Geometry/NodalSets/Waves/GaussianJet.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Yau.Geometry.JetSpace line 12
  2. def OAI.Yau.Geometry.normalizedRealJet line 14
  3. lemma OAI.Yau.Geometry.normalizedRealJet_inner line 18
  4. def OAI.Yau.Geometry.jetWaveCoefficients line 30
  5. lemma OAI.Yau.Geometry.gaussianWaveField_normalizedJet line 34
  6. lemma OAI.Yau.Geometry.normalizedRealJet_add line 46
  7. lemma OAI.Yau.Geometry.seeded_gaussian_jet_eq line 55
  8. lemma OAI.Yau.Geometry.seeded_gaussian_jet_law line 64
  9. lemma OAI.Yau.Geometry.seeded_gaussian_jet_variance line 75