OAI/NumberTheory/TwoPoint/Bounds/ShortBlockPartition.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The actual subdivision of perfect intervals into short blocks.

  1. def OAI.TwoPointCorrelations.shortBlockLengths line 12
  2. lemma OAI.TwoPointCorrelations.shortBlockLengths_sum line 14
  3. def OAI.TwoPointCorrelations.shortBlocks line 17
  4. theorem OAI.TwoPointCorrelations.shortBlocks_flatten line 20
  5. theorem OAI.TwoPointCorrelations.shortBlocks_length line 23
  6. theorem OAI.TwoPointCorrelations.shortBlocks_size line 27
  7. theorem OAI.TwoPointCorrelations.shortBlocks_infix line 36
  8. def OAI.TwoPointCorrelations.subdivideColumnChunks line 44

    Source documentation

    Imperfect positions stay single; perfect intervals are split into full blocks of size s and one possible final shorter block. Empty final blocks are harmless and are included in the upper bound.

    def subdivideColumnChunks (s : ℕ) (chunks : List (List α ⊕ α)) : List (List α ⊕ α) :=
…
  9. lemma OAI.TwoPointCorrelations.columnChunkEntries_map_inl line 47
  10. lemma OAI.TwoPointCorrelations.columnChunkEntries_append line 55
  11. theorem OAI.TwoPointCorrelations.subdivideColumnChunks_entries line 60

    Source documentation

    Subdivision preserves every position, including its perfect/imperfect status.

    theorem subdivideColumnChunks_entries (s : ℕ) (chunks : List (List α ⊕ α)) :
    columnChunkEntries (subdivideColumnChunks s chunks) = columnChunkEntries chunks := by
…

    Mentions: OAI.TwoPointCorrelations.columnChunkEntries, OAI.TwoPointCorrelations.subdivideColumnChunks

  12. def OAI.TwoPointCorrelations.perfectChunkLength line 74
  13. lemma OAI.TwoPointCorrelations.perfectChunkCount_append line 77
  14. lemma OAI.TwoPointCorrelations.perfectChunkCount_map_inl line 81
  15. theorem OAI.TwoPointCorrelations.subdivideColumnChunks_count line 87

    Source documentation

    The number of short perfect blocks is at most the total perfect length divided by the block size, plus the number of original perfect intervals.

    theorem subdivideColumnChunks_count (s : ℕ) (chunks : List (List α ⊕ α)) :
    perfectChunkCount (subdivideColumnChunks s chunks) ≤
      perfectChunkLength chunks / s + perfectChunkCount chunks := by
…

    Mentions: OAI.TwoPointCorrelations.perfectChunkCount, OAI.TwoPointCorrelations.subdivideColumnChunks, OAI.TwoPointCorrelations.perfectChunkLength