OAI/Probability/FKMaps/SimpleWalk.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FKCRT.SimpleWalk.kernel line 11

   Source documentation

   Exact probabilities for the symmetric nearest-neighbour walk on the integers.

   def kernel : ℕ → ℤ → ℝ
     | 0,z => if z=0 then 1 else 0
     | n+1,z => (kernel n (z-1)+kernel n (z+1))/2

2. lemma OAI.FKCRT.SimpleWalk.kernel_zero line 15
3. lemma OAI.FKCRT.SimpleWalk.kernel_succ line 16
4. lemma OAI.FKCRT.SimpleWalk.kernel_symm line 17
5. lemma OAI.FKCRT.SimpleWalk.kernel_nonneg line 23
6. lemma OAI.FKCRT.SimpleWalk.kernel_support line 27
7. def OAI.FKCRT.SimpleWalk.killed line 42

   Source documentation

   The walk killed on first visiting -1, with both endpoints nonnegative.

   def killed : ℕ → ℕ → ℕ → ℝ
     | 0,a,b => if a=b then 1 else 0
     | n+1,0,b => killed n 1 b/2
     | n+1,a+1,b => (killed n a b+killed n (a+2) b)/2

8. lemma OAI.FKCRT.SimpleWalk.killed_nonneg line 47
9. theorem OAI.FKCRT.SimpleWalk.killed_reflection line 56

   Source documentation

   Discrete reflection principle; this is an identity of the actual killed transition recursion, not an assumed excursion law.

   theorem killed_reflection (n a b : ℕ) :
       killed n a b = kernel n ((b:ℤ)-a)-kernel n ((b:ℤ)+a+2) := by
   …

   Mentions: OAI.FKCRT.SimpleWalk.killed, OAI.FKCRT.SimpleWalk.kernel

10. lemma OAI.FKCRT.SimpleWalk.killed_symm line 81
11. def OAI.FKCRT.SimpleWalk.chooseInt line 86

    Source documentation

    Binomial coefficients extended by zero to negative lower arguments.

    def chooseInt (n : ℕ) (k : ℤ) : ℝ := if 0≤k then (n.choose k.toNat:ℝ) else 0

12. lemma OAI.FKCRT.SimpleWalk.chooseInt_zero line 88
13. lemma OAI.FKCRT.SimpleWalk.chooseInt_pascal line 98
14. lemma OAI.FKCRT.SimpleWalk.kernel_binomial line 112
15. lemma OAI.FKCRT.SimpleWalk.chooseInt_adjacent line 138
16. lemma OAI.FKCRT.SimpleWalk.kernel_adjacent line 152
17. theorem OAI.FKCRT.SimpleWalk.killed_entrance line 173

    Source documentation

    Exact entrance density, including the zero-time and unreachable cases.

    theorem killed_entrance (n b : ℕ) :
        killed n 0 b = (2*((b:ℝ)+1)/((n:ℝ)+b+2))*kernel n b := by
    …

    Mentions: OAI.FKCRT.SimpleWalk.killed, OAI.FKCRT.SimpleWalk.kernel

18. def OAI.FKCRT.SimpleWalk.sign line 192
19. abbrev OAI.FKCRT.SimpleWalk.Path line 194
20. def OAI.FKCRT.SimpleWalk.pathSum line 196
21. lemma OAI.FKCRT.SimpleWalk.pathSum_zero line 199
22. lemma OAI.FKCRT.SimpleWalk.pathSum_cons line 201
23. def OAI.FKCRT.SimpleWalk.splitPath line 205
24. lemma OAI.FKCRT.SimpleWalk.sum_path_succ line 211
25. def OAI.FKCRT.SimpleWalk.pathMass line 217

    Source documentation

    Uniform nearest-neighbour path counting probability.

    def pathMass (n : ℕ) (P : Path n → Prop) : ℝ :=
    …

    Mentions: OAI.FKCRT.SimpleWalk.Path

