OAI/Combinatorics/Progressions/Geometry/MinkowskiSecondBox.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.BohrLattice.MinkowskiSecondBox.minkowskiSecondConstant line 14
  2. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.minkowskiSecondConstant_zero line 17
  3. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.minkowskiSecondConstant_one line 20
  4. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.minkowskiSecondConstant_nonneg line 23
  5. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.exists_shortest_nonzero_of_basis line 27
  6. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.abs_det_zspan_basis_eq line 56
  7. def OAI.Erdos3.BohrLattice.MinkowskiSecondBox.intCastVec line 75
  8. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.intCastVec_zero line 78
  9. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.intCastVec_add line 83
  10. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.intCastVec_smul line 88
  11. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.mem_realBox_const_iff_norm_le line 93
  12. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.reducedLift_norm_le_two line 110
  13. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.shortest_le_two_projection line 123
  14. def OAI.Erdos3.BohrLattice.MinkowskiSecondBox.roundedCoefficient line 128
  15. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.abs_sub_roundedCoefficient_le_half line 130
  16. def OAI.Erdos3.BohrLattice.MinkowskiSecondBox.deleteProjection line 134
  17. def OAI.Erdos3.BohrLattice.MinkowskiSecondBox.deleteProjectionLinear line 138
  18. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.deleteProjectionLinear_apply line 151
  19. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.deleteProjection_add_smul line 155
  20. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.deleteProjection_self line 163
  21. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.abs_apply_le_norm line 169
  22. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.reducedLift_apply_le line 174
  23. def OAI.Erdos3.BohrLattice.MinkowskiSecondBox.tailShear line 217
  24. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.tailShear_apply_zero_zero line 225
  25. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.tailShear_apply_succ_zero line 229
  26. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.tailShear_apply_zero_succ line 233
  27. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.tailShear_apply_succ_succ line 237
  28. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.tailShear_det line 242
  29. def OAI.Erdos3.BohrLattice.MinkowskiSecondBox.projectedTail line 260
  30. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.mul_tailShear_apply_zero line 265
  31. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.mul_tailShear_apply_succ line 270
  32. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.mul_tailShear_pivot_succ line 278
  33. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.mul_tailShear_minor line 286
  34. theorem OAI.Erdos3.BohrLattice.MinkowskiSecondBox.abs_det_eq_abs_pivot_mul_abs_det_projectedTail line 292