OAI/Combinatorics/KServer/Trees.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

A literal finite complete-prefix tree, numbered parent-before-child. The unused words are retained, as required for an unconditioned finite key tape.

  1. abbrev OAI.KServer.PrefixTree.Vertex line 14
  2. def OAI.KServer.PrefixTree.root line 16
  3. instance OAI.KServer.PrefixTree.(instance at line 17) line 17
  4. def OAI.KServer.PrefixTree.code line 19
  5. lemma OAI.KServer.PrefixTree.code_injective line 22
  6. instance OAI.KServer.PrefixTree.(instance at line 32) line 32
  7. lemma OAI.KServer.PrefixTree.root_le line 34
  8. instance OAI.KServer.PrefixTree.(instance at line 46) line 46
  9. def OAI.KServer.PrefixTree.numbering line 48
  10. lemma OAI.KServer.PrefixTree.numbering_zero line 51
  11. def OAI.KServer.PrefixTree.parent line 58
  12. lemma OAI.KServer.PrefixTree.parent_root line 63
  13. lemma OAI.KServer.PrefixTree.parent_lt line 65
  14. def OAI.KServer.PrefixTree.tree line 81
  15. def OAI.KServer.HierarchyCounts.hit line 110
  16. def OAI.KServer.HierarchyCounts.count line 113
  17. lemma OAI.KServer.HierarchyCounts.count_le line 117
  18. lemma OAI.KServer.HierarchyCounts.hit_zero line 122
  19. lemma OAI.KServer.HierarchyCounts.count_zero line 126
  20. lemma OAI.KServer.HierarchyCounts.hit_snoc line 130
  21. lemma OAI.KServer.HierarchyCounts.count_sum line 141
  22. lemma OAI.KServer.HierarchyCounts.positive_mass line 153
  23. def OAI.KServer.HierarchyCounts.conditional line 158

    Source documentation

    The actual conditional distribution on the true prefix fiber.

    def conditional (w : Ω → ℝ) (H : Ω → ℕ) (ω ρ : Ω) : ℝ :=
…
  24. lemma OAI.KServer.HierarchyCounts.conditional_nonneg line 161
  25. lemma OAI.KServer.HierarchyCounts.conditional_sum line 168
  26. lemma OAI.KServer.HierarchyCounts.conditional_rank line 174
  27. theorem OAI.KServer.HierarchyCounts.compatible line 183

    Source documentation

    The actual posterior lower bounds simultaneously satisfy both source superadditivities, even though the labeled counts are arbitrarily dependent.

    theorem compatible (w : Ω → ℝ) (hw : ∀ ω,0≤w ω) (H : Ω → ℕ) (ω : Ω)
    (hω : 0<w ω) (maps : Ω → ℕ → Y → A) (word : Fin d → A) (q : Ω → Fin k → Y)
    {z : ℝ} (hz : z∈Set.Icc 0 (1/100:ℝ)) :
    (∑ a : A, CompatibleBounds.L k (conditional w H ω)
      (fun ρ=>count (maps ρ) (Fin.snoc word a) (q ρ)) z) ≤
      CompatibleBounds.L k (conditional w H ω) (fun ρ=>count (maps ρ) word (q ρ)) z ∧
    (∑ a : A, CompatibleBounds.M k (conditional w H ω)
      (fun ρ=>count (maps ρ) (Fin.snoc word a) (q ρ))) ≤
      CompatibleBounds.M k (conditional w H ω) (fun ρ=>count (maps ρ) word (q ρ)) ∧
    CompatibleBounds.M k (conditional w H ω) (fun ρ=>count (maps ρ) word (q ρ)) ≤
      ∑ ρ,conditional w H ω ρ*count (maps ρ) word (q ρ) := by
…

    Mentions: OAI.KServer.CompatibleBounds.L, OAI.KServer.HierarchyCounts.conditional, OAI.KServer.HierarchyCounts.count, OAI.KServer.CompatibleBounds.M

  28. lemma OAI.KServer.HierarchyCounts.conditional_adapted line 200
  29. lemma OAI.KServer.HierarchyCounts.rank_adapted line 205