OAI/Combinatorics/UniformKServer/ConditionalRank.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Source §02/§03: the rank-tracker input is constructed from a hidden count, not obtained by assuming a martingale. Summed posterior rank drift is bounded by the actual count drift, with coefficient one.

  1. def OAI.UniformKServer.ConditionalRank.indicator line 17
  2. theorem OAI.UniformKServer.ConditionalRank.indicator_range line 19
  3. theorem OAI.UniformKServer.ConditionalRank.indicator_sum line 23
  4. theorem OAI.UniformKServer.ConditionalRank.indicator_distance_ordered line 45
  5. theorem OAI.UniformKServer.ConditionalRank.indicator_distance line 56
  6. def OAI.UniformKServer.ConditionalRank.input line 65

    Source documentation

    Actual finite posterior input for each child rank.

    def input (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) (htotal : ∑ ω, w ω=1)
    (F : ℕ → Setoid Ω) (hF : ∀ t ω v, (F (t+1)).r ω v → (F t).r ω v)
    (N : ℕ → Ω → ℕ) (j : ℕ) : RankTracking.Input Ω where
…

    Mentions: OAI.UniformKServer.RankTracking.Input

  7. theorem OAI.UniformKServer.ConditionalRank.total_drift line 85