Research proof index

]]σ,τ]] is an elementary predictable set for bounded stopping times on ℕ (blueprint lem:elementaryPredictableSet_stochasticInterval). With τ ≤ n, ]]σ,τ]] = ⋃_{i < n} (i, i+1] × {σ ≤ i < τ} is a finite disjoint union of predictable rectangles, which is exactly the data of an ElementaryPredictableSet.

Along a strictly decreasing sequence u → x from the right, the regularized values r (u k) tend to the right limit of h at x along T' ⊇ T.

Along a strictly increasing sequence u → x from the left, the regularized values r (u k) tend to the left limit of h at x along T' ⊇ T.

The right-limit regularization inherits left limits of h along T.

Version of boolBiasAdvantage_eq_boolDistAdvantage_uniformBool_branch with a shared sampled prefix before the real/random branch is chosen.

If a distribution has an element with probability 1, the distribution has a constant.