OAI/Combinatorics/KServer/RankProportions.lean

GitHub source file

122 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KServer.RankTracking.held line 12

   Source documentation

   Reference reset policy run on every input step.

   def held (test : ℝ → ℝ → Prop) [DecidableRel test] (p : ℕ → Ω → ℝ) : ℕ → Ω → ℝ
     | 0, ω => p 0 ω
     | t+1, ω => if test (p (t+1) ω) (held test p t ω) then p (t+1) ω else held test p t ω
   
   omit [Fintype Ω] in

2. lemma OAI.KServer.RankTracking.held_range line 17
3. lemma OAI.KServer.RankTracking.held_adapted line 24
4. def OAI.KServer.RankTracking.potential line 36

   Source documentation

   Exact bounded affine potential used in the manuscript.

   def potential (p r : ℝ) : ℝ := p*(1-p)+(p-r)^2

5. lemma OAI.KServer.RankTracking.potential_affine line 37
6. lemma OAI.KServer.RankTracking.potential_bounds line 38
7. lemma OAI.KServer.RankTracking.slope_abs line 48
8. def OAI.KServer.RankTracking.credit line 51
9. lemma OAI.KServer.RankTracking.credit_step line 55
10. lemma OAI.KServer.RankTracking.expected_credit_step line 64
11. theorem OAI.KServer.RankTracking.reset_credit_bound line 88

    Source documentation

    Signed filtering is retained at every step, before the reset decision.

    theorem reset_credit_bound (test : ℝ → ℝ → Prop) [DecidableRel test]
        {w : Ω → ℝ} (hw : ∀ ω, 0 ≤ w ω) (hw1 : ∑ ω, w ω=1) (R : FilteredRanks w) (N : ℕ) :
        (∑ t ∈ Finset.range N, avg w (credit test R.p t)) ≤
          (∑ t ∈ Finset.range N, avg w (fun ω => |R.p (t+1) ω-R.before (t+1) ω|))+1 := by
    …

    Mentions: OAI.KServer.RankTracking.FilteredRanks, OAI.KServer.RankTracking.avg, OAI.KServer.RankTracking.credit

12. lemma OAI.KServer.RankTracking.sqrt_factor_gap_one line 108

    Source documentation

    Source's scalar factor-loss constant, including zero endpoints.

    lemma sqrt_factor_gap_one {a b ξ : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b)
        (hξ : 0 < ξ) (hξh : ξ < 1/2) (hfail : (1+ξ)*b ≤ a) :
        (ξ/5)*(a-b) ≤ (Real.sqrt a-Real.sqrt b)^2 := by
    …

13. lemma OAI.KServer.RankTracking.sqrt_factor_gap line 138
14. def OAI.KServer.RankTracking.factorTest line 151
15. instance OAI.KServer.RankTracking.(instance at line 154) line 154
16. lemma OAI.KServer.RankTracking.factor_held_accurate line 157
17. lemma OAI.KServer.RankTracking.factor_movement_credit line 180
18. theorem OAI.KServer.RankTracking.multiplicative_rank_tracking line 206

    Source documentation

    Actual causal multiplicative held estimates, with horizon-independent additive initialization allowance and the source's C/xi drift dependence.

    theorem multiplicative_rank_tracking {w : Ω → ℝ} (hw : ∀ ω, 0 ≤ w ω)
        (hw1 : ∑ ω, w ω=1) (R : FilteredRanks w) (f : ℝ → ℝ) {ξ K : ℝ}
        (hξ : 0 < ξ) (hξh : ξ < 1/2) (hK : 0 ≤ K)
        (hf : ∀ p ∈ Set.Icc (0:ℝ) 1, 0 ≤ f p)
        (hlip : ∀ p ∈ Set.Icc (0:ℝ) 1, ∀ r ∈ Set.Icc (0:ℝ) 1,
          |Real.sqrt (f p)-Real.sqrt (f r)| ≤ K*|p-r|) :
        ∃ estimate : ℕ → Ω → ℝ,
          (∀ t, Adapted (R.history t) (estimate t)) ∧
          (∀ t ω, (1+ξ)⁻¹*f (R.p t ω) ≤ estimate t ω ∧ estimate t ω ≤ (1+ξ)*f (R.p t ω)) ∧
          ∀ N, (∑ t ∈ Finset.range N, avg w (fun ω => |estimate (t+1) ω-estimate t ω|)) ≤
            (5*K^2/ξ)*((∑ t ∈ Finset.range N, avg w (fun ω => |R.p (t+1) ω-R.before (t+1) ω|))+1) := by
    …

    Mentions: OAI.KServer.RankTracking.FilteredRanks, OAI.KServer.RankTracking.Adapted, OAI.KServer.RankTracking.avg

