OAI/Analysis/PlanarPacking/DataTail.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Tails of transformed contact data

Gaussian row estimates control the tails of the summable contact sequences.

  1. lemma OAI.SharpPlanar.sharp_data_row line 14
  2. lemma OAI.SharpPlanar.atom_natural_tail_summable line 51
  3. lemma OAI.SharpPlanar.atom_natural_tail_bound line 54
  4. lemma OAI.SharpPlanar.sharp_data_tail line 58