OAI/Probability/FKMaps/PieceWalks.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FKCRT.Inventory.wordSeries_substitution line 13
  2. def OAI.FKCRT.Inventory.emptyAtSizeEquiv line 39
  3. lemma OAI.FKCRT.Inventory.empty_tsum_by_size line 53

    Source documentation

    Arbitrary nonnegative observables partition by the actual even length.

    lemma empty_tsum_by_size (f : List TypedLetter→ℝ≥0∞) :
    (∑' w : EmptyTypedWord,f w.val)=∑' m : ℕ,∑ w∈typedEmptyWords (2*m),f w := by
…

    Mentions: OAI.FKCRT.Inventory.TypedLetter, OAI.FKCRT.Inventory.EmptyTypedWord, OAI.FKCRT.Inventory.typedEmptyWords

  4. def OAI.FKCRT.Inventory.typedCoefficient line 65
  5. lemma OAI.FKCRT.Inventory.wordSeries_coefficients line 68
  6. def OAI.FKCRT.Inventory.coreSubtypeEquiv line 79
  7. lemma OAI.FKCRT.Inventory.core_tsum_by_size line 85
  8. def OAI.FKCRT.Inventory.coreCoefficient line 101
  9. lemma OAI.FKCRT.Inventory.core_series_coefficients line 104
  10. theorem OAI.FKCRT.Inventory.wordSeries_core_coefficients line 118

    Source documentation

    Exact source T=1+Phi_+(u*T²), now for the actual connected-core coefficients extracted from the original inventory words.

    theorem wordSeries_core_coefficients (t r : ℝ≥0∞) :
    wordSeries t r=1+∑' m : ℕ,coreCoefficient t m*(r^2*wordSeries t r^2)^m := by
…

    Mentions: OAI.FKCRT.Inventory.wordSeries, OAI.FKCRT.Inventory.coreCoefficient

  11. lemma OAI.FKCRT.SimpleWalk.kernel_uniform_bound line 134
  12. lemma OAI.FKCRT.SimpleWalk.sum_difference_shift_le line 157
  13. lemma OAI.FKCRT.SimpleWalk.killed_sum_bound line 169
  14. lemma OAI.FKCRT.Inventory.signSum_bounds line 182
  15. def OAI.FKCRT.Inventory.rawSurvival line 191
  16. lemma OAI.FKCRT.Inventory.rawSurvival_union line 192
  17. lemma OAI.FKCRT.Inventory.signSum_measurable line 205
  18. lemma OAI.FKCRT.Inventory.rawKilled_measurable line 208
  19. lemma OAI.FKCRT.Inventory.rawSurvival_measurable line 215
  20. lemma OAI.FKCRT.Inventory.rawSurvival_measure line 218
  21. theorem OAI.FKCRT.Inventory.rawSurvival_bound line 229

    Source documentation

    Reflection gives a uniform first-passage survival bound for the actual inventory stream.

    theorem rawSurvival_bound : ∃ C : ℝ,0<C ∧ ∀ (P : Parameters) (a n : ℕ),0<n →
    (streamLaw P ℕ).real (rawSurvival a n) ≤ C*(a+1)/Real.sqrt n := by
…

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

  22. def OAI.FKCRT.Inventory.bottom line 248
  23. lemma OAI.FKCRT.Inventory.bottom_cons line 249
  24. lemma OAI.FKCRT.Inventory.bottom_all line 254
  25. lemma OAI.FKCRT.Inventory.count_bottom_le line 255
  26. lemma OAI.FKCRT.Inventory.pop_fixed_count line 258
  27. lemma OAI.FKCRT.Inventory.pop_fixed_bottom line 284

    Source documentation

    Removing the freshest burger of type b never reduces the bottom-k supply of another type. If it reduces the type-b supply, all of the remaining type-b supply is in the bottom k.

    lemma pop_fixed_bottom {b a : Bool} {s t : List Bool} (h : pop (some b) s=some t)
    {k : ℕ} (hk : k ≤ t.length) :
    (bottom s k).count a ≤ (bottom t k).count a ∨
      (a=b ∧ t.count a=(bottom t k).count a) := by
…

    Mentions: OAI.FKCRT.Inventory.pop, OAI.FKCRT.Inventory.bottom

  28. def OAI.FKCRT.Inventory.SupplyCondition line 320

    Source documentation

    Exact source criterion, expressed in freshest-first stack order.

    def SupplyCondition (s : List Bool) (os : List Order) : Prop :=
…

    Mentions: OAI.FKCRT.Inventory.Order

  29. lemma OAI.FKCRT.Inventory.fixed_pop_exists line 324
  30. lemma OAI.FKCRT.Inventory.supplyCondition_step line 333
  31. theorem OAI.FKCRT.Inventory.matching_of_supplyCondition line 369
  32. lemma OAI.FKCRT.Inventory.pop_fixed_exists line 390
  33. lemma OAI.FKCRT.Inventory.fixed_run_buffer line 397
  34. def OAI.FKCRT.Inventory.piecesPrefix line 446
  35. def OAI.FKCRT.Inventory.pieceSum line 450
  36. def OAI.FKCRT.Inventory.PieceBuffer line 453
  37. lemma OAI.FKCRT.Inventory.run_pieces_buffer line 456
  38. lemma OAI.FKCRT.Inventory.term_div_zero_of_averages line 496
  39. lemma OAI.FKCRT.Inventory.positive_piece_buffer line 520
  40. def OAI.FKCRT.Inventory.naturalPiecesLaw line 555
  41. instance OAI.FKCRT.Inventory.naturalPieces_probability line 557
  42. lemma OAI.FKCRT.Inventory.iid_piece_averages line 561
  43. lemma OAI.FKCRT.Inventory.iid_piece_buffer_ae line 576
  44. lemma OAI.FKCRT.Inventory.measurableSet_pieceBuffer line 591
  45. lemma OAI.FKCRT.Inventory.positive_piece_buffer_probability line 599
  46. def OAI.FKCRT.Inventory.piecesTail line 624
  47. lemma OAI.FKCRT.Inventory.piecesTail_measurable line 625
  48. lemma OAI.FKCRT.Inventory.piecesTail_preserving line 627
  49. def OAI.FKCRT.Inventory.pieceCoords line 631
  50. lemma OAI.FKCRT.Inventory.pieceCoords_indep line 633
  51. lemma OAI.FKCRT.Inventory.piecesTail_coords line 637
  52. def OAI.FKCRT.Inventory.pieceCylinder line 644
  53. lemma OAI.FKCRT.Inventory.pieceCylinder_coords line 646
  54. lemma OAI.FKCRT.Inventory.pieceCylinder_measurable line 654
  55. lemma OAI.FKCRT.Inventory.pieceCylinder_eq_pi line 658
  56. lemma OAI.FKCRT.Inventory.pieceCylinder_positive line 667
  57. lemma OAI.FKCRT.Inventory.pieceCylinder_tail_rectangle line 679
  58. lemma OAI.FKCRT.Inventory.piecesPrefix_ofFn line 690
  59. lemma OAI.FKCRT.Inventory.piecesPrefix_of_cylinder line 698
  60. lemma OAI.FKCRT.Inventory.piecesPrefix_add line 703