RegularSegmentCoding.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Assemble all actual regular segments into one shared forest code.

theorem OAI.TwoPointCorrelations.regular_segment_list_numbering line 16

Source documentation

Enumerating nonempty segments does not require separate choices of line names for each block. Their common quotient forest supplies one numbering.

theorem regular_segment_list_numbering {N : ℕ}
    (D : Submodule K (α → K)) (anchor : ι → (α → K) ⧸ D)
    (regularLabel : ι → α) (label : ℕ → α) (coefficient : ℕ → K)
    (hind : LinearIndependent K (fun j => D.mkQ (Pi.basisFun K α (regularLabel j))))
    (segments : List (List (ℕ × ι)))
    (hne : ∀ segment ∈ segments, segment ≠ [])
    (hstart : ∀ first rest, first :: rest ∈ segments → ∃ c : K,
      D.mkQ (formalDeparture label coefficient first.1) =
        anchor first.2 + c • D.mkQ (Pi.basisFun K α (regularLabel first.2)))
    (hdata : ∀ first rest, first :: rest ∈ segments →
      QuotientRunData D anchor regularLabel label coefficient first.1 first.2 rest)
    (hsize : 2 * (segments.map List.length).sum ≤ N) :
…

Mentions: OAI.TwoPointCorrelations.formalDeparture, OAI.TwoPointCorrelations.QuotientRunData

theorem OAI.TwoPointCorrelations.regular_pieces_total_length_le line 85

Source documentation

Removing omitted runs cannot increase the total number of regular vertices, even when a label is repeated in separate blocks.

theorem regular_pieces_total_length_le (pieces : List (List α ⊕ α)) :
    ((pieces.filterMap (Sum.elim some (fun _ => none))).map List.length).sum ≤
      (pieces.flatMap (Sum.elim id List.singleton)).length := by
…