OAI/Analysis/PlanarPacking/DirectBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Direct spectral estimates

The norm of the direct spectral kernel gives derivative bounds for cardinal functions.

  1. lemma OAI.SharpPlanar.directKernel_norm line 15
  2. lemma OAI.SharpPlanar.direct_piece_bound line 23
  3. lemma OAI.SharpPlanar.direct_positive_bound line 45