OAI/Combinatorics/Progressions/Lattices/IntegerFiberUniformBound.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.normalizedIntegerColumns line 14
  2. theorem OAI.Erdos3.normalizedIntegerColumns_mulVec line 18
  3. def OAI.Erdos3.normalizedPivotEquiv line 35
  4. theorem OAI.Erdos3.normalizedPivotEquiv_coe line 41
  5. theorem OAI.Erdos3.normalizedPivotEquiv_inverseJacobian line 48
  6. theorem OAI.Erdos3.scaledIntegerFiber_graph line 58
  7. def OAI.Erdos3.scaledIntegerWeight line 92
  8. theorem OAI.Erdos3.scaledIntegerWeight_eq_slice line 96
  9. theorem OAI.Erdos3.integerFiber_free_injective line 108
  10. theorem OAI.Erdos3.scaledIntegerWeight_fiber_summable line 121
  11. def OAI.Erdos3.scaledIntegerFiberOutputMass line 151
  12. def OAI.Erdos3.normalizedFiberDensity line 156
  13. theorem OAI.Erdos3.integerFiber_grid_error line 162
  14. theorem OAI.Erdos3.integerFiber_quadrature line 199
  15. theorem OAI.Erdos3.scaledIntegerFiberOutputMass_zero_off_image line 224
  16. def OAI.Erdos3.integerFiberErrorConstant line 241
  17. theorem OAI.Erdos3.integerFiberErrorConstant_nonneg line 244
  18. theorem OAI.Erdos3.integerFiber_uniform_quadrature line 250