26. lemma OAI.FKCRT.SimpleWalk.pathMass_congr line 220
27. lemma OAI.FKCRT.SimpleWalk.pathMass_succ line 223
28. lemma OAI.FKCRT.SimpleWalk.pathMass_endpoint line 230
29. def OAI.FKCRT.SimpleWalk.nonnegativePath line 244
30. lemma OAI.FKCRT.SimpleWalk.nonnegativePath_cons line 247
31. lemma OAI.FKCRT.SimpleWalk.pathMass_killed line 262
32. theorem OAI.FKCRT.SimpleWalk.pathMass_reflection line 304

    Source documentation

    Reflection counts actual nonnegative paths, including all parity cases.

    theorem pathMass_reflection (n a b : ℕ) :
        pathMass n (fun d => nonnegativePath a d ∧ (a:ℤ)+pathSum d n=b)=
          kernel n ((b:ℤ)-a)-kernel n ((b:ℤ)+a+2) := by
    …

    Mentions: OAI.FKCRT.SimpleWalk.pathMass, OAI.FKCRT.SimpleWalk.nonnegativePath, OAI.FKCRT.SimpleWalk.pathSum, OAI.FKCRT.SimpleWalk.kernel

33. def OAI.FKCRT.TreeCoding.binaryMass line 318
34. lemma OAI.FKCRT.TreeCoding.binaryMass_nonneg line 320
35. lemma OAI.FKCRT.TreeCoding.binaryMass_total line 322
36. lemma OAI.FKCRT.TreeCoding.binaryMass_moment line 326
37. def OAI.FKCRT.TreeCoding.binaryOffspring line 339
38. lemma OAI.FKCRT.TreeCoding.binaryOffspring_variance line 352
39. lemma OAI.FKCRT.TreeCoding.binaryOffspring_sigma line 363
40. def OAI.FKCRT.TreeCoding.binaryDegree line 367

    Source documentation

    Binary paths really sample critical, variance-one even offspring.

    def binaryDegree (s : Bool) : ℕ := if s then 2 else 0

41. instance OAI.FKCRT.TreeCoding.(instance at line 369) line 369
42. instance OAI.FKCRT.TreeCoding.(instance at line 370) line 370
43. def OAI.FKCRT.TreeCoding.coinLaw line 372
44. lemma OAI.FKCRT.TreeCoding.coinLaw_singleton line 374
45. instance OAI.FKCRT.TreeCoding.(instance at line 377) line 377
46. lemma OAI.FKCRT.TreeCoding.binaryDegree_preserving line 382
47. lemma OAI.FKCRT.TreeCoding.binaryStep line 402
48. def OAI.FKCRT.TreeCoding.binaryArray line 405
49. lemma OAI.FKCRT.TreeCoding.binaryArray_preserving line 407
50. lemma OAI.FKCRT.TreeCoding.binaryArray_totalStep line 415
51. lemma OAI.FKCRT.TreeCoding.coinPath_singleton line 419
52. lemma OAI.FKCRT.TreeCoding.coinPath_event line 426
53. lemma OAI.FKCRT.TreeCoding.binary_kernel line 439

    Source documentation

    The recursive symmetric kernel is the exact endpoint law used by the already-proved finite-variance conditioned bridge invariance principle.

    lemma binary_kernel (N : ℕ) (z : ℤ) :
        (binaryOffspring.iidLaw N).real {d | totalStep d=z}=SimpleWalk.kernel N z := by
    …

    Mentions: OAI.FKCRT.TreeCoding.totalStep, OAI.FKCRT.SimpleWalk.kernel

