Independent depth and full ladder bound

Conditioning on the full stable ladder height leaves an independent infimum depth. Its exponential tail integrates exactly by the ladder-height Laplace transform.

theorem BGW.StableTrees.measure_supLadderHeight_le_independent_depth {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (r v : NNReal) {q : ℝ} (hq : 0 ≤ q) : ((↑(stableLocalLaw θ)).prod ↑(stableLocalLaw θ)) {p : Skorokhod.DLoc × Skorokhod.DLoc | supLadderHeight θ v p.1 ≤ -runningInfLoc p.2 r} ≤ ENNReal.ofReal (Real.exp (q * ↑r - ↑v * (q ^ (1 / θ)) ^ (θ - 1)))

An independent fresh infimum dominates a full ladder height with an exponential bound.