OAI/Analysis/PlanarPacking/NormalizedCandidate.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Normalization of the radial Schwartz Fourier pair

  1. def OAI.SharpPlanar.normalizationConstant line 12
  2. lemma OAI.SharpPlanar.normalizationConstant_pos line 13
  3. def OAI.SharpPlanar.normalizedCandidate line 14
  4. lemma OAI.SharpPlanar.normalizedCandidate_apply line 16
  5. lemma OAI.SharpPlanar.exactLeft_radial line 18
  6. lemma OAI.SharpPlanar.normalizedCandidate_radial line 21
  7. lemma OAI.SharpPlanar.normalizedCandidate_origin line 25
  8. lemma OAI.SharpPlanar.fourier_eq_fourierIntegral line 32
  9. lemma OAI.SharpPlanar.normalizedCandidate_fourier line 39
  10. lemma OAI.SharpPlanar.normalizedCandidate_fourier_origin line 49
  11. lemma OAI.SharpPlanar.normalizedCandidate_fourier_real line 52