OAI/Combinatorics/Progressions/Lattices/TriangularAffineReset.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.earlierSlotMatrix_apply_lt line 15
  2. theorem OAI.Erdos3.unitLower_mulVec line 29
  3. def OAI.Erdos3.reducedLatticeColumn line 49
  4. def OAI.Erdos3.triangularReductionMatrix line 57
  5. theorem OAI.Erdos3.triangularReductionMatrix_above line 60
  6. theorem OAI.Erdos3.triangularReductionMatrix_diag line 66
  7. theorem OAI.Erdos3.triangularReductionMatrix_det line 72
  8. def OAI.Erdos3.reducedTriangularMatrix line 77
  9. theorem OAI.Erdos3.reducedTriangularMatrix_entry line 81
  10. theorem OAI.Erdos3.reducedTriangularMatrix_above line 88
  11. theorem OAI.Erdos3.reducedTriangularMatrix_diag line 98
  12. theorem OAI.Erdos3.reducedTriangularMatrix_lower_bound line 111
  13. theorem OAI.Erdos3.reducedTriangularMatrix_bound line 124
  14. def OAI.Erdos3.integerMatrixEquiv line 133
  15. theorem OAI.Erdos3.one_sub_unitLower_strict line 152
  16. def OAI.Erdos3.TriangularSlots.unitLowerBlock line 160
  17. theorem OAI.Erdos3.TriangularSlots.unitLowerBlock_residual line 165
  18. def OAI.Erdos3.triangularLatticeValue line 173
  19. theorem OAI.Erdos3.triangularLatticeValue_eq_patchValue line 177
  20. theorem OAI.Erdos3.triangularLatticeValue_mem_Icc line 184
  21. theorem OAI.Erdos3.bounded_matrix_mulVec_lipschitz line 191
  22. theorem OAI.Erdos3.triangularLatticeValue_lipschitz line 211
  23. theorem OAI.Erdos3.triangularLatticeValue_integer_periodic line 233
  24. theorem OAI.Erdos3.integerMatrixEquiv_cast line 259
  25. theorem OAI.Erdos3.integerMatrix_cast_mul_inv line 266
  26. theorem OAI.Erdos3.integer_basis_change_residual line 272
  27. theorem OAI.Erdos3.real_basis_change_residual line 281
  28. theorem OAI.Erdos3.triangularLatticeValue_change_basis line 290
  29. theorem OAI.Erdos3.matrix_mulVec_affine line 302
  30. theorem OAI.Erdos3.triangular_affine_density_increment line 309