OAI/Analysis/PlanarPacking/Certificate/TailCoefficients.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Tails of the interpolation coefficients

Truncating a summable coefficient family contracts its norm. The finite rational table for OpenAI's sharp planar Fourier construction bounds the tails of the exact coefficients through the coefficient error estimate.

  1. def OAI.SharpPlanar.tailList line 16
  2. lemma OAI.SharpPlanar.tailList_apply line 21
  3. lemma OAI.SharpPlanar.tailList_norm line 23
  4. lemma OAI.SharpPlanar.tailList_contraction line 28
  5. lemma OAI.SharpPlanar.tailList_sub line 32
  6. lemma OAI.SharpPlanar.tailList_table line 36
  7. lemma OAI.SharpPlanar.tailList_table_norm line 49
  8. lemma OAI.SharpPlanar.tailList_table_bound line 59
  9. lemma OAI.SharpPlanar.exact_tail_norm line 67