OAI/Computability/FourierTransform/SectorPacking.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Sector partitions of arbitrary sequences of pair slots.

  1. structure OAI.PowerSaving.Grove.Reloc line 12

    Source documentation

    helper for Nat ranged permutations

    structure Reloc (n : ℕ) (q : ℕ → ℕ) : Prop where
…
  2. def OAI.PowerSaving.Grove.seek line 16
  3. lemma OAI.PowerSaving.Grove.Reloc.onto line 23
  4. lemma OAI.PowerSaving.Grove.Reloc.seeks line 32
  5. lemma OAI.PowerSaving.Grove.Reloc.seeks_at line 38
  6. lemma OAI.PowerSaving.Grove.Reloc.sum line 42
  7. lemma OAI.PowerSaving.Grove.Reloc.sow line 50
  8. structure OAI.PowerSaving.Grove.Shard line 64
  9. def OAI.PowerSaving.Grove.Shard.tip line 73
  10. def OAI.PowerSaving.Grove.Shard.addr line 74
  11. structure OAI.PowerSaving.Grove.Shard.Mark line 76
  12. lemma OAI.PowerSaving.Grove.Shard.Mark.small line 84
  13. lemma OAI.PowerSaving.Grove.Shard.Mark.positive line 86
  14. lemma OAI.PowerSaving.Grove.Shard.Mark.starts line 87
  15. def OAI.PowerSaving.Grove.Shard.same line 91
  16. def OAI.PowerSaving.Grove.Shard.fits line 94
  17. structure OAI.PowerSaving.Grove.Shard.Quilt line 97
  18. def OAI.PowerSaving.Grove.Shard.patch line 103

    Source documentation

    Metadata on packed indices; never computed by inversion, only used for proofs.

    def patch (n : ℕ) (f : ℕ → Shard) (j : ℕ) :=
…

    Mentions: OAI.PowerSaving.Grove.Shard

  19. lemma OAI.PowerSaving.Grove.Shard.Quilt.reloc line 109
  20. lemma OAI.PowerSaving.Grove.Shard.Quilt.aligns line 112
  21. lemma OAI.PowerSaving.Grove.Shard.Quilt.matches_of_eq line 117
  22. lemma OAI.PowerSaving.Grove.Shard.Quilt.patch_addr line 123
  23. lemma OAI.PowerSaving.Grove.Shard.Quilt.patch_mark line 126
  24. lemma OAI.PowerSaving.Grove.Shard.Quilt.patch_at line 129
  25. lemma OAI.PowerSaving.Grove.Shard.Quilt.patch_seam line 132
  26. lemma OAI.PowerSaving.Grove.Shard.Quilt.patch_align line 136
  27. def OAI.PowerSaving.Grove.Shard.fringe line 153

    Source documentation

    composition of sector metadata under extension of an axis.

    def fringe (r : ℕ) (s t : Shard) : Shard :=
…

    Mentions: OAI.PowerSaving.Grove.Shard

  28. lemma OAI.PowerSaving.Grove.Shard.fr_tip line 157
  29. lemma OAI.PowerSaving.Grove.Shard.tip_steps line 161
  30. lemma OAI.PowerSaving.Grove.Shard.Mark.fringe line 167
  31. lemma OAI.PowerSaving.Grove.Shard.fr_same line 179
  32. lemma OAI.PowerSaving.Grove.Shard.fr_before line 184
  33. lemma OAI.PowerSaving.Grove.Shard.fr_within line 188
  34. lemma OAI.PowerSaving.Grove.Shard.same_sym line 193
  35. lemma OAI.PowerSaving.Grove.Shard.fr_fits line 196
  36. lemma OAI.PowerSaving.Grove.Shard.fr_unique line 207
  37. def OAI.PowerSaving.Grove.Shard.attach line 220
  38. lemma OAI.PowerSaving.Grove.Shard.Quilt.attach line 223
  39. def OAI.PowerSaving.Grove.Hem.crown line 268
  40. def OAI.PowerSaving.Grove.Hem.thickness line 269
  41. def OAI.PowerSaving.Grove.Hem.up line 270
  42. def OAI.PowerSaving.Grove.Hem.trim line 271
  43. def OAI.PowerSaving.Grove.Hem.tier line 272
  44. def OAI.PowerSaving.Grove.Hem.sums line 273
  45. def OAI.PowerSaving.Grove.Hem.hem line 275
  46. lemma OAI.PowerSaving.Grove.Hem.crown_partner line 280
  47. lemma OAI.PowerSaving.Grove.Hem.thickness_partner line 283
  48. lemma OAI.PowerSaving.Grove.Hem.crown_closed line 287
  49. lemma OAI.PowerSaving.Grove.Hem.crown_class line 293
  50. lemma OAI.PowerSaving.Grove.Hem.thick_tip line 305
  51. lemma OAI.PowerSaving.Grove.Hem.tier_lt line 312
  52. lemma OAI.PowerSaving.Grove.Hem.sum_trim line 318
  53. lemma OAI.PowerSaving.Grove.Hem.tip_hem line 334
  54. lemma OAI.PowerSaving.Grove.Hem.sums_mono line 339
  55. lemma OAI.PowerSaving.Grove.Hem.marked line 343
  56. lemma OAI.PowerSaving.Grove.Hem.same_class line 351
  57. lemma OAI.PowerSaving.Grove.Hem.hem_before line 358
  58. lemma OAI.PowerSaving.Grove.Hem.class_of_start line 362
  59. lemma OAI.PowerSaving.Grove.Hem.tier_partner_ne line 370
  60. lemma OAI.PowerSaving.Grove.Hem.quilt line 374
  61. def OAI.PowerSaving.Grove.seed line 400
  62. def OAI.PowerSaving.Grove.mosaic line 401
  63. lemma OAI.PowerSaving.Grove.seed_quilt line 405
  64. lemma OAI.PowerSaving.Grove.mosaic_quilt line 409