OAI/Probability/FKMaps/HeightBounds.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FKCRT.TreeCoding.LadderEnumeration.prefixMaximum line 10
2. lemma OAI.FKCRT.TreeCoding.prefix_record_remainder line 15
3. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.prefix_record_uniform_remainder line 22
4. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.prefix_record_remainder_probability line 31
5. lemma OAI.FKCRT.TreeCoding.le_prefixMaximum line 50
6. lemma OAI.FKCRT.TreeCoding.prefixMaximum_le line 54
7. lemma OAI.FKCRT.TreeCoding.prefixMaximum_mono line 58
8. lemma OAI.FKCRT.TreeCoding.prefixMaximum_attained line 62
9. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.integerSum_scaled line 67
10. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.prefix_maximum_bound line 73
11. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.prefix_record_error_bound line 90
12. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_prefix_record_error line 120

    Source documentation

    Finite variance suffices for the uniform renewal-record approximation on an unconditioned iid prefix; no upper exponential moment is used.

    theorem CriticalEvenOffspring.iid_prefix_record_error (p : CriticalEvenOffspring)
        {δ : ℝ} (hδ : 0<δ) :
        Tendsto (fun N : ℕ => p.streamLaw.real {x | ∃ k≤N,
          δ*Real.sqrt N <
            |(prefixMaximum (integerSum x) k:ℝ)-(p.variance/2)*(weakRecords (integerSum x) k).card|})
          atTop (𝓝 0) := by
    …

    Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.prefixMaximum, OAI.FKCRT.TreeCoding.integerSum, OAI.FKCRT.TreeCoding.weakRecords

13. lemma OAI.FKCRT.TreeCoding.map_cond_preimage line 173
14. def OAI.FKCRT.TreeCoding.streamPrefix line 179
15. lemma OAI.FKCRT.TreeCoding.measurable_streamPrefix line 181
16. lemma OAI.FKCRT.TreeCoding.totalStep_streamPrefix line 184
17. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.streamPrefix_hasLaw line 188
18. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.streamBridgeLaw line 191
19. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.streamBridge_restrict line 194
20. instance OAI.FKCRT.TreeCoding.(instance at line 202) line 202
21. def OAI.FKCRT.TreeCoding.arrayStream line 208
22. lemma OAI.FKCRT.TreeCoding.integerSum_arrayStream_prefix line 211
23. def OAI.FKCRT.TreeCoding.recordError line 218
24. lemma OAI.FKCRT.TreeCoding.recordError_congr line 221
25. lemma OAI.FKCRT.TreeCoding.recordError_arrayStream_prefix line 225
26. lemma OAI.FKCRT.TreeCoding.iidSplit_streamPrefix line 229
27. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.prefix_domination_stream line 232
28. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.prefix_record_domination line 249
29. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_prefix_record_error line 265

    Source documentation

    The uniform record approximation survives conditioning on every fixed proper prefix. The remaining terminal segment is handled separately.

    theorem CriticalEvenOffspring.bridge_prefix_record_error (p : CriticalEvenOffspring)
        {J : ℕ} (hJ : 0<J) (m r : ℕ → ℕ)
        (hs : ∀ n, m n+r n=2*n+1) (hfrac : ∀ᶠ n in atTop, 2*n+1 ≤ J*r n)
        {δ : ℝ} (hδ : 0<δ) :
        Tendsto (fun n => (p.streamBridgeLaw n).real {x | ∃ k ≤ m n,
          δ*Real.sqrt ((2*n+1:ℕ):ℝ)<recordError (p.variance/2) (integerSum x) k}) atTop (𝓝 0) := by
    …

    Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.recordError, OAI.FKCRT.TreeCoding.integerSum

30. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.streamBridge_reverse line 286
31. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.integer_maximal_bound line 294
32. lemma OAI.FKCRT.TreeCoding.integerSum_prefix_event line 310
33. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_initial_maximal_bound line 319
34. lemma OAI.FKCRT.TreeCoding.weakRecords_mono line 337
35. lemma OAI.FKCRT.TreeCoding.weakRecords_suffix_card_le line 344

    Source documentation

    New absolute weak records are a subset of records in the translated suffix.

    lemma weakRecords_suffix_card_le (S : ℕ → ℤ) {m n : ℕ} (h : m ≤ n) :
        (weakRecords S n).card  ≤  (weakRecords S m).card+
          (weakRecords (fun k => S (m+k)-S m) (n-m)).card := by
    …

    Mentions: OAI.FKCRT.TreeCoding.weakRecords