19. def OAI.KServer.RankTracking.absoluteTest line 231
20. instance OAI.KServer.RankTracking.(instance at line 232) line 232
21. def OAI.KServer.RankTracking.resetIndicator line 234
22. theorem OAI.KServer.RankTracking.absolute_rank_tracking line 239

    Source documentation

    The absolute tracker used for all core flags. Its cost is the actual number of reference refreshes, not the variation of the raw posteriors.

    theorem absolute_rank_tracking {w : Ω → ℝ} (hw : ∀ ω, 0 ≤ w ω)
        (hw1 : ∑ ω, w ω=1) (R : FilteredRanks w) {δ : ℝ} (hδ : 0 < δ) :
        (∀ t ω, |R.p t ω-held (absoluteTest δ) R.p t ω| ≤ δ) ∧
        ∀ N, (∑ t ∈ Finset.range N, avg w (resetIndicator (absoluteTest δ) R.p t)) ≤
          (δ^2)⁻¹*((∑ t ∈ Finset.range N, avg w (fun ω => |R.p (t+1) ω-R.before (t+1) ω|))+1) := by
    …

    Mentions: OAI.KServer.RankTracking.FilteredRanks, OAI.KServer.RankTracking.held, OAI.KServer.RankTracking.absoluteTest, OAI.KServer.RankTracking.avg, OAI.KServer.RankTracking.resetIndicator

23. lemma OAI.KServer.RankTracking.held_variation_step line 273

    Source documentation

    Causal hold-or-reset rules never increase total scalar input variation. The deviation from the held reference pays for any waiting interval.

    lemma held_variation_step (test : ℝ → ℝ → Prop) [DecidableRel test]
        (p : ℕ → Ω → ℝ) (t : ℕ) (ω : Ω) :
        |held test p (t+1) ω-held test p t ω|+|p (t+1) ω-held test p (t+1) ω| ≤
          |p (t+1) ω-p t ω|+|p t ω-held test p t ω| := by
    …

    Mentions: OAI.KServer.RankTracking.held

24. theorem OAI.KServer.RankTracking.held_variation line 282
25. lemma OAI.KServer.RankTracking.factor_change_charge line 295
26. def OAI.KServer.CoreFlags.tolerance line 315

    Source documentation

    §03: the literal absolute reference tolerance p*/8, p*=1/24.

    def tolerance : ℝ := (1/24)/8

27. lemma OAI.KServer.CoreFlags.tolerance_pos line 316
28. def OAI.KServer.CoreFlags.flag line 317
29. def OAI.KServer.CoreFlags.change line 320
30. lemma OAI.KServer.CoreFlags.flag_accuracy line 323
31. lemma OAI.KServer.CoreFlags.core_upper line 333
32. lemma OAI.KServer.CoreFlags.noncore_lower line 340
33. lemma OAI.KServer.CoreFlags.small_is_core line 348
34. lemma OAI.KServer.CoreFlags.change_le_reset line 354
35. theorem OAI.KServer.CoreFlags.core_change_budget line 364

    Source documentation

    The exact number of changed flags is charged to the fixed absolute trackers. No raw posterior total variation is charged.

    theorem core_change_budget {J : Type} [Fintype J]
        (hw : ∀ ω, 0 ≤ w ω) (hw1 : ∑ ω, w ω=1) (R : J → FilteredRanks w) (N : ℕ) :
        (∑ t ∈ range N, avg w (fun ω => ∑ j, change (R j) t ω)) ≤
          (tolerance^2)⁻¹ * ((∑ t ∈ range N, avg w
            (fun ω => ∑ j, |(R j).p (t+1) ω-(R j).before (t+1) ω|)) + Fintype.card J) := by
    …

    Mentions: OAI.KServer.CoreFlags.change, OAI.KServer.CoreFlags.tolerance