54. def OAI.FKCRT.TreeCoding.arrayWalk line 457
55. def OAI.FKCRT.TreeCoding.ArrayGood line 460
56. lemma OAI.FKCRT.TreeCoding.arrayWalk_codeEmbedding line 463
57. lemma OAI.FKCRT.TreeCoding.arrayGood_range line 466
58. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_good_integral line 482

    Source documentation

    The actual good-array restriction is the weighted finite code sum.

    lemma CriticalEvenOffspring.iid_good_integral (p : CriticalEvenOffspring) (N : ℕ)
        (F : (Fin N → ℕ) → ℝ) :
        (∫ d,if ArrayGood d then F d else 0 ∂p.iidLaw N)=
          ∑ d : Code N,codeWeight p d*F (codeEmbedding N d) := by
    …

    Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.ArrayGood, OAI.FKCRT.TreeCoding.Code, OAI.FKCRT.TreeCoding.codeWeight, OAI.FKCRT.TreeCoding.codeEmbedding

59. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.code_iid_integral line 521

    Source documentation

    No informal conditioning is used: finite code expectations are exactly normalized restriction of the iid offspring law to the good event.

    theorem CriticalEvenOffspring.code_iid_integral (p : CriticalEvenOffspring) (n : ℕ)
        (F : (Fin (2*n+1) → ℕ) → ℝ) :
        (∫ c,F (codeEmbedding (2*n+1) c) ∂p.codeLaw n)=
          (∫ d,if ArrayGood d then F d else 0 ∂p.iidLaw (2*n+1))/codePartition p (2*n+1) := by
    …

    Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.codeEmbedding, OAI.FKCRT.TreeCoding.ArrayGood, OAI.FKCRT.TreeCoding.codePartition

60. lemma OAI.FKCRT.TreeCoding.arrayWalk_binaryArray line 530
61. def OAI.FKCRT.TreeCoding.SimpleExcursion line 534
62. lemma OAI.FKCRT.TreeCoding.binaryArray_good line 537
63. lemma OAI.FKCRT.TreeCoding.binary_partition line 540
64. theorem OAI.FKCRT.TreeCoding.binary_code_integral line 548

    Source documentation

    Exact simple-excursion representation of the binary conditioned tree law.

    theorem binary_code_integral (n : ℕ) (F : (Fin (2*n+1) → ℕ) → ℝ) :
        (∫ c,F (codeEmbedding (2*n+1) c) ∂binaryOffspring.codeLaw n)=
          ((2*n+1:ℕ):ℝ)/SimpleWalk.kernel (2*n+1) (-1) *
            ∫ d,if SimpleExcursion d then F (binaryArray d) else 0
              ∂Measure.pi (fun _ : Fin (2*n+1) => coinLaw) := by
    …

    Mentions: OAI.FKCRT.TreeCoding.codeEmbedding, OAI.FKCRT.SimpleWalk.kernel, OAI.FKCRT.TreeCoding.SimpleExcursion, OAI.FKCRT.TreeCoding.binaryArray, OAI.FKCRT.TreeCoding.coinLaw

65. def OAI.FKCRT.SimpleWalk.splitPathAt line 570
66. lemma OAI.FKCRT.SimpleWalk.pathSum_append_left line 576
67. lemma OAI.FKCRT.SimpleWalk.pathSum_append_right line 587
68. lemma OAI.FKCRT.SimpleWalk.nonnegativePath_append line 597
69. lemma OAI.FKCRT.SimpleWalk.pathMass_append line 617
70. theorem OAI.FKCRT.SimpleWalk.pathMass_killed_middle line 632

    Source documentation

    Exact fixed-middle-point Markov factorization of killed path counts.

    theorem pathMass_killed_middle (n m a b c : ℕ) :
        pathMass (n+m) (fun d => nonnegativePath a d ∧
          (a:ℤ)+pathSum d n=b ∧ (a:ℤ)+pathSum d (n+m)=c)=
            killed n a b*killed m b c := by
    …

    Mentions: OAI.FKCRT.SimpleWalk.pathMass, OAI.FKCRT.SimpleWalk.nonnegativePath, OAI.FKCRT.SimpleWalk.pathSum, OAI.FKCRT.SimpleWalk.killed

