OAI/Combinatorics/KServer/Ranks.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KServer.RankTracking.avg line 12
2. lemma OAI.KServer.RankTracking.avg_add line 14
3. lemma OAI.KServer.RankTracking.avg_sub line 16
4. lemma OAI.KServer.RankTracking.avg_mul line 18
5. lemma OAI.KServer.RankTracking.avg_sum line 20
6. lemma OAI.KServer.RankTracking.avg_mono line 23
7. lemma OAI.KServer.RankTracking.avg_const line 25
8. def OAI.KServer.RankTracking.Adapted line 29

   Source documentation

   Functions known from the observed finite history label.

   def Adapted (H : Ω → ℕ) (f : Ω → ℝ) : Prop := ∀ ω ω', H ω=H ω' → f ω=f ω'

9. structure OAI.KServer.RankTracking.FilteredRanks line 33

   Source documentation

   Increasing history information, adapted ranks, and the literal finite conditional tower relation for old counts under the new observation.

   structure FilteredRanks (w : Ω → ℝ) where
   …

10. lemma OAI.KServer.RankTracking.fiber_weighted_zero line 44
11. lemma OAI.KServer.RankTracking.filtering_affine line 68
12. def OAI.KServer.PosteriorRanks.fiber line 84
13. def OAI.KServer.PosteriorRanks.mass line 85
14. def OAI.KServer.PosteriorRanks.numerator line 86
15. def OAI.KServer.PosteriorRanks.posterior line 89
16. lemma OAI.KServer.PosteriorRanks.mass_nonneg line 92
17. lemma OAI.KServer.PosteriorRanks.numerator_zero line 95
18. lemma OAI.KServer.PosteriorRanks.posterior_adapted line 101
19. lemma OAI.KServer.PosteriorRanks.posterior_range line 106
20. lemma OAI.KServer.PosteriorRanks.fiber_posterior line 121
21. lemma OAI.KServer.PosteriorRanks.fiber_difference line 137
22. lemma OAI.KServer.PosteriorRanks.weighted_posterior line 142
23. lemma OAI.KServer.PosteriorRanks.posterior_avg line 150
24. lemma OAI.KServer.PosteriorRanks.filtered_fiber line 154
25. def OAI.KServer.PosteriorRanks.rank line 171

    Source documentation

    The true post-filtering, post-drift ranks and the filtered old ranks on an arbitrary finite experiment with increasing observations.

    def rank (N : Ω → ℕ) (a : ℕ) (ω : Ω) : ℝ := if N ω ≤ a then 1 else 0
    …

26. lemma OAI.KServer.PosteriorRanks.rank_range line 173
27. def OAI.KServer.PosteriorRanks.rankProcess line 176
28. lemma OAI.KServer.PosteriorRanks.posterior_sub line 191
29. lemma OAI.KServer.PosteriorRanks.abs_posterior_le line 195
30. theorem OAI.KServer.PosteriorRanks.posterior_drift line 208

    Source documentation

    Conditional averaging cannot increase the drift, even at zero-mass histories, where the quotient convention simply chooses zero.

    theorem posterior_drift {w : Ω → ℝ} (hw : ∀ ω, 0 ≤ w ω)
        (H : Ω → ℕ) (f g : Ω → ℝ) :
        avg w (fun ω => |posterior w H f ω-posterior w H g ω|) ≤
          avg w (fun ω => |f ω-g ω|) := by
    …

    Mentions: OAI.KServer.PosteriorRanks.posterior

31. lemma OAI.KServer.PosteriorRanks.sum_below line 217
32. lemma OAI.KServer.PosteriorRanks.sum_above line 227
33. lemma OAI.KServer.PosteriorRanks.indicator_count_distance line 239
34. theorem OAI.KServer.PosteriorRanks.rank_drift_count line 257

    Source documentation

    The exact §03 all-rank drift budget, derived from the finite hidden count process rather than assumed as an interface.

    theorem rank_drift_count {w : Ω → ℝ} (hw : ∀ ω, 0 ≤ w ω)
        (H : Ω → ℕ) {k : ℕ} (N M : Ω → ℕ) (hN : ∀ ω, N ω ≤ k) (hM : ∀ ω, M ω ≤ k) :
        (∑ a : Fin k, avg w (fun ω => |posterior w H (rank N a.val) ω-
          posterior w H (rank M a.val) ω|)) ≤ avg w (fun ω => |(N ω:ℝ)-M ω|) := by
    …

    Mentions: OAI.KServer.PosteriorRanks.posterior, OAI.KServer.PosteriorRanks.rank

35. theorem OAI.KServer.PosteriorRanks.rankProcess_drift line 272

    Source documentation

    The instantiated process defined above obeys the source estimate with actual one-step hidden-count motion on its right-hand side.

    theorem rankProcess_drift {w : Ω → ℝ} (hw : ∀ ω, 0 ≤ w ω)
        (H : ℕ → Ω → ℕ) (hr : ∀ t ω z, H (t+1) ω=H (t+1) z → H t ω=H t z)
        {k : ℕ} (N : ℕ → Ω → ℕ) (hN : ∀ t ω, N t ω ≤ k) (t : ℕ) :
        (∑ a : Fin k, avg w (fun ω => |(rankProcess hw H hr N a.val).p (t+1) ω-
          (rankProcess hw H hr N a.val).before (t+1) ω|)) ≤
          avg w (fun ω => |(N (t+1) ω:ℝ)-N t ω|) := by
    …

    Mentions: OAI.KServer.PosteriorRanks.rankProcess

36. lemma OAI.KServer.PosteriorRanks.mass_pos_of_weight line 292
37. lemma OAI.KServer.PosteriorRanks.posterior_nonneg line 297
38. lemma OAI.KServer.PosteriorRanks.posterior_sum line 301
39. lemma OAI.KServer.PosteriorRanks.posterior_fiber_const line 307
40. lemma OAI.KServer.PosteriorRanks.posterior_mono_fiber line 318
41. lemma OAI.KServer.PosteriorRanks.posterior_add line 326
42. lemma OAI.KServer.PosteriorRanks.posterior_mul line 330