OAI/Analysis/PlanarPacking/Main.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpPlanar.normalizedCandidate_nonpos line 7
2. lemma OAI.SharpPlanar.normalizedCandidate_fourier_nonneg line 16
3. lemma OAI.SharpPlanar.normalizedCandidate_certificate line 25
4. theorem OAI.sharp_fourier_certificate line 32

   Source documentation

   A normalized radial Schwartz certificate for the sharp planar packing bound.

   Distinct definitions of this name: ComparatorChallenges/PlanarPacking.lean:36 (same statement text; different proof or body). Qualify references as OAI.sharp_fourier_certificate@path.

   theorem sharp_fourier_certificate :
       ∃ f : SchwartzMap SharpPlanar.Plane ℝ, SharpPlanar.SharpCertificate f :=
   …

   Mentions: OAI.SharpPlanar.Plane, OAI.SharpPlanar.SharpCertificate