OAI/Combinatorics/UniformKServer/RankTracking.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.RankTracking.average line 17
2. def OAI.UniformKServer.RankTracking.measurableAt line 19
3. structure OAI.UniformKServer.RankTracking.Input line 22
4. def OAI.UniformKServer.RankTracking.reference line 36
5. def OAI.UniformKServer.RankTracking.estimate line 43
6. def OAI.UniformKServer.RankTracking.potential line 46
7. def OAI.UniformKServer.RankTracking.driftBudget line 48
8. theorem OAI.UniformKServer.RankTracking.average_add line 53
9. theorem OAI.UniformKServer.RankTracking.average_mono line 57
10. theorem OAI.UniformKServer.RankTracking.potential_range line 61
11. theorem OAI.UniformKServer.RankTracking.reset_identity line 74
12. theorem OAI.UniformKServer.RankTracking.drift_slope line 79
13. theorem OAI.UniformKServer.RankTracking.credit_step line 88
14. theorem OAI.UniformKServer.RankTracking.reset_credit line 118
15. theorem OAI.UniformKServer.RankTracking.reference_range line 147
16. theorem OAI.UniformKServer.RankTracking.reference_measurable line 159
17. theorem OAI.UniformKServer.RankTracking.reference_step line 170
18. theorem OAI.UniformKServer.RankTracking.square_root_failure_ordered line 176
19. theorem OAI.UniformKServer.RankTracking.square_root_failure line 204
20. theorem OAI.UniformKServer.RankTracking.estimate_spec line 214
21. theorem OAI.UniformKServer.RankTracking.estimate_step line 237
22. theorem OAI.UniformKServer.RankTracking.average_mul line 260
23. theorem OAI.UniformKServer.RankTracking.relative_tracker line 269

    Source documentation

    Source Lemma lem:rank-tracking, with the absolute constant made explicit as five times the common squared Lipschitz constant of the square root.

    theorem relative_tracker (I : Input Ω) (f : ℝ → ℝ) (ξ K : ℝ)
        (hξ : 0 < ξ) (hξ' : ξ < 1/2) (hK : 0 ≤ K)
        (hf : ∀ p ∈ Set.Icc (0 : ℝ) 1, 0 ≤ f p)
        (hLip : ∀ p ∈ Set.Icc (0 : ℝ) 1, ∀ q ∈ Set.Icc (0 : ℝ) 1,
          |Real.sqrt (f p) - Real.sqrt (f q)| ≤ K * |p - q|) :
        (∀ t ω, (1+ξ)⁻¹ * f (I.posterior t ω) ≤ estimate I f ξ t ω ∧
          estimate I f ξ t ω ≤ (1+ξ) * f (I.posterior t ω)) ∧
        (∀ H, (∑ t ∈ Finset.range H, average I.weight
          (fun ω => |estimate I f ξ (t+1) ω - estimate I f ξ t ω|)) ≤
          (5*K^2/ξ) * (driftBudget I H + 1)) := by
    …

    Mentions: OAI.UniformKServer.RankTracking.Input, OAI.UniformKServer.RankTracking.estimate, OAI.UniformKServer.RankTracking.average, OAI.UniformKServer.RankTracking.driftBudget

24. def OAI.UniformKServer.RankTracking.absoluteReference line 299

    Source documentation

    The held posterior used for the source's fixed-threshold core flags.

    noncomputable def absoluteReference (I : Input Ω) (δ : ℝ) : ℕ → Ω → ℝ
      | 0, ω => I.posterior 0 ω
      | t + 1, ω =>
        if |I.posterior (t + 1) ω - absoluteReference I δ t ω| ≤ δ
        then absoluteReference I δ t ω else I.posterior (t + 1) ω

    Mentions: OAI.UniformKServer.RankTracking.Input

25. def OAI.UniformKServer.RankTracking.refreshCount line 305
26. theorem OAI.UniformKServer.RankTracking.absoluteReference_range line 310
27. theorem OAI.UniformKServer.RankTracking.absoluteReference_measurable line 322
28. theorem OAI.UniformKServer.RankTracking.absoluteReference_step line 333
29. theorem OAI.UniformKServer.RankTracking.absoluteReference_spec line 339
30. theorem OAI.UniformKServer.RankTracking.absolute_refresh_charge line 349
31. theorem OAI.UniformKServer.RankTracking.absolute_tracker line 366

    Source documentation

    The fixed absolute threshold part of source Lemma lem:rank-tracking.

    theorem absolute_tracker (I : Input Ω) (δ : ℝ) (hδ : 0 < δ) :
        (∀ t ω, |I.posterior t ω - absoluteReference I δ t ω| ≤ δ) ∧
        (∀ H, refreshCount I δ H ≤ (δ^2)⁻¹ * (driftBudget I H + 1)) := by
    …

    Mentions: OAI.UniformKServer.RankTracking.Input, OAI.UniformKServer.RankTracking.absoluteReference, OAI.UniformKServer.RankTracking.refreshCount, OAI.UniformKServer.RankTracking.driftBudget