OAI/Analysis/PlanarPacking/Entries.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Entries of the cardinal interpolation operator

The columns of the interpolation operator are cardinal basis functions, and certified quadrature controls their value and derivative entries.

  1. def OAI.SharpPlanar.columnVector line 17
  2. lemma OAI.SharpPlanar.density_column line 19
  3. lemma OAI.SharpPlanar.K_column_integral line 31
  4. lemma OAI.SharpPlanar.K_column_rule_error line 49
  5. lemma OAI.SharpPlanar.S_column_value line 56
  6. lemma OAI.SharpPlanar.S_column_derivative line 59