OAI/Combinatorics/UniformKServer/ConditionalRanks.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The source rank and size inequalities for the actual finite conditional law, with normalization proved on every positive-ConditionalLaw.mass history. Null histories are not silently assigned a normalized law.

  1. def OAI.UniformKServer.ConditionalRanks.rankProbability line 19
  2. theorem OAI.UniformKServer.ConditionalRanks.normalized_kernel line 22
  3. def OAI.UniformKServer.ConditionalRanks.countInput line 26
  4. theorem OAI.UniformKServer.ConditionalRanks.rankProbability_eq line 35
  5. theorem OAI.UniformKServer.ConditionalRanks.conditional_convex_superadditivity line 38
  6. theorem OAI.UniformKServer.ConditionalRanks.size_superadditivity line 49
  7. theorem OAI.UniformKServer.ConditionalRanks.rank_superadditivity line 57
  8. theorem OAI.UniformKServer.ConditionalRanks.sum_complements line 66
  9. theorem OAI.UniformKServer.ConditionalRanks.size_le_mean line 86
  10. theorem OAI.UniformKServer.ConditionalRanks.root_probability_zero line 97
  11. theorem OAI.UniformKServer.ConditionalRanks.root_size_rank line 102
  12. theorem OAI.UniformKServer.ConditionalRanks.required_probability_zero line 109

    Source documentation

    The required first rank is zero on positive-weight atoms of the observed history; no assertion is inserted for impossible hidden configurations.

    theorem required_probability_zero (w : Ω → ℝ) (F : Setoid Ω) (ω : Ω) (N : Ω → ℕ)
    (hN : ∀ v, F.r ω v → w v ≠ 0 → 1 ≤ N v) : rankProbability w F N ω 0 = 0 := by
…

    Mentions: OAI.UniformKServer.ConditionalRanks.rankProbability

  13. theorem OAI.UniformKServer.ConditionalRanks.required_rank_lower line 121