OAI/Combinatorics/KServer/Hierarchy.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Conditional ranks of literal complete-prefix cells, connected to the allocation's filtered process and compatible lower envelopes. No local allocation or competitiveness assertion is an input.

  1. def OAI.KServer.HierarchicalRanks.family line 22
  2. def OAI.KServer.HierarchicalRanks.lower line 25
  3. def OAI.KServer.HierarchicalRanks.size line 28
  4. lemma OAI.KServer.HierarchicalRanks.family_value line 32
  5. lemma OAI.KServer.HierarchicalRanks.lower_eq line 39
  6. lemma OAI.KServer.HierarchicalRanks.size_eq line 45
  7. lemma OAI.KServer.HierarchicalRanks.lower_superadditive line 50
  8. lemma OAI.KServer.HierarchicalRanks.size_superadditive line 56
  9. lemma OAI.KServer.HierarchicalRanks.family_root line 63
  10. lemma OAI.KServer.HierarchicalRanks.lower_root line 74
  11. lemma OAI.KServer.HierarchicalRanks.size_root line 80
  12. lemma OAI.KServer.HierarchicalRanks.lower_nonneg line 86
  13. lemma OAI.KServer.HierarchicalRanks.lower_size line 91
  14. lemma OAI.KServer.HierarchicalRanks.size_bound line 99
  15. lemma OAI.KServer.HierarchicalRanks.first_rank_zero line 112

    Source documentation

    The first reward rank is exactly zero if each possible hidden placement has a member in the current observed cell. This is a fiber, not an independence assertion and does not condition on any rounding outcomes.

    lemma first_rank_zero {k : ℕ} (hk : 0<k) (q : ℕ → Ω → Fin k → Y)
    (word : Fin d → A) (t : ℕ) (ω : Ω)
    (hs : ∀ ρ,H t ρ=H t ω → ∃ l,hit (maps t ρ) word (q t ρ l)) :
    (family hw H hr maps q word ⟨0,hk⟩).p t ω=0 := by
…

    Mentions: OAI.KServer.HierarchicalRanks.family

  16. lemma OAI.KServer.HierarchicalRanks.served_lower line 128
  17. def OAI.KServer.HierarchicalQuota.children line 157
  18. def OAI.KServer.HierarchicalQuota.parent line 159
  19. def OAI.KServer.HierarchicalQuota.quota line 162
  20. lemma OAI.KServer.HierarchicalQuota.quota_snoc line 168
  21. lemma OAI.KServer.HierarchicalQuota.sizes line 174
  22. lemma OAI.KServer.HierarchicalQuota.size_bound line 179
  23. lemma OAI.KServer.HierarchicalQuota.parent_budget line 183
  24. lemma OAI.KServer.HierarchicalQuota.quota_bounds line 202
  25. lemma OAI.KServer.HierarchicalQuota.children_budget line 229
  26. lemma OAI.KServer.HierarchicalQuota.quota_nonneg line 236
  27. lemma OAI.KServer.HierarchicalQuota.served line 241