OAI/Probability/TraceReconstruction/Scales.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TraceReconstruction.scaleA line 16

   Source documentation

   The exact real scale exponents in the scale inequalities; natural indices are zero-based.

   def scaleA (b j : ℕ) (ε : ℝ) : ℝ := (1+ε)* (2:ℝ)^j / (2:ℝ)^b - ε

2. def OAI.TraceReconstruction.scaleKappa line 18
3. def OAI.TraceReconstruction.sourceEpsilon line 21
4. theorem OAI.TraceReconstruction.scaleA_top line 23
5. theorem OAI.TraceReconstruction.scaleA_step line 28
6. theorem OAI.TraceReconstruction.scaleKappa_step line 33
7. def OAI.TraceReconstruction.forcedDecay line 41
8. theorem OAI.TraceReconstruction.forcedDecay_summand line 46
9. theorem OAI.TraceReconstruction.forcedDecay_lower line 54
10. theorem OAI.TraceReconstruction.nat_add_one_le_two_pow line 75
11. theorem OAI.TraceReconstruction.sourceEpsilon_pos line 80
12. theorem OAI.TraceReconstruction.sourceEpsilon_loss line 84
13. theorem OAI.TraceReconstruction.forcedDecay_margin line 117
14. def OAI.TraceReconstruction.workingDeletion line 133
15. def OAI.TraceReconstruction.blockGain line 134
16. def OAI.TraceReconstruction.warmupBlocks line 135
17. def OAI.TraceReconstruction.sourceDepth line 136
18. def OAI.TraceReconstruction.totalScoreExponent line 137
19. def OAI.TraceReconstruction.finalSlope line 139
20. theorem OAI.TraceReconstruction.workingDeletion_bounds line 141
21. theorem OAI.TraceReconstruction.workingScale_bounds line 152
22. theorem OAI.TraceReconstruction.blockGain_two line 162
23. theorem OAI.TraceReconstruction.blockGain_pos line 163
24. theorem OAI.TraceReconstruction.totalScoreExponent_exact line 168
25. theorem OAI.TraceReconstruction.sourceDepth_lower line 188
26. theorem OAI.TraceReconstruction.totalScoreExponent_slope_lower line 194
27. theorem OAI.TraceReconstruction.sourceDepth_tendsto line 208
28. theorem OAI.TraceReconstruction.eventually_exponent_margin line 221

    Source documentation

    A fixed multiplicative constant is absorbed by any strict exponent slope margin, with two independently diverging instance parameters.

    theorem eventually_exponent_margin {N H d : ℕ → ℝ} {α c K a : ℝ}
        (hN : Tendsto N atTop atTop) (hH : Tendsto H atTop atTop)
        (hα : c < α) (ha : 0 < a)
        (hd : ∀ᶠ k in atTop, α*Real.log (H k)-K ≤ d k) :
        ∀ᶠ k in atTop, (N k)^(c*Real.log (H k)) ≤ a*(N k)^(d k) := by
    …

29. def OAI.TraceReconstruction.sourceDimension line 254

    Source documentation

    Literal source block dimensions, with zero-based block number.

    def sourceDimension (B i : ℕ) : ℕ := if i < warmupBlocks B then 2 else B

    Mentions: OAI.TraceReconstruction.warmupBlocks

30. def OAI.TraceReconstruction.sourceScaleProduct line 256
31. def OAI.TraceReconstruction.sourceTargetScale line 260

    Source documentation

    The backwards target scales as an exact product of source exponents.

    def sourceTargetScale (B D : ℕ) (n : ℝ) (i : ℕ) : ℝ := n ^ sourceScaleProduct B D i

    Mentions: OAI.TraceReconstruction.sourceScaleProduct

