OAI/NumberTheory/TwoPoint/Walks/ColumnNameTransport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Transport the actual run decomposition to its canonical class names.

  1. theorem OAI.TwoPointCorrelations.columnRunHeads_map line 11
  2. theorem OAI.TwoPointCorrelations.columnChunkRuns_map line 18
  3. theorem OAI.TwoPointCorrelations.mapped_pieces_flatten line 36
  4. theorem OAI.TwoPointCorrelations.mapped_column_pieces_heads line 49

    Source documentation

    Canonical renaming preserves the exact merge list when it preserves the equality relation on each actual block.

    theorem mapped_column_pieces_heads (f : α → β) (omitted : α → Bool)
    (chunks : List (List α ⊕ α))
    (hinj : ∀ l, Sum.inl l ∈ chunks → ∀ a ∈ l, ∀ b ∈ l, f a = f b ↔ a = b) :
    ((columnChunkPieces omitted chunks).map (Sum.map (List.map f) f)).flatMap
        (Sum.elim id List.singleton) =
      columnRunHeadsWithCuts (columnChunkCuts (chunks.map (Sum.map (List.map f) f))) none := by
…

    Mentions: OAI.TwoPointCorrelations.columnChunkPieces, OAI.TwoPointCorrelations.columnRunHeadsWithCuts, OAI.TwoPointCorrelations.columnChunkCuts

  5. theorem OAI.TwoPointCorrelations.mapped_pieces_regular line 59
  6. theorem OAI.TwoPointCorrelations.mapped_pieces_omitted line 69