OAI/Combinatorics/SumProduct/Alignment/LagrangeBounds01.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RoughCharacterThinning.progressionIndex line 29
  2. lemma OAI.RoughCharacterThinning.progressionIndex_val line 33
  3. theorem OAI.RoughCharacterThinning.common_character_from_discrepancies line 56
  4. def OAI.LagrangeBounds.nodes line 156
  5. lemma OAI.LagrangeBounds.nodes_mem line 158
  6. lemma OAI.LagrangeBounds.nodes_separated line 167
  7. lemma OAI.LagrangeBounds.nodes_injective line 192
  8. theorem OAI.LagrangeBounds.uniform_integer_interpolation line 205
  9. def OAI.LagrangeBounds.coefficientBound line 229
  10. lemma OAI.LagrangeBounds.coefficientBound_nonneg line 232
  11. lemma OAI.LagrangeBounds.polynomial_growth line 235
  12. theorem OAI.LagrangeBounds.derivative_interpolation_error line 251