ShortColumnBlocks.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The actual short perfect blocks of a finite column, with all positions and budgets.

def OAI.TwoPointCorrelations.columnNatLabel line 13
def OAI.TwoPointCorrelations.columnNatPerfect line 16
theorem OAI.TwoPointCorrelations.columnNatLabel_fin line 19
theorem OAI.TwoPointCorrelations.columnNatPerfect_fin line 23
theorem OAI.TwoPointCorrelations.range_map_eq_ofFn line 27
def OAI.TwoPointCorrelations.shortColumnChunks line 31
theorem OAI.TwoPointCorrelations.shortColumnChunks_entries line 36

theorem OAI.TwoPointCorrelations.shortColumnChunks_blocks line 47

Source documentation

The short blocks used by the decoder are actual intervals, all of length at most s. Their count and total length satisfy the original position budgets, before any quotient geometry is used.

theorem shortColumnChunks_blocks (label : Fin n → α) (hn : 0 < n)
    (perfect : Finset (Fin n)) (s : ℕ) (hs : 0 < s) :
    ∃ blocks : List (ℕ × ℕ),
      (shortColumnChunks label hn perfect s).filterMap (Sum.elim some (fun _ => none)) =
        blocks.map (fun b => blockLabelList (columnNatLabel label hn) b.1 b.2) ∧
      (blocks.map Prod.snd).sum ≤ n ∧
      blocks.length ≤ n / s + ((columnPositionEntries perfect).filter (fun p => !p.2)).length + 1 ∧
      ∀ b ∈ blocks, b.1 + b.2 ≤ n ∧ b.2 ≤ s ∧
        ∀ t ∈ intervalPositions b, columnNatPerfect perfect t = true := by
…

Mentions: OAI.TwoPointCorrelations.shortColumnChunks, OAI.TwoPointCorrelations.blockLabelList, OAI.TwoPointCorrelations.columnNatLabel, OAI.TwoPointCorrelations.columnPositionEntries, OAI.TwoPointCorrelations.intervalPositions, OAI.TwoPointCorrelations.columnNatPerfect