OAI/Analysis/Littlewood/SlotParameters.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Parameter choices for the concrete signed-slot packing. The chunk length is chosen first and remains fixed while the prime modulus grows.

  1. def OAI.AsymptoticallyMinimalLittlewood.Packing.chunkCount line 14
  2. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.chunkCount_bounds line 16
  3. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.chunkCount_pos line 26
  4. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.chunkCount_ratio_error line 29
  5. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.chunkCount_ratio_tendsto line 45
  6. def OAI.AsymptoticallyMinimalLittlewood.Packing.packingAV line 53
  7. def OAI.AsymptoticallyMinimalLittlewood.Packing.packingNV line 60
  8. def OAI.AsymptoticallyMinimalLittlewood.Packing.packingALimit line 63
  9. def OAI.AsymptoticallyMinimalLittlewood.Packing.packingNLimit line 66
  10. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.packingAV_tendsto line 69
  11. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.packingNV_tendsto line 91
  12. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.packingALimit_tendsto line 105
  13. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.packingNLimit_tendsto line 109
  14. def OAI.AsymptoticallyMinimalLittlewood.Packing.packingBV line 117
  15. def OAI.AsymptoticallyMinimalLittlewood.Packing.packingBLimit line 120
  16. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.packingBV_nonneg line 123
  17. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.packingBV_tendsto line 127
  18. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.packingBLimit_tendsto line 135
  19. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.packing_choose_R line 141
  20. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.packing_eventual_parameters line 172
  21. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.concrete_slot_variance_le_av line 205
  22. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.concrete_slot_nv line 252