OAI/Analysis/PlanarPacking/ContactData.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Contact data for cardinal interpolation

The prescribed contacts and their Gaussian transforms give summable right hand sides for the interpolation equations.

  1. def OAI.SharpPlanar.transformedJets line 13
  2. def OAI.SharpPlanar.dataMass line 16
  3. lemma OAI.SharpPlanar.dataMass_nonneg line 18
  4. lemma OAI.SharpPlanar.transformedJets_bound line 22
  5. lemma OAI.SharpPlanar.transformedJets_summable line 55
  6. def OAI.SharpPlanar.transformedJetList line 58
  7. def OAI.SharpPlanar.firstNode line 60
  8. def OAI.SharpPlanar.contactList line 61
  9. def OAI.SharpPlanar.gā‚ line 62
  10. def OAI.SharpPlanar.gā‚‚ line 63