36. lemma OAI.FKCRT.TreeCoding.weakRecords_suffix_of_ladder_level line 366
37. lemma OAI.FKCRT.TreeCoding.prefixMaximum_tail_le line 388
38. lemma OAI.FKCRT.TreeCoding.prefix_record_error_tail line 401

    Source documentation

    Uniform numerical estimate used to pass from a truncated bridge to its full record count. It needs only attained maxima and a one-sided suffix bound.

    lemma prefix_record_error_tail {x : ℕ → ℕ} {m n h : ℕ} (hmn : m ≤ n)
        (hx : HasAllLadders (streamShift m x)) {ν a : ℝ} (hν : 0 ≤ ν) (ha : 0 ≤ a)
        (hla : a  ≤  renewalLevel h (streamShift m x))
        (hosc : ∀ k, m ≤ k → k ≤ n → (integerSum x k:ℝ)-(integerSum x m:ℝ)<a) :
        |(prefixMaximum (integerSum x) n:ℝ)-ν*(weakRecords (integerSum x) n).card|  ≤ 
          |(prefixMaximum (integerSum x) m:ℝ)-ν*(weakRecords (integerSum x) m).card|+a+ν*h := by
    …

    Mentions: OAI.FKCRT.TreeCoding.HasAllLadders, OAI.FKCRT.TreeCoding.streamShift, OAI.FKCRT.TreeCoding.renewalLevel, OAI.FKCRT.TreeCoding.integerSum, OAI.FKCRT.TreeCoding.prefixMaximum, OAI.FKCRT.TreeCoding.weakRecords

39. lemma OAI.FKCRT.TreeCoding.cond_real_le line 429
40. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.stream_endpoint_probability line 437
41. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.stream_endpoint_limit line 444
42. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.streamBridge_shift_ladders line 449
43. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_shift_ladder_bound line 453
44. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_terminal_maximal_bound line 467
45. lemma OAI.FKCRT.TreeCoding.tendsto_natCeil_comp_atTop line 504
46. lemma OAI.FKCRT.TreeCoding.polynomial_geometric_ceil line 510
47. lemma OAI.FKCRT.TreeCoding.odd_size_tendsto line 524
48. lemma OAI.FKCRT.TreeCoding.odd_sqrt_tendsto line 527
49. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_geometric_vanish line 530
50. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_record_tail_bound line 550
51. lemma OAI.FKCRT.TreeCoding.terminal_ratio_bound line 578
52. lemma OAI.FKCRT.TreeCoding.division_prefix_properties line 605
53. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_record_error line 626

    Source documentation

    The weak-record approximation for the whole conditioned bridge. The terminal part is controlled by reversal and a second-moment maximal inequality, not by independence at the random Vervaat cut.

    theorem CriticalEvenOffspring.bridge_record_error (p : CriticalEvenOffspring)
        {δ : ℝ} (hδ : 0<δ) :
        Tendsto (fun n => (p.streamBridgeLaw n).real {x |
          δ*Real.sqrt ((2*n+1:ℕ):ℝ)<recordError (p.variance/2) (integerSum x) (2*n+1)})
          atTop (𝓝 0) := by
    …

    Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.recordError, OAI.FKCRT.TreeCoding.integerSum

54. instance OAI.FKCRT.TreeCoding.(instance at line 709) line 709
55. instance OAI.FKCRT.TreeCoding.(instance at line 710) line 710
56. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.codeLaw line 712
57. instance OAI.FKCRT.TreeCoding.(instance at line 715) line 715
58. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.code_integral line 718
59. lemma OAI.FKCRT.TreeCoding.integerSum_arrayStream_bridge line 725
60. lemma OAI.FKCRT.TreeCoding.measurable_recordError_integerSum line 745
61. def OAI.FKCRT.TreeCoding.badHeightFraction line 751
62. lemma OAI.FKCRT.TreeCoding.badHeightFraction_nonneg line 754
63. lemma OAI.FKCRT.TreeCoding.recordError_reverse_array_bridge line 758
64. lemma OAI.FKCRT.TreeCoding.recordError_reverse_streamPrefix line 766
65. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.code_average_height_error line 774
66. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.average_height_error_limit line 810

    Source documentation

    The expected proportion of vertices with macroscopic height/walk error vanishes. This is an exact consequence of cyclic averaging and the full conditioned-bridge weak-record theorem.

    theorem CriticalEvenOffspring.average_height_error_limit (p : CriticalEvenOffspring)
        {δ : ℝ} (hδ : 0<δ) :
        Tendsto (fun n => ∫ d,badHeightFraction (p.variance/2)
          (δ*Real.sqrt ((2*n+1:ℕ):ℝ)) d ∂p.codeLaw n) atTop (𝓝 0) := by
    …

    Mentions: OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.TreeCoding.badHeightFraction