OAI/Analysis/Littlewood/Chunks.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.choose_odd_lengths line 13
  2. def OAI.AsymptoticallyMinimalLittlewood.Packing.slotPrefix line 44
  3. def OAI.AsymptoticallyMinimalLittlewood.Packing.periodLength line 46
  4. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.prefix_add_length_le line 48
  5. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.prefix_separated line 56
  6. def OAI.AsymptoticallyMinimalLittlewood.Packing.slotLeft line 70

    Source documentation

    Site immediately to the left of a slot. The actual sites are left+1,...,left+L_i. Each full chunk keeps R-1 translated periods.

    def slotLeft (L : Fin r → ℕ) (R : ℕ) (shift chunk period : ℕ) (i : Fin r) : ℕ :=
…
  7. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.slotLeft_bounds line 73
  8. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.slots_separated_same_chunk line 86
  9. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.slots_separated_chunks line 99
  10. def OAI.AsymptoticallyMinimalLittlewood.Packing.signedSite line 108
  11. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.signedSite_injective line 110
  12. abbrev OAI.AsymptoticallyMinimalLittlewood.Packing.oddLengths line 125
  13. def OAI.AsymptoticallyMinimalLittlewood.Packing.siteCenter line 127
  14. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.periodLength_pos line 130
  15. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.centerOffset_bounds line 135
  16. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.siteCenter_bounds line 142
  17. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.siteCenter_chunk line 150
  18. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.interior_center_exists line 165
  19. def OAI.AsymptoticallyMinimalLittlewood.Packing.interiorSite line 195
  20. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.interiorSite_bounds line 198
  21. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.interiorSite_chunk line 209
  22. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.interior_signed_injective line 219
  23. abbrev OAI.AsymptoticallyMinimalLittlewood.Packing.SlotChoices line 243
  24. def OAI.AsymptoticallyMinimalLittlewood.Packing.slotHit line 246
  25. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.interior_hit_coordinate line 251
  26. def OAI.AsymptoticallyMinimalLittlewood.Packing.shortResidues line 297

    Source documentation

    The finite residue neighborhood used to detect same-chunk collisions.

    def shortResidues (q B : ℕ) : Finset (ZMod q) :=
…
  27. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.shortResidues_card line 300
  28. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.same_chunk_collision line 305
  29. abbrev OAI.AsymptoticallyMinimalLittlewood.Packing.InteriorCatalog line 349
  30. def OAI.AsymptoticallyMinimalLittlewood.Packing.catalogValue line 352
  31. def OAI.AsymptoticallyMinimalLittlewood.Packing.catalogSet line 355
  32. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.catalogValue_injective line 358
  33. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.catalogSet_card line 368
  34. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.catalog_chunk_system line 375
  35. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.actual_centers_injective line 434
  36. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.slotHit_card line 464