36. lemma OAI.KServer.CoreFlags.flag_adapted line 388
37. lemma OAI.KServer.CoreFlags.flagged_mass_change line 395

    Source documentation

    Changing core flags after inspecting new posteriors costs at most one per changed flag, since each rank remains in [0,1].

    lemma flagged_mass_change {J : Type} [Fintype J] (p : J → ℝ)
        (hp : ∀ j, p j ∈ Set.Icc 0 1) (K K' : J → Bool) :
        |(∑ j, if K' j then p j else 0) - (∑ j, if K j then p j else 0)| ≤
          ∑ j, if K' j = K j then (0:ℝ) else 1 := by
    …

38. def OAI.KServer.RankFunctions.pstar line 417
39. def OAI.KServer.RankFunctions.sstar line 418
40. def OAI.KServer.RankFunctions.A line 420
41. def OAI.KServer.RankFunctions.B line 421
42. def OAI.KServer.RankFunctions.middle line 422
43. def OAI.KServer.RankFunctions.rank line 425
44. def OAI.KServer.RankFunctions.slope line 429
45. lemma OAI.KServer.RankFunctions.middle_literal line 433
46. lemma OAI.KServer.RankFunctions.derivative_ite_le line 440

    Source documentation

    C¹ gluing at a scalar threshold, applied twice to the rank formula.

    lemma derivative_ite_le {f g f' g' : ℝ → ℝ} {c : ℝ}
        (hf : ∀ x, HasDerivAt f (f' x) x) (hg : ∀ x, HasDerivAt g (g' x) x)
        (he : f c = g c) (hd : f' c = g' c) (x : ℝ) :
        HasDerivAt (fun p => if p ≤ c then f p else g p)
          (if x ≤ c then f' x else g' x) x := by
    …

47. lemma OAI.KServer.RankFunctions.middle_derivative line 476
48. lemma OAI.KServer.RankFunctions.rank_derivative line 483
49. lemma OAI.KServer.RankFunctions.coefficients line 497
50. lemma OAI.KServer.RankFunctions.middle_slope_monotone line 502
51. lemma OAI.KServer.RankFunctions.slope_monotone line 513
52. lemma OAI.KServer.RankFunctions.rank_convex line 540
53. lemma OAI.KServer.RankFunctions.rank_antitone line 547
54. lemma OAI.KServer.RankFunctions.rank_zero line 559
55. lemma OAI.KServer.RankFunctions.rank_cutoff line 561
56. lemma OAI.KServer.RankFunctions.rank_pos line 569
57. lemma OAI.KServer.RankFunctions.rank_nonneg line 584
58. lemma OAI.KServer.RankFunctions.rank_range line 590
59. def OAI.KServer.RankFunctions.parameterSlope line 595

    Source documentation

    Minus the derivative in beta, exactly as defined after eq:explicit-rank.

    def parameterSlope (p : ℝ) : ℝ :=
    …

60. lemma OAI.KServer.RankFunctions.rank_parameter_affine line 599
61. lemma OAI.KServer.RankFunctions.parameterSlope_nonneg line 604
62. lemma OAI.KServer.RankFunctions.rank_parameter_antitone line 612
63. lemma OAI.KServer.RankFunctions.parameterSlope_compare line 619
64. lemma OAI.KServer.RankFunctions.sqrt_slope_bound line 645
65. lemma OAI.KServer.RankFunctions.sqrt_right_derivative line 686
66. lemma OAI.KServer.RankFunctions.sqrt_rank_lipschitz line 698
67. def OAI.KServer.RankFunctions.sizeRank line 724

    Source documentation

    The broader size function, literally as in §03.

    def sizeRank (p : ℝ) : ℝ := (max (3 / 4 - p) 0)^2 / (3 / 4)^2

68. lemma OAI.KServer.RankFunctions.sizeRank_piece line 726
69. lemma OAI.KServer.RankFunctions.sizeRank_derivative line 732
70. lemma OAI.KServer.RankFunctions.sizeRank_convex line 746
71. lemma OAI.KServer.RankFunctions.sizeRank_zero line 752
72. lemma OAI.KServer.RankFunctions.sizeRank_one line 753
73. lemma OAI.KServer.RankFunctions.sizeRank_nonneg line 754
74. lemma OAI.KServer.RankFunctions.sizeRank_le_complement line 756
75. lemma OAI.KServer.RankFunctions.sqrt_sizeRank line 764
76. lemma OAI.KServer.RankFunctions.sqrt_sizeRank_lipschitz line 770
77. def OAI.KServer.FineCaps.estimate line 790
78. lemma OAI.KServer.FineCaps.estimate_range line 793
79. lemma OAI.KServer.FineCaps.estimate_accuracy line 797
80. lemma OAI.KServer.FineCaps.relative_absolute line 803
81. lemma OAI.KServer.FineCaps.estimate_absolute line 818
82. lemma OAI.KServer.FineCaps.interpolate_rank line 824
83. def OAI.KServer.FineCaps.interpolated line 829
84. lemma OAI.KServer.FineCaps.interpolated_range line 832
85. lemma OAI.KServer.FineCaps.interpolated_accuracy line 843
86. lemma OAI.KServer.FineCaps.noncore_interpolation_error line 864

    Source documentation

    §03 flex-estimate error, including exact zero at the common cutoff.

    lemma noncore_interpolation_error {ξ a z ε : ℝ} (hξ : 0 < ξ) (ha : a ∈ Set.Icc 0 1)
        (hz : z ∈ Set.Icc 0 (1/100 : ℝ)) (hza : z ≤ a/100) (hea : a/100-z ≤ ε)
        (R : FilteredRanks w) (t : ℕ) (ω : Ω) (hf : flag R t ω=false) :
        |interpolated ξ a R t ω-rank z (R.p t ω)| ≤ (ξ+ε)*rank z (R.p t ω) := by
    …

    Mentions: OAI.KServer.FineCaps.interpolated

87. lemma OAI.KServer.FineCaps.cap_scaling line 893

    Source documentation

    Deterministic scaling of an accurately tracked flex term. Parameters here are already normalized by ell: l=lambda_b/ell, e=error/ell, g=gamma/ell, b=epsilon_b/ell. All zero-flex cases are included.

    lemma cap_scaling {F E Fc l e g b : ℝ}
        (hF : 0 ≤ F) (hE : |E-F| ≤ e*F) (he : 0 ≤ e)
        (hl : 0 < l) (hls : l ≤ 1/4) (hel : e ≤ l/4)
        (hg : 4*l ≤ g) (hb : 4*l ≤ b) (hfc : Fc ≤ (1-g)*F) :
        (Fc ≤ (1-l)*E ∧ (1-l)*E ≤ F) ∧
        (F ≤ (1+l)*E ∧ (1+l)*E ≤ (1+b)*F) := by
    …

88. lemma OAI.KServer.FineCaps.estimate_variation_budget line 919

    Source documentation

    The concrete endpoint tracker, not a separately postulated estimate.

    lemma estimate_variation_budget (hw : ∀ ω, 0 ≤ w ω) (hw1 : ∑ ω, w ω=1)
        {ξ z : ℝ} (hξ : 0 < ξ) (hξh : ξ < 1/2) (hz : z ∈ Set.Icc 0 (1/100 : ℝ))
        (R : FilteredRanks w) (N : ℕ) :
        (∑ t ∈ range N, avg w (fun ω => |estimate ξ z R (t+1) ω-estimate ξ z R t ω|)) ≤
          (80/ξ)*((∑ t ∈ range N, avg w (fun ω => |R.p (t+1) ω-R.before (t+1) ω|))+1) := by
    …

    Mentions: OAI.KServer.FineCaps.estimate

89. lemma OAI.KServer.FineCaps.interpolated_variation line 941
90. def OAI.KServer.FineCaps.capTerm line 959

    Source documentation

    One rank's core-plus-scaled-flex contribution to the actual cap.

    def capTerm (ξ a κ : ℝ) (R : FilteredRanks w) (t : ℕ) (ω : Ω) : ℝ :=
    …

91. lemma OAI.KServer.FineCaps.capTerm_range line 962
92. lemma OAI.KServer.FineCaps.capTerm_variation line 970
93. def OAI.KServer.FineCaps.fineVariation line 998

    Source documentation

    Fine changes can be selected pathwise; wholesale changes are excluded only when the interpolation and scale parameters are actually held fixed.

    def fineVariation (ξ : ℝ) (a κ : ℕ → Ω → ℝ) (wholesale : ℕ → Ω → Bool)
        (R : FilteredRanks w) (t : ℕ) (ω : Ω) : ℝ :=
    …

94. lemma OAI.KServer.FineCaps.fineVariation_step line 1003
95. lemma OAI.KServer.FineCaps.all_endpoint_budget line 1020
96. theorem OAI.KServer.FineCaps.fine_cap_budget line 1043

    Source documentation

    §03 fine-cap budget. The right side has one uniform initialization term per rank, not one per coarse epoch. Arbitrary pathwise nonwholesale selection is valid only after the all-step filtering credits have been accounted for.

    theorem fine_cap_budget {J : Type} [Fintype J]
        (hw : ∀ ω, 0 ≤ w ω) (hw1 : ∑ ω, w ω=1)
        {ξ : ℝ} (hξ : 0 < ξ) (hξh : ξ < 1/2)
        (a κ : J → ℕ → Ω → ℝ) (wholesale : J → ℕ → Ω → Bool)
        (ha : ∀ j t ω, a j t ω ∈ Set.Icc 0 1) (hκ : ∀ j t ω, κ j t ω ∈ Set.Icc 0 2)
        (hhold : ∀ j t ω, wholesale j t ω=false →
          a j (t+1) ω=a j t ω ∧ κ j (t+1) ω=κ j t ω)
        (R : J → FilteredRanks w) (N : ℕ) :
        (∑ t ∈ range N, avg w (fun ω => ∑ j, fineVariation ξ (a j) (κ j) (wholesale j) (R j) t ω)) ≤
          2*(160/ξ+(tolerance^2)⁻¹)*((∑ t ∈ range N, avg w
            (fun ω => ∑ j, |(R j).p (t+1) ω-(R j).before (t+1) ω|))+Fintype.card J) := by
    …

    Mentions: OAI.KServer.FineCaps.fineVariation

97. lemma OAI.KServer.RankOrder.convex_tangent line 1094
98. lemma OAI.KServer.RankOrder.convex_sum_of_prefix line 1108
99. def OAI.KServer.RankOrder.extend line 1136
100. lemma OAI.KServer.RankOrder.extend_fin line 1139
101. lemma OAI.KServer.RankOrder.sum_outside line 1142
102. lemma OAI.KServer.RankOrder.sum_rank_indicators line 1149
103. lemma OAI.KServer.RankOrder.outside_card_bound line 1158
104. lemma OAI.KServer.RankOrder.rank_prefix line 1165

     Source documentation

     Pool rank probabilities, then sort them. Every prefix is bounded below by the corresponding parent rank prefix. Dependence between ranks is arbitrary.

     lemma rank_prefix {Ω : Type*} [Fintype Ω] {n : ℕ}
         (B : Ω → Finset (Fin n)) (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω)
         (σ : Equiv.Perm (Fin n)) (m : ℕ) (hm : m ≤ n) :
         (∑ j ∈ range m, ∑ ω, w ω * (if (B ω).card ≤ j then (1 : ℝ) else 0)) ≤
           ∑ j ∈ range m, extend (fun i => ∑ ω, w ω * (if σ i ∈ B ω then (0 : ℝ) else 1)) j := by
     …

     Mentions: OAI.KServer.RankOrder.extend

105. lemma OAI.KServer.RankOrder.rank_total line 1194
106. lemma OAI.KServer.RankOrder.convex_rank_sum line 1211

     Source documentation

     The convex superadditivity comparison for an arbitrary joint distribution of integer rank indicators. Padding of parent ranks is automatic.

     lemma convex_rank_sum {Ω : Type*} [Fintype Ω] {n : ℕ}
         (B : Ω → Finset (Fin n)) (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω)
         {f : ℝ → ℝ} (hf : ConvexOn ℝ Set.univ f) (hd : ∀ x, DifferentiableAt ℝ f x) :
         (∑ i : Fin n, f (∑ ω, w ω * (if i ∈ B ω then (0 : ℝ) else 1))) ≤
           ∑ j : Fin n, f (∑ ω, w ω * (if (B ω).card ≤ j.val then (1 : ℝ) else 0)) := by
     …

107. lemma OAI.KServer.RankOrder.convex_rank_sum_type line 1239
108. lemma OAI.KServer.RankOrder.sum_below line 1256
109. def OAI.KServer.RankOrder.countRank line 1268

     Source documentation

     Source integer ranks: rank a (with zero-based index) is P(N ≤ a). The probability law is joint, without independent-child assumptions.

     def countRank {Ω : Type*} [Fintype Ω] (w : Ω → ℝ) (N : Ω → ℕ) (a : ℕ) : ℝ :=
     …

110. lemma OAI.KServer.RankOrder.countRank_range line 1271
111. lemma OAI.KServer.RankOrder.countRank_expected line 1281
112. lemma OAI.KServer.RankOrder.convex_count_superadditivity line 1302
113. def OAI.KServer.CompatibleBounds.L line 1368

     Source documentation

     The two actual lower-bound sums on a conditional count distribution.

     def L {Ω : Type*} [Fintype Ω] (k : ℕ) (w : Ω → ℝ) (N : Ω → ℕ) (z : ℝ) : ℝ :=
     …

114. def OAI.KServer.CompatibleBounds.M line 1370
115. theorem OAI.KServer.CompatibleBounds.compatible_bounds line 1374

     Source documentation

     Lemma superadditivity, with arbitrary dependence and empty child sets.

     theorem compatible_bounds {Ω I : Type*} [Fintype Ω] [Fintype I]
         (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) (hws : ∑ ω, w ω = 1)
         {k : ℕ} (N : Ω → I → ℕ) (hN : ∀ ω, ∑ i, N ω i ≤ k)
         {z : ℝ} (hz : z ∈ Set.Icc 0 (1 / 100 : ℝ)) :
         (∑ i, L k w (fun ω => N ω i) z) ≤ L k w (fun ω => ∑ i, N ω i) z ∧
         (∑ i, M k w (fun ω => N ω i)) ≤ M k w (fun ω => ∑ i, N ω i) ∧
         M k w (fun ω => ∑ i, N ω i) ≤ ∑ ω, w ω * (∑ i, N ω i) := by
     …

     Mentions: OAI.KServer.CompatibleBounds.L, OAI.KServer.CompatibleBounds.M

116. lemma OAI.KServer.CompatibleBounds.sizeRank_antitone line 1390
117. lemma OAI.KServer.CompatibleBounds.sizeRank_at_cutoff line 1395
118. lemma OAI.KServer.CompatibleBounds.sizeRank_below_cutoff line 1397
119. lemma OAI.KServer.CompatibleBounds.rank_size_domination line 1401
120. lemma OAI.KServer.CompatibleBounds.core_decomposition line 1412

     Source documentation

     Exact core/flex decomposition for one child's ranks; indexing zero-based changes no values because countRank a is the source rank a+1.

     lemma core_decomposition {k : ℕ} (p : Fin k → ℝ) (K : Finset (Fin k)) (z : ℝ)
         (hK : ∀ a ∈ K, p a ≤ pstar) :
         (∑ a, rank z (p a)) = K.card - (3 + z) * (∑ a ∈ K, p a) +
           ∑ a ∈ univ \ K, rank z (p a) := by
     …

121. lemma OAI.KServer.CompatibleBounds.core_flex_domination line 1427
122. lemma OAI.KServer.CompatibleBounds.flex_parameter_slack line 1444