[STATEMENT]
lemma escape_rate_pos: "0 < escape_rate x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < escape_rate x
[PROOF STEP]
using positive_weight
[PROOF STATE]
proof (prove)
using this:
0 < \<integral>\<^sup>+ x. ennreal (R ?x x) \<partial>count_space UNIV

goal (1 subgoal):
 1. 0 < escape_rate x
[PROOF STEP]
unfolding ennreal_escape_rate[symmetric]
[PROOF STATE]
proof (prove)
using this:
0 < ennreal (escape_rate ?x)

goal (1 subgoal):
 1. 0 < escape_rate x
[PROOF STEP]
by simp