OAI/Combinatorics/UniformKServer/RadiusTail.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformKServer.RadiusTail.clipped line 10
  2. def OAI.UniformKServer.RadiusTail.tail line 14

    Source documentation

    Survival function of the manuscript's truncated exponential radius, normalized by r. It includes support endpoints with their exact values.

    def tail (lam a : ℝ) : ℝ :=
…
  3. theorem OAI.UniformKServer.RadiusTail.clipped_bounds line 16
  4. theorem OAI.UniformKServer.RadiusTail.clipped_mono line 19
  5. theorem OAI.UniformKServer.RadiusTail.clipped_difference line 23
  6. theorem OAI.UniformKServer.RadiusTail.denominator_pos line 39
  7. theorem OAI.UniformKServer.RadiusTail.tail_bounds line 43
  8. theorem OAI.UniformKServer.RadiusTail.tail_antitone line 53
  9. theorem OAI.UniformKServer.RadiusTail.tail_eq_one line 62
  10. theorem OAI.UniformKServer.RadiusTail.tail_eq_zero line 70
  11. theorem OAI.UniformKServer.RadiusTail.tail_offset line 76
  12. theorem OAI.UniformKServer.RadiusTail.tail_difference line 88

    Source documentation

    Exact separation-tail estimate, including intervals crossing either end of the support. The two actual distances are later substituted for a,b.

    theorem tail_difference (lam a b : ℝ) (hlam : 0 < lam) (hab : a ≤ b) :
    tail lam a-tail lam b ≤ lam*(b-a)*(tail lam a+1/(Real.exp lam-1))
 := by
…

    Mentions: OAI.UniformKServer.RadiusTail.tail