OAI/Geometry/LatticeCovering/Chains.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleLatticeCovering.Vertical.concat line 41
  2. lemma OAI.SingleLatticeCovering.Vertical.append_injective line 46
  3. lemma OAI.SingleLatticeCovering.Vertical.mem_concat line 55
  4. lemma OAI.SingleLatticeCovering.Vertical.suffixBinary_subset line 67
  5. theorem OAI.SingleLatticeCovering.Vertical.suffixBinary_concat line 76
  6. structure OAI.SingleLatticeCovering.Vertical.Block line 122
  7. abbrev OAI.SingleLatticeCovering.Vertical.Block.Group line 133
  8. abbrev OAI.SingleLatticeCovering.Vertical.Block.Vec line 134
  9. instance OAI.SingleLatticeCovering.Vertical.Block.(instance at line 135) line 135
  10. def OAI.SingleLatticeCovering.Vertical.Block.lattice line 137
  11. def OAI.SingleLatticeCovering.Vertical.Block.g line 140
  12. def OAI.SingleLatticeCovering.Vertical.Block.grid line 144
  13. def OAI.SingleLatticeCovering.Vertical.Block.weight line 147
  14. def OAI.SingleLatticeCovering.Vertical.Block.det line 150
  15. lemma OAI.SingleLatticeCovering.Vertical.Block.g_nonneg line 152
  16. lemma OAI.SingleLatticeCovering.Vertical.Block.weight_pos line 159
  17. lemma OAI.SingleLatticeCovering.Vertical.Block.weight_bits line 164
  18. lemma OAI.SingleLatticeCovering.Vertical.Block.cell line 177
  19. def OAI.SingleLatticeCovering.Vertical.Block.shift line 203
  20. lemma OAI.SingleLatticeCovering.Vertical.Block.shift_grid_bits line 206
  21. inductive OAI.SingleLatticeCovering.Vertical.Chain line 249
  22. abbrev OAI.SingleLatticeCovering.Vertical.Chain.dim line 257
  23. abbrev OAI.SingleLatticeCovering.Vertical.Chain.Vec line 261
  24. def OAI.SingleLatticeCovering.Vertical.Chain.last line 263
  25. def OAI.SingleLatticeCovering.Vertical.Chain.subLast line 267
  26. lemma OAI.SingleLatticeCovering.Vertical.Chain.last_subLast line 272
  27. def OAI.SingleLatticeCovering.Vertical.Chain.RawMem line 277
  28. def OAI.SingleLatticeCovering.Vertical.Chain.weight line 285
  29. def OAI.SingleLatticeCovering.Vertical.Chain.Residual line 293
  30. def OAI.SingleLatticeCovering.Vertical.Chain.coefficient line 303
  31. def OAI.SingleLatticeCovering.Vertical.Chain.Good line 308
  32. lemma OAI.SingleLatticeCovering.Vertical.Chain.coefficient_nonneg line 317
  33. lemma OAI.SingleLatticeCovering.Vertical.Chain.weight_pos line 324
  34. lemma OAI.SingleLatticeCovering.Vertical.Chain.base_pattern line 329
  35. theorem OAI.SingleLatticeCovering.Vertical.Chain.truncated_patterns line 362
  36. def OAI.SingleLatticeCovering.Vertical.blockLoss line 422
  37. def OAI.SingleLatticeCovering.Vertical.Regular line 425
  38. lemma OAI.SingleLatticeCovering.Vertical.regular_mean line 433
  39. theorem OAI.SingleLatticeCovering.Vertical.block_preparation line 441
  40. def OAI.SingleLatticeCovering.Vertical.Block.roundingLoss line 500
  41. lemma OAI.SingleLatticeCovering.Vertical.Block.roundingLoss_nonneg line 501
  42. def OAI.SingleLatticeCovering.Vertical.Chain.first line 508
  43. def OAI.SingleLatticeCovering.Vertical.Chain.Every line 512
  44. lemma OAI.SingleLatticeCovering.Vertical.Chain.every_last line 516
  45. lemma OAI.SingleLatticeCovering.Vertical.Chain.every_mono line 520
  46. def OAI.SingleLatticeCovering.Vertical.Chain.blockSum line 526
  47. lemma OAI.SingleLatticeCovering.Vertical.Chain.blockSum_nonneg line 530
  48. lemma OAI.SingleLatticeCovering.Vertical.Chain.blockSum_le line 535
  49. lemma OAI.SingleLatticeCovering.Vertical.Chain.blockSum_mul line 540
  50. def OAI.SingleLatticeCovering.Vertical.Chain.Halving line 546
  51. theorem OAI.SingleLatticeCovering.Vertical.Chain.inverse_power_sum line 551
  52. lemma OAI.SingleLatticeCovering.Vertical.Chain.mul_deficit line 576
  53. theorem OAI.SingleLatticeCovering.Vertical.Chain.coefficient_bounds line 582
  54. def OAI.SingleLatticeCovering.Vertical.nextSize line 628
  55. lemma OAI.SingleLatticeCovering.Vertical.nextSize_relation line 630
  56. lemma OAI.SingleLatticeCovering.Vertical.eventually_nextSize_half line 638
  57. def OAI.SingleLatticeCovering.Vertical.Chain.CeilingSizes line 653
  58. theorem OAI.SingleLatticeCovering.Vertical.hierarchy_preparation line 660