OAI/Analysis/PlanarPacking/TableDensityBase.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite cardinal densities

Finite rational coefficient families determine the densities used in the quadrature estimates.

  1. def OAI.SharpPlanar.tableNum line 17
  2. lemma OAI.SharpPlanar.tableNum_coefficient line 22
  3. lemma OAI.SharpPlanar.scaled_table_basis line 27
  4. def OAI.SharpPlanar.tableDensity line 37
  5. lemma OAI.SharpPlanar.tableDensity_weighted line 40
  6. lemma OAI.SharpPlanar.cached_density_rule_contains line 50
  7. lemma OAI.SharpPlanar.table_range_mass line 73