OAI/Combinatorics/UniformKServer/LevelSeparation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniformKServer.LevelMap.Data.indicator_ne line 18
2. def OAI.UniformKServer.LevelMap.Data.component line 21
3. theorem OAI.UniformKServer.LevelMap.Data.first_components line 25
4. theorem OAI.UniformKServer.LevelMap.Data.priority_bound line 31
5. theorem OAI.UniformKServer.LevelMap.Data.tier_coverage line 47
6. theorem OAI.UniformKServer.LevelMap.Data.heavy_separation line 53
7. theorem OAI.UniformKServer.LevelMap.Data.tier_separation line 73
8. theorem OAI.UniformKServer.LevelMap.Data.expect_list_sum line 102
9. theorem OAI.UniformKServer.LevelMap.Data.prefix_separation line 110

   Source documentation

   Only the prefix through a qualifying tier is charged. In particular this is not the number of levels times a worst-case tier coefficient.

   theorem prefix_separation (D : Data X N H) (is js : List (Fin H)) (n : Fin N)
       (hq : ∃ i∈is, D.qualify i n) (p : X) (hp : dist (D.center n) p<D.r/4) :
       D.law.expect (fun ω => indicator (D.key (is++js) ω (n.val+1) (D.center n))
         (D.key (is++js) ω (n.val+1) p))≤dist (D.center n) p/D.r+
           (is.map (fun i => 2*Real.log (1+(D.K i:ℝ)^2)*dist (D.center n) p/D.r)).sum := by
   …

   Mentions: OAI.UniformKServer.LevelMap.Data