IndexedBlockFamily.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The actual indexed regular segments of a finite family of perfect blocks.

theorem OAI.TwoPointCorrelations.decoded_forest_transport line 12
def OAI.TwoPointCorrelations.indexedRegularSegments line 21
theorem OAI.TwoPointCorrelations.mem_indexedRegularSegments line 27
theorem OAI.TwoPointCorrelations.indexedRegularSegments_nonempty line 41
theorem OAI.TwoPointCorrelations.indexedBlockRuns_length_le line 47
theorem OAI.TwoPointCorrelations.indexedRegularSegments_total_length line 55
Source documentation
The total number of retained regular run starts is bounded by the number of original positions, with no factor for the number of labels.
```
theorem indexedRegularSegments_total_length (label : ℕ → α) (omitted : α → Bool)
    (blocks : List (ℕ × ℕ)) :
    ((indexedRegularSegments label omitted blocks).map List.length).sum ≤
      (blocks.map Prod.snd).sum := by
…
```
Mentions: OAI.TwoPointCorrelations.indexedRegularSegments

theorem OAI.TwoPointCorrelations.indexedRegularSegments_cover line 71

Source documentation

Every regular label seen in a block survives both compression and the omitted-label cut, so its forest line is included in the shared numbering.

theorem indexedRegularSegments_cover (label : ℕ → α) (omitted : α → Bool)
    (blocks : List (ℕ × ℕ)) (b : ℕ × ℕ) (hb : b ∈ blocks) (z : α)
    (hz : z ∈ blockLabelList label b.1 b.2) (hregular : omitted z = false) :
    ∃ segment ∈ indexedRegularSegments label omitted blocks, ∃ p ∈ segment, p.2 = z := by
…

Mentions: OAI.TwoPointCorrelations.blockLabelList, OAI.TwoPointCorrelations.indexedRegularSegments

theorem OAI.TwoPointCorrelations.indexed_block_family_numbering line 88

Source documentation

Number the regular paths actually produced by the given blocks. The hypotheses are line incidence and nonvanishing physical intervals; all path, compression, coverage and size data are constructed here.

theorem indexed_block_family_numbering {N : ℕ}
    (D : Submodule K (α → K)) (anchor : ι → (α → K) ⧸ D)
    (regularLabel : ι → α) (rename : α → ι)
    (label : ℕ → α) (coefficient : ℕ → K) (omitted : α → Bool)
    (blocks : List (ℕ × ℕ))
    (hind : LinearIndependent K (fun j => D.mkQ (Pi.basisFun K α (regularLabel j))))
    (hname : ∀ z, omitted z = false → regularLabel (rename z) = z)
    (hline : ∀ b ∈ blocks, ∀ t ∈ Ico b.1 (b.1 + b.2), omitted (label t) = false →
      ∃ c : K, D.mkQ (formalDeparture label coefficient t) = anchor (rename (label t)) +
        c • D.mkQ (Pi.basisFun K α (regularLabel (rename (label t)))))
    (hnonzero : ∀ b ∈ blocks, ∀ a e z, b.1 ≤ a → a < e → e ≤ b.1 + b.2 →
      (∀ t ∈ Ico a e, label t = z) → (∑ t ∈ Ico a e, coefficient t) ≠ 0)
…

Mentions: OAI.TwoPointCorrelations.formalDeparture