OAI/Probability/FKMaps/SpineBounds.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FKCRT.TreeCoding.PlaneTree.incrementWord_sum line 11
  2. lemma OAI.FKCRT.TreeCoding.PlaneTree.degrees_sum line 18
  3. lemma OAI.FKCRT.TreeCoding.PlaneTree.degree_lt_length line 23
  4. def OAI.FKCRT.TreeCoding.PlaneTree.toCode line 28
  5. lemma OAI.FKCRT.TreeCoding.PlaneTree.toCode_degrees_ofFn line 35
  6. lemma OAI.FKCRT.TreeCoding.PlaneTree.incrementWord_ofFn line 39
  7. def OAI.FKCRT.TreeCoding.PlaneTree.ofCode line 43
  8. lemma OAI.FKCRT.TreeCoding.PlaneTree.ofCode_degrees line 47
  9. lemma OAI.FKCRT.TreeCoding.PlaneTree.ofCode_size line 52
  10. lemma OAI.FKCRT.TreeCoding.PlaneTree.ofCode_injective line 55
  11. lemma OAI.FKCRT.TreeCoding.PlaneTree.ofCode_toCode line 65
  12. abbrev OAI.FKCRT.TreeCoding.PlaneTree.Sized line 69
  13. def OAI.FKCRT.TreeCoding.PlaneTree.sizedEquiv line 71
  14. def OAI.FKCRT.TreeCoding.PlaneTree.mirrored line 77
  15. lemma OAI.FKCRT.TreeCoding.PlaneTree.ofCode_mirrored line 80
  16. lemma OAI.FKCRT.TreeCoding.PlaneTree.mirrored_involutive line 83
  17. def OAI.FKCRT.TreeCoding.PlaneTree.mirrorEquiv line 88
  18. lemma OAI.FKCRT.TreeCoding.PlaneTree.codeWeight_ofCode line 90
  19. lemma OAI.FKCRT.TreeCoding.PlaneTree.mirrored_weight line 95
  20. lemma OAI.FKCRT.TreeCoding.PlaneTree.mirrorEquiv_preserving line 99
  21. lemma OAI.FKCRT.TreeCoding.recordSpineSum_extend line 131
  22. def OAI.FKCRT.TreeCoding.listStream line 180
  23. lemma OAI.FKCRT.TreeCoding.listStream_get line 182
  24. lemma OAI.FKCRT.TreeCoding.integerSum_listStream line 185
  25. lemma OAI.FKCRT.TreeCoding.integerSum_listStream_length line 196
  26. lemma OAI.FKCRT.TreeCoding.listStream_append_prefix line 200
  27. lemma OAI.FKCRT.TreeCoding.prefixSum_reverse_nat line 204
  28. lemma OAI.FKCRT.TreeCoding.list_reverse_prefix_max line 213
  29. lemma OAI.FKCRT.TreeCoding.record_count_reverse line 230
  30. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.record_spine_bound line 236
  31. def OAI.FKCRT.TreeCoding.codeSpineSum line 307

    Source documentation

    The exact deterministic ancestral statistic at preorder position v.

    def codeSpineSum {N : ℕ} (b : ℕ×ℕ → ℝ) (d : Code N) (v : ℕ) : ℝ :=
…

    Mentions: OAI.FKCRT.TreeCoding.Code

  32. lemma OAI.FKCRT.TreeCoding.reverseFirst_prefix_congr line 310
  33. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.code_spine_bound line 317
  34. lemma OAI.FKCRT.TreeCoding.integerSum_list_append line 350
  35. lemma OAI.FKCRT.TreeCoding.reverse_word_strict_negative line 360
  36. def OAI.FKCRT.TreeCoding.profileSum line 369

    Source documentation

    Sum of the genuine ancestral record types of a finite preorder prefix.

    def profileSum (b : ℕ×ℕ → ℝ) (l : List ℕ) : ℝ :=
…
  37. lemma OAI.FKCRT.TreeCoding.profileSum_empty line 372
  38. lemma OAI.FKCRT.TreeCoding.profileSum_attach line 375
  39. lemma OAI.FKCRT.TreeCoding.reverseFirst_list_prefix line 428
  40. lemma OAI.FKCRT.TreeCoding.code_profileSum line 436
  41. lemma OAI.FKCRT.TreeCoding.PlaneTree.forest_properties line 464
  42. lemma OAI.FKCRT.TreeCoding.PlaneTree.forest_split_index line 477
  43. inductive OAI.FKCRT.TreeCoding.PlaneTree.Profile line 491

    Source documentation

    Literal ancestor offspring/slot list of a preorder vertex. Slot counts siblings to its right.

    inductive Profile : PlaneTree → ℕ → List (ℕ×ℕ) → Prop
  | root (t) : Profile t 0 []
  | child (pre : List PlaneTree) (t : PlaneTree) (post : List PlaneTree) {v a}
      (h : Profile t v a) :
      Profile (node (pre++t::post)) (1+(forestDegrees pre).length+v)
        (((pre++t::post).length,post.length)::a)

    Mentions: OAI.FKCRT.TreeCoding.PlaneTree, OAI.FKCRT.TreeCoding.PlaneTree.forestDegrees

  44. lemma OAI.FKCRT.TreeCoding.PlaneTree.Profile.bound line 498
  45. lemma OAI.FKCRT.TreeCoding.PlaneTree.exists_profile line 506
  46. lemma OAI.FKCRT.TreeCoding.PlaneTree.degrees_take_child line 519
  47. lemma OAI.FKCRT.TreeCoding.PlaneTree.Profile.spineSum line 534
  48. def OAI.FKCRT.TreeCoding.PlaneTree.flipSlot line 558
  49. lemma OAI.FKCRT.TreeCoding.PlaneTree.Profile.slots line 560
  50. lemma OAI.FKCRT.TreeCoding.PlaneTree.Profile.mirrored line 569
  51. lemma OAI.FKCRT.TreeCoding.distribution_norm_tight line 590
  52. lemma OAI.FKCRT.TreeCoding.code_height_le_norm line 634
  53. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.code_height_tight line 656
  54. lemma OAI.FKCRT.TreeCoding.polynomial_exp_sqrt line 684
  55. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.code_spine_exp_vanish line 695
  56. lemma OAI.FKCRT.TreeCoding.spine_exp_ceiling_bound line 715
  57. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.uniform_bounded_spine_limit line 740

    Source documentation

    All-vertex bounded ancestral sums under the actual conditioned code law. The centering is the derived spine expectation, not an assumed path average.

    theorem CriticalEvenOffspring.uniform_bounded_spine_limit (p : CriticalEvenOffspring)
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (b : ℕ×ℕ → ℝ) {R ε : ℝ} (hR : 0<R) (hb : ∀ z,|b z|≤R) (hε : 0<ε) :
    Tendsto (fun n => (p.codeLaw n).real {c | ∃ v≤2*n+1,
      ε*Real.sqrt ((2*n+1:ℕ):ℝ)< |codeSpineSum b c v-(∫ z,b z ∂p.spineLaw)*height c.val v|})
      atTop (𝓝 0) := by
…

    Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.codeSpineSum, OAI.FKCRT.TreeCoding.height