OAI/Analysis/PlanarPacking/TableKBridge.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quadrature bounds for finite cardinal kernels

Certified quadrature and the finite coefficient densities control the cardinal kernel integrals.

  1. lemma OAI.SharpPlanar.normalized_kernel line 15
  2. lemma OAI.SharpPlanar.tableMomentK_eq line 20