71. def OAI.FKCRT.SimpleWalk.firstHit line 660

    Source documentation

    Probability of a first visit to -1, starting at a nonnegative integer.

    def firstHit {n : ℕ} (a : ℕ) (d : Path n) : Prop :=
    …

    Mentions: OAI.FKCRT.SimpleWalk.Path

72. lemma OAI.FKCRT.SimpleWalk.firstHit_last line 663
73. lemma OAI.FKCRT.SimpleWalk.pathMass_firstHit line 689
74. theorem OAI.FKCRT.SimpleWalk.firstHit_formula line 711

    Source documentation

    Ballot/first-hitting formula, without parity or reachability restrictions.

    theorem firstHit_formula (n a : ℕ) :
        pathMass (n+1) (firstHit a)=((a:ℝ)+1)/((n:ℝ)+1)*kernel (n+1) ((a:ℤ)+1) := by
    …

    Mentions: OAI.FKCRT.SimpleWalk.pathMass, OAI.FKCRT.SimpleWalk.firstHit, OAI.FKCRT.SimpleWalk.kernel

75. lemma OAI.FKCRT.SimpleWalk.pathMass_true line 731
76. lemma OAI.FKCRT.SimpleWalk.pathMass_endpoint_from line 734
77. lemma OAI.FKCRT.SimpleWalk.firstHit_append_middle line 741

    Source documentation

    Cutting a first-hitting path at a specified nonnegative intermediate level.

    lemma firstHit_append_middle {n m : ℕ} (a b : ℕ) (d : Path n) (e : Path m) :
        (firstHit a (Fin.append d e) ∧ (a:ℤ)+pathSum d n=b)↔
          (nonnegativePath a d ∧ (a:ℤ)+pathSum d n=b) ∧ firstHit b e := by
    …

    Mentions: OAI.FKCRT.SimpleWalk.Path, OAI.FKCRT.SimpleWalk.firstHit, OAI.FKCRT.SimpleWalk.pathSum, OAI.FKCRT.SimpleWalk.nonnegativePath

78. def OAI.FKCRT.SimpleWalk.traceSize line 770
79. def OAI.FKCRT.SimpleWalk.tracePoints line 775

    Source documentation

    Successive specified heights, with free terminal suffix.

    def tracePoints (a R : ℕ) : (xs : List (ℕ×ℕ)) → Path (traceSize R xs) → Prop
      | [],_ => True
      | x::xs,d => (a:ℤ)+pathSum (splitPathAt x.1 (traceSize R xs) d).1 x.1=x.2 ∧
        tracePoints x.2 R xs (splitPathAt x.1 (traceSize R xs) d).2
    
    /-- The same specified heights, together with nonnegative segments and final first hit. -/

    Mentions: OAI.FKCRT.SimpleWalk.Path, OAI.FKCRT.SimpleWalk.traceSize, OAI.FKCRT.SimpleWalk.pathSum, OAI.FKCRT.SimpleWalk.splitPathAt, OAI.FKCRT.SimpleWalk.segments

80. def OAI.FKCRT.SimpleWalk.traceExcursion line 781

    Source documentation

    The same specified heights, together with nonnegative segments and final first hit.

    def traceExcursion (a R : ℕ) : (xs : List (ℕ×ℕ)) → Path (traceSize R xs) → Prop
      | [],d => firstHit a d
      | x::xs,d =>
        (nonnegativePath a (splitPathAt x.1 (traceSize R xs) d).1 ∧
          (a:ℤ)+pathSum (splitPathAt x.1 (traceSize R xs) d).1 x.1=x.2) ∧
        traceExcursion x.2 R xs (splitPathAt x.1 (traceSize R xs) d).2

    Mentions: OAI.FKCRT.SimpleWalk.Path, OAI.FKCRT.SimpleWalk.traceSize, OAI.FKCRT.SimpleWalk.firstHit, OAI.FKCRT.SimpleWalk.nonnegativePath, OAI.FKCRT.SimpleWalk.splitPathAt, OAI.FKCRT.SimpleWalk.pathSum

