OAI/NumberTheory/Ostmann/Construction/WordRangeReplay.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.WordRange line 11
2. structure OAI.Ostmann.HistoryRange line 16
3. def OAI.Ostmann.WordRange.Holds line 21
4. def OAI.Ostmann.HistoryRange.Holds line 24
5. def OAI.Ostmann.WordRange.toHistory line 27
6. theorem OAI.Ostmann.WordRange.toHistory_holds line 31
7. inductive OAI.Ostmann.WordRangeDecoration line 46
8. def OAI.Ostmann.WordRangeDecoration.ValidAt line 51
9. def OAI.Ostmann.WordRangeDecoration.formulas line 62
10. theorem OAI.Ostmann.WordRangeDecoration.formulas_iff line 75

    Source documentation

    Every intermediate bin, including its endpoints, is precisely a range of the formula obtained by the original integer reconstruction.

    theorem WordRangeDecoration.formulas_iff {σ : Type*} {n : ℕ}
        (D : WordRangeDecoration σ n) (template : WordTransferTemplate σ n)
        (t : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t)
        (env : σ → HistoryFormula σ) (a : σ → ℤ) (x : σ → ℕ)
        (henv : ∀ i, (env i).value (fun j => (a j : ℚ)) = (x i : ℚ))
        (hv : ValidTransferHistory (wordTransferSystem σ) n (template.state x) t) :
        (∀ r ∈ D.formulas template t ht env, r.Holds a) ↔ D.ValidAt template x t := by
    …

    Mentions: OAI.Ostmann.WordRangeDecoration, OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.HistoryFormula, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.wordTransferSystem

11. def OAI.Ostmann.WordRangeDecoration.count line 99
12. theorem OAI.Ostmann.WordRangeDecoration.formulas_length line 103