OAI/Analysis/PlanarPacking/Envelopes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Spectral derivative bounds

Monotone spectral envelopes bound the cardinal functions and their Fourier kernels. The estimates follow A sharp Fourier certificate for planar circle packing (OpenAI, 2026).

  1. lemma OAI.SharpPlanar.pieceL_antitone line 16
  2. lemma OAI.SharpPlanar.atomL_antitone line 25
  3. def OAI.SharpPlanar.directEnvelope line 31
  4. def OAI.SharpPlanar.transformEnvelope line 33
  5. def OAI.SharpPlanar.atomicEnvelope line 35
  6. lemma OAI.SharpPlanar.directEnvelope_nonneg line 37
  7. lemma OAI.SharpPlanar.transformEnvelope_nonneg line 40
  8. lemma OAI.SharpPlanar.atomicEnvelope_nonneg line 44
  9. lemma OAI.SharpPlanar.transformEnvelope_antitone line 47
  10. lemma OAI.SharpPlanar.atomicEnvelope_antitone line 52
  11. lemma OAI.SharpPlanar.Pmoment_norm_bound line 57
  12. lemma OAI.SharpPlanar.direct_spectral_bound line 74
  13. lemma OAI.SharpPlanar.direct_envelope_coarse line 94