OAI/Probability/FKMaps/Inventory.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FKCRT.Inventory.Order line 11

   Source documentation

   none is the flexible order; a typed order is some type.

   abbrev Order := Option Bool

2. inductive OAI.FKCRT.Inventory.Letter line 12
3. def OAI.FKCRT.Inventory.eligible line 19

   Source documentation

   Internal stacks are freshest-first. The source's surviving-burger list is Evaluation.burgers.reverse, so source chronology is unchanged.

   def eligible (a : Order) (b : Bool) : Prop := a=none ∨ a=some b

   Mentions: OAI.FKCRT.Inventory.Order

4. instance OAI.FKCRT.Inventory.(instance at line 21) line 21
5. def OAI.FKCRT.Inventory.pop line 24
6. lemma OAI.FKCRT.Inventory.pop_append line 28
7. lemma OAI.FKCRT.Inventory.pop_eq_none_iff line 41
8. lemma OAI.FKCRT.Inventory.pop_length line 48
9. structure OAI.FKCRT.Inventory.Evaluation line 65
10. def OAI.FKCRT.Inventory.step line 70
11. def OAI.FKCRT.Inventory.run line 76
12. def OAI.FKCRT.Inventory.reduce line 80
13. def OAI.FKCRT.Inventory.evalOrders line 82
14. lemma OAI.FKCRT.Inventory.run_append line 85
15. lemma OAI.FKCRT.Inventory.run_orders_prefix line 91
16. lemma OAI.FKCRT.Inventory.evalOrders_nil line 105
17. lemma OAI.FKCRT.Inventory.evalOrders_append line 107
18. theorem OAI.FKCRT.Inventory.run_older_supply line 119

    Source documentation

    Exact older-supply reduction. Unfilled orders retain chronological order; all surviving new burgers are fresher than all surviving old burgers.

    theorem run_older_supply (w : List Letter) (s : List Bool) :
        run w ⟨[],s⟩ =
          ⟨(evalOrders (reduce w).orders s).orders,
            (reduce w).burgers++(evalOrders (reduce w).orders s).burgers⟩ := by
    …

    Mentions: OAI.FKCRT.Inventory.Letter, OAI.FKCRT.Inventory.run, OAI.FKCRT.Inventory.evalOrders, OAI.FKCRT.Inventory.reduce

19. lemma OAI.FKCRT.Inventory.run_burgers line 144
20. def OAI.FKCRT.Inventory.normalWord line 150
21. theorem OAI.FKCRT.Inventory.run_normalWord line 154

    Source documentation

    A finite word may be replaced by its source reduction in any supply.

    theorem run_normalWord (w : List Letter) (e : Evaluation) :
        run (normalWord (reduce w)) e=run w e := by
    …

    Mentions: OAI.FKCRT.Inventory.Letter, OAI.FKCRT.Inventory.Evaluation, OAI.FKCRT.Inventory.run, OAI.FKCRT.Inventory.normalWord, OAI.FKCRT.Inventory.reduce

22. theorem OAI.FKCRT.Inventory.freshest_survivor_prepend line 167

    Source documentation

    Once a suffix has a surviving burger, its freshest survivor is unchanged by prepending arbitrary further letters.

    theorem freshest_survivor_prepend (w w' : List Letter) {b : Bool} {bs : List Bool}
        (h : (reduce w).burgers=b::bs) : (reduce (w'++w)).burgers.head?=some b := by
    …

    Mentions: OAI.FKCRT.Inventory.Letter, OAI.FKCRT.Inventory.reduce

23. def OAI.FKCRT.Inventory.Letter.increment line 176
24. def OAI.FKCRT.Inventory.imbalance line 180
25. lemma OAI.FKCRT.Inventory.step_imbalance line 182
26. lemma OAI.FKCRT.Inventory.run_imbalance line 195
27. lemma OAI.FKCRT.Inventory.reduce_imbalance line 203
28. lemma OAI.FKCRT.Inventory.survivor_of_sum_pos line 208
29. lemma OAI.FKCRT.Inventory.orders_length_le_step line 215
30. lemma OAI.FKCRT.Inventory.orders_length_le_run line 221
31. def OAI.FKCRT.Inventory.EmptyReducing line 227
32. theorem OAI.FKCRT.Inventory.emptyReducing_dyck line 230

    Source documentation

    Exact necessary Dyck-path event, without invoking a map encoding.

    theorem emptyReducing_dyck (w : List Letter) (h : EmptyReducing w) :
        (w.map Letter.increment).sum=0 ∧
          ∀ j,0≤((w.take j).map Letter.increment).sum := by
    …

    Mentions: OAI.FKCRT.Inventory.Letter, OAI.FKCRT.Inventory.EmptyReducing, OAI.FKCRT.Inventory.Letter.increment

33. lemma OAI.FKCRT.Inventory.evalOrders_cons line 246
34. lemma OAI.FKCRT.Inventory.evalOrders_empty line 258
35. lemma OAI.FKCRT.Inventory.evalOrders_singleton line 263
36. lemma OAI.FKCRT.Inventory.evalOrders_no_match line 273
37. lemma OAI.FKCRT.Inventory.prepend_order_burgers line 280
38. theorem OAI.FKCRT.Inventory.first_survivor_shape line 289

    Source documentation

    The first backwards survivor has exactly one burger and only fixed orders of the opposite type, precisely as in source word:stopped-sum.

    theorem first_survivor_shape (a : Letter) (w : List Letter)
        (h₀ : (reduce w).burgers=[]) (h₁ : (reduce (a::w)).burgers≠[]) :
        ∃ b, a=.burger b ∧ reduce (a::w)=⟨(reduce w).orders,[b]⟩ ∧
          ∀ o∈(reduce w).orders,o=some (!b) := by
    …

    Mentions: OAI.FKCRT.Inventory.Letter, OAI.FKCRT.Inventory.reduce