32. theorem OAI.TraceReconstruction.sourceTargetScale_top line 262
33. theorem OAI.TraceReconstruction.sourceTargetScale_step line 265
34. theorem OAI.TraceReconstruction.sourceEpsilon_small line 272
35. theorem OAI.TraceReconstruction.scaleA_zero_lower line 286
36. theorem OAI.TraceReconstruction.sourceScaleProduct_lower line 299
37. theorem OAI.TraceReconstruction.sourceDepth_upper line 336
38. theorem OAI.TraceReconstruction.sourceDepth_power line 343
39. theorem OAI.TraceReconstruction.sourceTargetScale_log_lower line 355

    Source documentation

    Source smallest-scale lower bound, with an absolute explicit factor.

    theorem sourceTargetScale_log_lower (B : ℕ) (ζ H n : ℝ) (i : ℕ) (hB : 2 ≤ B)
        (hζ : ζ ≤ 1) (hH : 1 ≤ H) (hn : 1 < n) :
        Real.log n/(2*H^(1-ζ)) ≤ Real.log (sourceTargetScale B (sourceDepth B ζ H) n i) := by
    …

    Mentions: OAI.TraceReconstruction.sourceTargetScale, OAI.TraceReconstruction.sourceDepth

40. theorem OAI.TraceReconstruction.sourceDepth_polynomial_absorption line 369

    Source documentation

    Polynomial depth losses are negligible compared with the H-zeta gain. This statement has no bounded-deletion-rate premise.

    theorem sourceDepth_polynomial_absorption (B h : ℕ) (ζ : ℝ) (hB : 2 ≤ B)
        (hζ : ζ∈Set.Ioo 0 1) {H : ℕ → ℝ} (hH : Tendsto H atTop atTop) :
        Tendsto (fun k => ((sourceDepth B ζ (H k):ℝ)+1)^h/(H k)^ζ) atTop (nhds 0) := by
    …

    Mentions: OAI.TraceReconstruction.sourceDepth

41. theorem OAI.TraceReconstruction.sourceTargetScale_epsilon_log_lower line 398

    Source documentation

    Uniform quantitative scale margin. This is the source's Lambda*H^zeta bound, before any little-o notation or parameter choices.

    theorem sourceTargetScale_epsilon_log_lower (B : ℕ) (ζ H n Λ : ℝ) (i : ℕ)
        (hB : 2 ≤ B) (hζ : ζ ≤ 1) (hH : 1 ≤ H) (hn : 1 < n)
        (hΛ : 0 < Λ) (hrel : Real.log n=Λ*H) :
        Λ*H^ζ/(2*(2:ℝ)^(4*B+100)*((sourceDepth B ζ H:ℝ)+1)) ≤
          sourceEpsilon B (sourceDepth B ζ H)*
            Real.log (sourceTargetScale B (sourceDepth B ζ H) n i) := by
    …

    Mentions: OAI.TraceReconstruction.sourceDepth, OAI.TraceReconstruction.sourceEpsilon, OAI.TraceReconstruction.sourceTargetScale

42. theorem OAI.TraceReconstruction.source_absorption_ratio_bound line 416
43. theorem OAI.TraceReconstruction.source_uniform_absorption line 434

    Source documentation

    Joint-regime uniform absorption at the genuine backwards scales, with an arbitrary index choice and with the channel unchanged across scales.

    theorem source_uniform_absorption (B h : ℕ) (ζ : ℝ) (hB : 2 ≤ B) (hζ : ζ∈Set.Ioo 0 1)
        {n Λ H : ℕ → ℝ} (i : ℕ → ℕ) (hn : Tendsto n atTop atTop) (hH : Tendsto H atTop atTop)
        (hΛ : ∀k,0 < Λ k) (hrel : ∀k,Real.log (n k)=Λ k*H k) :
        Tendsto (fun k => ((sourceDepth B ζ (H k):ℝ)+1)^h*Λ k /
          (sourceEpsilon B (sourceDepth B ζ (H k))*
            Real.log (sourceTargetScale B (sourceDepth B ζ (H k)) (n k) (i k)))) atTop (nhds 0) := by
    …

    Mentions: OAI.TraceReconstruction.sourceDepth, OAI.TraceReconstruction.sourceEpsilon, OAI.TraceReconstruction.sourceTargetScale

