OAI/Probability/FKMaps/WordLaw.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.FKCRT.Inventory.(instance at line 11) line 11
  2. instance OAI.FKCRT.Inventory.(instance at line 12) line 12
  3. instance OAI.FKCRT.Inventory.(instance at line 13) line 13
  4. instance OAI.FKCRT.Inventory.(instance at line 14) line 14
  5. structure OAI.FKCRT.Inventory.Parameters line 16
  6. lemma OAI.FKCRT.Inventory.Parameters.pos line 21
  7. def OAI.FKCRT.Inventory.Parameters.ofQ line 23
  8. def OAI.FKCRT.Inventory.mass line 32
  9. lemma OAI.FKCRT.Inventory.mass_pos line 37
  10. lemma OAI.FKCRT.Inventory.sum_letters line 42
  11. lemma OAI.FKCRT.Inventory.mass_sum line 55
  12. def OAI.FKCRT.Inventory.law line 60
  13. lemma OAI.FKCRT.Inventory.law_singleton line 64
  14. lemma OAI.FKCRT.Inventory.law_real_singleton line 68
  15. lemma OAI.FKCRT.Inventory.integral_law line 72
  16. lemma OAI.FKCRT.Inventory.integral_increment line 78
  17. def OAI.FKCRT.Inventory.streamLaw line 84
  18. instance OAI.FKCRT.Inventory.(instance at line 86) line 86
  19. def OAI.FKCRT.Inventory.signSum line 89
  20. lemma OAI.FKCRT.Inventory.signSum_succ line 92
  21. lemma OAI.FKCRT.Inventory.increment_bounds line 95
  22. theorem OAI.FKCRT.Inventory.signs_hit_one line 100

    Source documentation

    Recurrence of the actual raw-word signs. This uses the proved integer martingale recurrence theorem, not a recurrence hypothesis.

    theorem signs_hit_one (P : Parameters) :
    ∀ᵐ x ∂streamLaw P ℕ,∃ n,signSum x n=1 := by
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.streamLaw, OAI.FKCRT.Inventory.signSum

  23. lemma OAI.FKCRT.Inventory.pop_fixed line 156
  24. lemma OAI.FKCRT.Inventory.pop_flexible line 166
  25. inductive OAI.FKCRT.Inventory.TypedLetter line 169
  26. def OAI.FKCRT.Inventory.TypedLetter.fixed line 174
  27. def OAI.FKCRT.Inventory.stackTypedStep line 178
  28. def OAI.FKCRT.Inventory.identifyOne line 182
  29. def OAI.FKCRT.Inventory.identify line 189
  30. def OAI.FKCRT.Inventory.stackTypedRun line 196
  31. lemma OAI.FKCRT.Inventory.identifyOne_step line 200
  32. lemma OAI.FKCRT.Inventory.identifyOne_none line 219
  33. lemma OAI.FKCRT.Inventory.identify_sound line 229
  34. lemma OAI.FKCRT.Inventory.identify_complete line 249
  35. lemma OAI.FKCRT.Inventory.emptyReducing_iff_identify line 266
  36. lemma OAI.FKCRT.Inventory.identify_fixed line 272
  37. def OAI.FKCRT.Inventory.flexibleClosing line 295

    Source documentation

    A fixed typed closing is flexible exactly when its type is the freshest burger still present. This is a property of the identified word, not of marks.

    def flexibleClosing (s : List Bool) : TypedLetter → Prop
  | .burger _ => False
  | .order b => s.head?=some b

    Mentions: OAI.FKCRT.Inventory.TypedLetter

  38. instance OAI.FKCRT.Inventory.(instance at line 298) line 298
  39. def OAI.FKCRT.Inventory.origins line 301
  40. lemma OAI.FKCRT.Inventory.identifyOne_typedStep line 304
  41. lemma OAI.FKCRT.Inventory.identifyOne_unique line 339
  42. def OAI.FKCRT.Inventory.markings line 343
  43. lemma OAI.FKCRT.Inventory.mem_markings line 349
  44. def OAI.FKCRT.Inventory.wordMass line 397
  45. def OAI.FKCRT.Inventory.flexibleCount line 399
  46. lemma OAI.FKCRT.Inventory.origins_mass line 405
  47. lemma OAI.FKCRT.Inventory.markings_mass line 418
  48. lemma OAI.FKCRT.Inventory.stack_pop_fixed_count line 455
  49. lemma OAI.FKCRT.Inventory.typedRun_append line 467
  50. lemma OAI.FKCRT.Inventory.typedRun_balance line 475
  51. lemma OAI.FKCRT.Inventory.typedRun_prefix line 494
  52. lemma OAI.FKCRT.Inventory.typedRun_prefix_count line 502
  53. lemma OAI.FKCRT.Inventory.typedRun_exists_iff line 511

    Source documentation

    Successful typed words are exactly the shuffles of two nonnegative paths; final emptiness will make both paths Dyck words.

    lemma typedRun_exists_iff (w : List TypedLetter) (s : List Bool) :
    (∃ t,stackTypedRun w s=some t) ↔
      ∀ v,v<+:w → ∀ c : Bool,v.count (.order c)≤ s.count c+v.count (.burger c) := by
…

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.stackTypedRun

  54. def OAI.FKCRT.Inventory.colorStep line 542
  55. def OAI.FKCRT.Inventory.colorWord line 546
  56. lemma OAI.FKCRT.Inventory.colorWord_counts line 548
  57. def OAI.FKCRT.Inventory.identifiedDyck line 560

    Source documentation

    The precise source identification: each type separately is a genuine Mathlib Dyck word, with no assumption about flexible marks.

    def identifiedDyck {w : List TypedLetter} (h : stackTypedRun w []=some []) (c : Bool) : DyckWord where
…

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.stackTypedRun

  58. lemma OAI.FKCRT.Inventory.typedRun_empty_iff line 572
  59. lemma OAI.FKCRT.Inventory.fixed_word_mass line 593
  60. lemma OAI.FKCRT.Inventory.typedLetter_length line 604
  61. theorem OAI.FKCRT.Inventory.empty_markings_mass line 614

    Source documentation

    Exact finite flexible-marking weight from words.tex (markedweight). The remaining map activity correspondence must identify flexibleCount.

    theorem empty_markings_mass (P : Parameters) {w : List TypedLetter}
    (h : stackTypedRun w []=some []) :
    (∑ v∈markings w [],wordMass P v) =
      ((1-P.p)/16)^(w.length/2)*(1+2*P.p/(1-P.p))^(flexibleCount w []) := by
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.stackTypedRun, OAI.FKCRT.Inventory.markings, OAI.FKCRT.Inventory.wordMass, OAI.FKCRT.Inventory.flexibleCount