WordCoefficients.lean`

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FKCRT.Inventory.stoppedWord line 12
def OAI.FKCRT.Inventory.stoppedTail line 14
lemma OAI.FKCRT.Inventory.measurable_revealed line 16
lemma OAI.FKCRT.Inventory.measurable_stoppedWord line 19
lemma OAI.FKCRT.Inventory.measurable_stoppedTail line 24
lemma OAI.FKCRT.Inventory.stoppedWord_of_hit line 29
lemma OAI.FKCRT.Inventory.stoppedTail_of_hit line 31
lemma OAI.FKCRT.Inventory.stoppedWord_rectangle_sum line 34
lemma OAI.FKCRT.Inventory.stoppedWord_rectangle line 70
lemma OAI.FKCRT.Inventory.stoppedTail_preserving line 79
lemma OAI.FKCRT.Inventory.stoppedWord_indep_tail line 87
def OAI.FKCRT.Inventory.wordPieces line 95
lemma OAI.FKCRT.Inventory.stoppedWordPieces_iid line 97
lemma OAI.FKCRT.TreeCoding.firstZero_eq_iff line 113
lemma OAI.FKCRT.Inventory.stopping_measurable line 127
def OAI.FKCRT.Inventory.downPath line 143
def OAI.FKCRT.Inventory.firstDown line 144
lemma OAI.FKCRT.Inventory.downPath_adapted line 145
lemma OAI.FKCRT.Inventory.firstDown_stopping line 150
lemma OAI.FKCRT.Inventory.firstDown_measurable line 152
lemma OAI.FKCRT.Inventory.downPath_step line 153
lemma OAI.FKCRT.Inventory.downPath_initial line 158
lemma OAI.FKCRT.Inventory.downPath_martingale line 162
lemma OAI.FKCRT.Inventory.firstDown_finite line 167
lemma OAI.FKCRT.Inventory.firstDown_of_hit_iff line 181
lemma OAI.FKCRT.Inventory.firstDown_prefix_pos line 190
def OAI.FKCRT.Inventory.reverseRightWord line 203
def OAI.FKCRT.Inventory.reverseRightLaw line 204
lemma OAI.FKCRT.Inventory.reverseRightWord_measurable line 205
instance OAI.FKCRT.Inventory.reverseRightLaw_probability line 206
lemma OAI.FKCRT.Inventory.reverseRightWord_net line 208
def OAI.FKCRT.SimpleWalk.greenMajorant line 227
Source documentation
Bounded discrete Green supersolution for the walk killed at -1.
```
def greenMajorant (a b : ℕ) : ℝ := 2*(min (a+1) (b+1):ℕ)
```
lemma OAI.FKCRT.SimpleWalk.greenMajorant_nonneg line 228
lemma OAI.FKCRT.SimpleWalk.greenMajorant_zero line 229
lemma OAI.FKCRT.SimpleWalk.greenMajorant_succ line 234
lemma OAI.FKCRT.SimpleWalk.killed_green_partial line 257
lemma OAI.FKCRT.SimpleWalk.killed_summable line 273
theorem OAI.FKCRT.SimpleWalk.killed_green_bound line 278
Source documentation
Expected visits below a first down-crossing are at most twice the height above the killing boundary. This includes every initial level.
```
theorem killed_green_bound (a b : ℕ) : (∑' n,killed n a b) ≤ 2*(b+1:ℕ) := by
…
```
Mentions: OAI.FKCRT.SimpleWalk.killed
def OAI.FKCRT.Inventory.burgerSign line 293
lemma OAI.FKCRT.Inventory.burgerSign_increment line 296
lemma OAI.FKCRT.Inventory.burgerSign_preserving line 298
def OAI.FKCRT.Inventory.rawPrefix line 317
lemma OAI.FKCRT.Inventory.rawPrefix_measurable line 318
lemma OAI.FKCRT.Inventory.rawPrefix_preserving line 320
def OAI.FKCRT.Inventory.rawWord line 332
def OAI.FKCRT.Inventory.wordWeight line 333
lemma OAI.FKCRT.Inventory.rawWord_cylinder line 334
def OAI.FKCRT.Inventory.finiteSigns line 351
lemma OAI.FKCRT.Inventory.finiteSigns_preserving line 352
lemma OAI.FKCRT.Inventory.raw_sign_pathSum line 359
def OAI.FKCRT.Inventory.rawKilled line 370
lemma OAI.FKCRT.Inventory.rawKilled_measure line 372
lemma OAI.FKCRT.Inventory.typed_fixed_balance line 402
def OAI.FKCRT.Inventory.burgerCount line 406
def OAI.FKCRT.Inventory.orderCount line 409
lemma OAI.FKCRT.Inventory.typed_counts line 412
lemma OAI.FKCRT.Inventory.fixed_wordMass line 420
lemma OAI.FKCRT.Inventory.fixed_wordMass_empty line 427
lemma OAI.FKCRT.Inventory.markings_mass_empty line 438
def OAI.FKCRT.Inventory.wordsOfLength line 444
lemma OAI.FKCRT.Inventory.mem_wordsOfLength line 447
def OAI.FKCRT.Inventory.emptyWords line 458
def OAI.FKCRT.Inventory.typedEmptyWords line 460
lemma OAI.FKCRT.Inventory.emptyWords_markings line 463
lemma OAI.FKCRT.Inventory.markings_disjoint line 479
theorem OAI.FKCRT.Inventory.empty_wordMass_sum line 490
Source documentation
Exact total genuine iid weight, before identifying it with its cylinder probability. All flexible markings are summed, not picked deterministically.
```
theorem empty_wordMass_sum (P : Parameters) (m : ℕ) :
    (∑ w∈emptyWords (2*m),wordMass P w)=
      ((1-P.p)/16)^m * ∑ v∈typedEmptyWords (2*m),
        (1+2*P.p/(1-P.p))^flexibleCount v [] := by
…
```
Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.emptyWords, OAI.FKCRT.Inventory.wordMass, OAI.FKCRT.Inventory.typedEmptyWords, OAI.FKCRT.Inventory.flexibleCount
lemma OAI.FKCRT.Inventory.wordMass_nonneg line 500
lemma OAI.FKCRT.Inventory.wordWeight_eq line 503
lemma OAI.FKCRT.Inventory.rawEmpty_measure line 511
lemma OAI.FKCRT.Inventory.rawEmpty_real line 538
lemma OAI.FKCRT.Inventory.cornerInsert_length line 552
lemma OAI.FKCRT.Inventory.cornerList_length line 561
lemma OAI.FKCRT.Inventory.cornerList_flexible line 566
lemma OAI.FKCRT.Inventory.empty_length_even line 574
def OAI.FKCRT.Inventory.CoreTree.vertexCount line 582
lemma OAI.FKCRT.Inventory.CoreTree.word_length line 586
def OAI.FKCRT.Inventory.wordMonomial line 600
Source documentation
Literal weight in the letter-size variable. Specializing r²=u gives exactly the source weight t^flex u^edges.
```
def wordMonomial {R : Type*} [CommMonoid R] (t r : R) (w : List TypedLetter) : R :=
…
```
Mentions: OAI.FKCRT.Inventory.TypedLetter
lemma OAI.FKCRT.Inventory.wordMonomial_nil line 603
lemma OAI.FKCRT.Inventory.wordMonomial_corners line 606
def OAI.FKCRT.Inventory.wordSeries line 615
Source documentation
The full genuine word generating series, with no convergence premise.
```
def wordSeries (t r : ℝ≥0∞) : ℝ≥0∞ := ∑' w : EmptyTypedWord,wordMonomial t r w.val
```
Mentions: OAI.FKCRT.Inventory.EmptyTypedWord, OAI.FKCRT.Inventory.wordMonomial
lemma OAI.FKCRT.Inventory.tsum_fin_product line 617
lemma OAI.FKCRT.Inventory.coreChildrenEquiv_weight line 628
theorem OAI.FKCRT.Inventory.nonempty_word_series line 635
Source documentation
The nonempty part of T is exactly the nonnegative connected-core substitution series. No independence or coefficient identity is assumed.
```
theorem nonempty_word_series (t r : ℝ≥0∞) :
    (∑' w : NonemptyTypedWord,wordMonomial t r w.val.val)=
      ∑' c : Core,t^flexibleCount c.val []*(r*wordSeries t r)^c.val.length := by
…
```
Mentions: OAI.FKCRT.Inventory.NonemptyTypedWord, OAI.FKCRT.Inventory.wordMonomial, OAI.FKCRT.Inventory.Core, OAI.FKCRT.Inventory.flexibleCount, OAI.FKCRT.Inventory.wordSeries