44. theorem OAI.TraceReconstruction.source_uniform_exp_absorption line 455
45. theorem OAI.TraceReconstruction.source_deletion_uniform_absorption line 495

    Source documentation

    Direct instantiation with the manuscript's known deletion rate: Lambda is q^{-3}, H=q^3 log n, never recomputed at an intermediate scale.

    theorem source_deletion_uniform_absorption (B h : ℕ) (ζ : ℝ) (hB : 2 ≤ B)
        (hζ : ζ∈Set.Ioo 0 1) {n q : ℕ → ℝ} (i : ℕ → ℕ)
        (hq : ∀k,0 < q k) (hn : Tendsto n atTop atTop)
        (hH : Tendsto (fun k => (q k)^3*Real.log (n k)) atTop atTop) :
        Tendsto (fun k =>
          ((sourceDepth B ζ ((q k)^3*Real.log (n k)):ℝ)+1)^h*(q k)^(-3:ℤ) /
          (sourceEpsilon B (sourceDepth B ζ ((q k)^3*Real.log (n k)))*
            Real.log (sourceTargetScale B (sourceDepth B ζ ((q k)^3*Real.log (n k)))
              (n k) (i k)))) atTop (nhds 0) := by
    …

    Mentions: OAI.TraceReconstruction.sourceDepth, OAI.TraceReconstruction.sourceEpsilon, OAI.TraceReconstruction.sourceTargetScale

46. def OAI.TraceReconstruction.PowerRate line 520

    Source documentation

    Logarithmic order along a genuine diverging positive scale.

    def PowerRate (N f : ℕ → ℝ) (a : ℝ) : Prop :=
    …

47. def OAI.TraceReconstruction.PowerUpper line 524

    Source documentation

    A robust upper order, with arbitrary strictly positive exponent slack.

    def PowerUpper (N f : ℕ → ℝ) (a : ℝ) : Prop :=
    …

48. theorem OAI.TraceReconstruction.PowerRate.congr line 529
49. theorem OAI.TraceReconstruction.PowerRate.const line 534
50. theorem OAI.TraceReconstruction.PowerRate.base line 538
51. theorem OAI.TraceReconstruction.PowerRate.mul line 545
52. theorem OAI.TraceReconstruction.PowerRate.div line 552
53. theorem OAI.TraceReconstruction.PowerRate.rpow line 559
54. theorem OAI.TraceReconstruction.PowerRate.pow line 567
55. theorem OAI.TraceReconstruction.PowerRate.sqrt line 571
56. theorem OAI.TraceReconstruction.PowerRate.inv line 575
57. theorem OAI.TraceReconstruction.PowerRate.const_mul line 579
58. theorem OAI.TraceReconstruction.PowerRate.mul_const line 583
59. theorem OAI.TraceReconstruction.PowerRate.div_const line 587
60. theorem OAI.TraceReconstruction.PowerRate.upper line 591
61. theorem OAI.TraceReconstruction.PowerRate.lower line 598
62. theorem OAI.TraceReconstruction.PowerRate.tendsto_atTop line 604
63. theorem OAI.TraceReconstruction.PowerUpper.mono line 609
64. theorem OAI.TraceReconstruction.PowerUpper.congr line 612
65. theorem OAI.TraceReconstruction.PowerUpper.of_abs_le line 617
66. theorem OAI.TraceReconstruction.PowerUpper.zero line 623
67. theorem OAI.TraceReconstruction.PowerUpper.mul line 628
68. theorem OAI.TraceReconstruction.PowerUpper.pow line 638
69. theorem OAI.TraceReconstruction.PowerUpper.add line 648
70. theorem OAI.TraceReconstruction.PowerUpper.sum line 661
71. theorem OAI.TraceReconstruction.PowerRate.add_const line 672
72. theorem OAI.TraceReconstruction.PowerRate.of_tendsto line 689
73. theorem OAI.TraceReconstruction.PowerUpper.tendsto_zero line 693
74. theorem OAI.TraceReconstruction.PowerRate.of_ratio line 699
75. theorem OAI.TraceReconstruction.PowerRate.nat_floor line 714
76. theorem OAI.TraceReconstruction.PowerRate.exp_neg_upper line 719