OAI/Analysis/PlanarPacking/TableNorms.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Norm bounds for the rational coefficient family

Finite rational sums give bounds for the mass of the cardinal coefficients.

  1. def OAI.SharpPlanar.tableCoordRat line 14
  2. def OAI.SharpPlanar.tableFiniteNormRat line 16
  3. lemma OAI.SharpPlanar.tableList_norm line 17
  4. lemma OAI.SharpPlanar.table_coeff_mass line 30
  5. lemma OAI.SharpPlanar.table_constant_bound line 39