81. def OAI.FKCRT.SimpleWalk.traceFreeWeight line 788
82. def OAI.FKCRT.SimpleWalk.traceKilledWeight line 792
83. lemma OAI.FKCRT.SimpleWalk.traceExcursion_iff line 796
84. theorem OAI.FKCRT.SimpleWalk.pathMass_tracePoints line 810

    Source documentation

    Actual unrestricted finite-dimensional probabilities factor into free kernels.

    theorem pathMass_tracePoints (a R : ℕ) (xs : List (ℕ×ℕ)) :
        pathMass (traceSize R xs) (tracePoints a R xs)=traceFreeWeight a xs := by
    …

    Mentions: OAI.FKCRT.SimpleWalk.pathMass, OAI.FKCRT.SimpleWalk.traceSize, OAI.FKCRT.SimpleWalk.tracePoints, OAI.FKCRT.SimpleWalk.traceFreeWeight

85. theorem OAI.FKCRT.SimpleWalk.pathMass_traceExcursion line 824

    Source documentation

    Actual nonnegative first-hitting finite-dimensional probabilities have the reflected-kernel product, with the exact terminal first-hitting factor.

    theorem pathMass_traceExcursion (a R : ℕ) (xs : List (ℕ×ℕ)) :
        pathMass (traceSize R xs) (traceExcursion a R xs)=traceKilledWeight a R xs := by
    …

    Mentions: OAI.FKCRT.SimpleWalk.pathMass, OAI.FKCRT.SimpleWalk.traceSize, OAI.FKCRT.SimpleWalk.traceExcursion, OAI.FKCRT.SimpleWalk.traceKilledWeight

86. lemma OAI.FKCRT.SimpleWalk.killed_le_kernel line 838
87. lemma OAI.FKCRT.SimpleWalk.traceKilledWeight_nonneg line 842
88. lemma OAI.FKCRT.SimpleWalk.traceFreeWeight_nonneg line 848
89. lemma OAI.FKCRT.SimpleWalk.traceKilledWeight_eq_zero line 853
90. def OAI.FKCRT.SimpleWalk.uniformLaw line 877

    Source comment

    The inherited product-law realization, not a fresh informal conditioning.

    def uniformLaw (N : ℕ) : Measure (Path N) := Measure.pi (fun _ => coinLaw)

    Mentions: OAI.FKCRT.SimpleWalk.Path

91. instance OAI.FKCRT.SimpleWalk.uniformLaw_probability line 879
92. lemma OAI.FKCRT.SimpleWalk.uniformLaw_singleton line 882
93. lemma OAI.FKCRT.SimpleWalk.uniformLaw_real line 887
94. lemma OAI.FKCRT.SimpleWalk.firstHit_zero_iff line 899
95. lemma OAI.FKCRT.SimpleWalk.firstHit_mass_pos line 902
96. def OAI.FKCRT.SimpleWalk.excursionLaw line 913

    Source documentation

    Uniform binary walks conditioned on their first hit of -1 at the odd endpoint.

    def excursionLaw (n : ℕ) : Measure (Path (2*n+1)) :=
    …

    Mentions: OAI.FKCRT.SimpleWalk.Path

97. instance OAI.FKCRT.SimpleWalk.excursionLaw_probability line 916
98. lemma OAI.FKCRT.SimpleWalk.excursionLaw_real line 924
99. lemma OAI.FKCRT.SimpleWalk.excursionLaw_ae line 934
100. lemma OAI.FKCRT.SimpleWalk.excursionLaw_integral line 937
101. lemma OAI.FKCRT.SimpleWalk.binary_code_integral line 944
102. lemma OAI.FKCRT.SimpleWalk.pathSum_parity line 962