OAI/Analysis/PlanarPacking/Basic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Sharp Fourier certificates in the plane

The radial Schwartz certificate uses the Fourier kernel exp (-2πi⟪x, ξ⟫) and the sharp triangular packing normalization.

  1. def OAI.SharpPlanar.Radial line 21

    Also declared: ComparatorChallenges/PlanarPacking.lean:19 (same declaration text).

  2. def OAI.SharpPlanar.fourier line 25

    Also declared: ComparatorChallenges/PlanarPacking.lean:23 (same declaration text).

  3. def OAI.SharpPlanar.SharpCertificate line 30

    Also declared: ComparatorChallenges/PlanarPacking.lean:28 (same declaration text).