Eight hard problems in criminology, with proofs behind the functions

Every function on this page rests on a theorem checked in Lean 4 with Mathlib. The Lean sources are in research/lean/ of the source repository (they are not part of the installed package); Audit.lean prints the axioms each theorem uses, which are the three standard ones (propext, Classical.choice, Quot.sound), and no project file contains sorry. The rule throughout: Lean certifies the implication, never the antecedent. Each section says where the empirical assumption enters.

P4. Predictive-policing feedback loops run away, and slowly

Two regions, true rates 0.3 and 0.2, patrol allocated in proportion to discovered crime. The mean-field recursion converges to sending the whole patrol to the higher-rate region, whatever the ratio of the rates (Research.P4.naiveShare_tendsto_one):

mf <- morie_feedback_loop_meanfield(0.3, 0.2, 10, 10, n_steps = 20000)
tail(mf$share_a, 1)
#> [1] 0.8883716
attr(mf, "limit")$theorem
#> [1] "Research.P4.naiveShare_tendsto_one"

The corrected update of Ensign et al. (discount each discovery by the presence that produced it) converges to the true-rate proportion instead (Research.P4.corrected_share_tendsto):

cf <- morie_feedback_loop_meanfield(0.3, 0.2, 10, 10, n_steps = 20000, update = "corrected")
tail(cf$share_a, 1)
#> [1] 0.5998004

The limit is not the whole story. The proved rate bound (Research.P4.naiveShare_rate_bound) shows the share can move at most like a harmonic sum: a 5 percent rate gap from a 1/99 start cannot move the allocation by more than about a tenth in two million steps.

morie_feedback_loop_bound(0.21, 0.20, 1, 99, n_steps = 2e6)$bound
#> [1] 0.1036912

Assumption that enters: that discovery is proportional to presence times the true rate.

P5. What a risk score’s fairness can and cannot be

Chouldechova’s identity ties the false positive rate to base rate, PPV and FNR (Research.P5.Table.chouldechova); two groups with equal PPV and FNR but different base rates cannot share an FPR (Research.P5.impossibility):

morie_fairness_implied_fpr(p = 0.30, ppv = 0.6, fnr = 0.25)
#> [1] 0.2142857
morie_fairness_implied_fpr(p = 0.50, ppv = 0.6, fnr = 0.25)
#> [1] 0.5

With rearrest as a noisy proxy for reoffending, the true base rate is identified only up to an interval, and both ends are attainable (Research.P5.true_base_rate_bounds); whether two groups can even be ordered depends on whether the intervals overlap (Research.P5.compare_decided, compare_undecided):

morie_fairness_base_rate_bounds(c(0.35, 0.55), alpha_max = 0.05, beta_max = 0.20)
#>   p_obs     lower  upper     width
#> 1  0.35 0.3157895 0.4375 0.1217105
#> 2  0.55 0.5263158 0.6875 0.1611842
morie_fairness_compare_groups(0.35, 0.55, alpha_max = 0.05, beta_max = 0.40)[c("order", "breakdown_beta_max")]
#> $order
#> [1] "undecided"
#> 
#> $breakdown_beta_max
#> [1] 0.335

Assumption that enters: the noise boxes.

P1. The dark figure as an interval, not a point

Two lists of the same events identify the true count only under independence; with a dependence factor in a box the count is an interval with attainable ends (Research.P1.TwoSource.petersen_bounds):

morie_dark_figure_two_source(400, 250, 80)
#> $point
#> [1] 1250
#> 
#> $lower
#> [1] 1250
#> 
#> $upper
#> [1] 1250
#> 
#> $kappa
#> [1] 1
#> 
#> $theorem
#> [1] "Research.P1.TwoSource.lincoln_petersen"
morie_dark_figure_two_source(400, 250, 80, kappa = 2)[c("lower", "upper")]
#> $lower
#> [1] 625
#> 
#> $upper
#> [1] 2500

A recorded rate and a survey rate together bound the true rate and the dark figure (Research.P1.dark_figure_bounds), and the breakdown value says how much under-reporting would overturn a conclusion (Research.P1.conclusion_holds_below_breakdown):

morie_dark_figure_bounds(v_obs = 0.06, r = 0.02, alpha_max = 0.01, beta_max = 0.30)
#>   v_obs    r    v_lower    v_upper dark_lower dark_upper ratio_upper
#> 1  0.06 0.02 0.05050505 0.08571429 0.03050505 0.06571429    4.285714
morie_dark_figure_breakdown(0.06, threshold = 0.10)$breakdown_beta_max
#> [1] 0.4

P3. Hot-spot effects when places affect their neighbours

An exposure mapping on a place network (treated / untreated with a treated neighbour / isolated), the stratified exposure adjustment (Research.P3.Model.exposure_adjustment), the direct/spillover split, and the bias of pooling exposures 0 and 1 as “control”:

set.seed(1)
n <- 400
stratum <- rep(c("core", "edge"), each = n / 2)
exposure <- sample(0:2, n, replace = TRUE)
y <- 5 - 1.0 * (exposure == 2) - 0.4 * (exposure == 1) + (stratum == "core")
morie_spillover_effects(y, exposure, stratum)[c("spillover", "direct", "total")]
#> $spillover
#> [1] -0.4
#> 
#> $direct
#> [1] -0.6
#> 
#> $total
#> [1] -1

Under a randomised deployment the Horvitz–Thompson estimator needs no ignorability at all (Research.P3.Design.ht_unbiased):

edges <- cbind(1:7, 2:8)
pr <- morie_spillover_exposure_probs(n = 8, edges, n_treated = 3)
trt <- c(2, 5, 7)
e <- morie_spillover_exposure(seq_len(8) %in% trt, edges)$exposure
morie_spillover_ht(y = 10 + seq_len(8) - 3 * (e == 2) - (e == 1), e, pr)$total_effect
#> [1] 11.66667

One draw of the design gives a noisy estimate of the true total effect (-3 in this outcome model). Unbiasedness is a statement about the average over the design, which here can be enumerated exactly: all choose(8, 3) = 56 ways of treating three of the eight places.

draws <- combn(8, 3)
ht <- apply(draws, 2, function(trt) {
  e <- morie_spillover_exposure(seq_len(8) %in% trt, edges)$exposure
  morie_spillover_ht(y = 10 + seq_len(8) - 3 * (e == 2) - (e == 1), e, pr)$total_effect
})
mean(ht)
#> [1] -3
range(ht)
#> [1] -30.9  12.0

P7. How much of the “law of crime concentration” is crime-free places?

The Gini of all places splits exactly into the zero share and the Gini among places with any crime (Research.P7.gini_zero_decomposition), and a uniform Poisson process produces a zero share of exactly exp(-mu) (Research.P7.poisson_zero_prob):

set.seed(1)
x <- rpois(2000, 0.4)
unlist(morie_concentration_decompose(x)[c("zero_share", "null_zero_share", "gini_all", "gini_positive")])
#>      zero_share null_zero_share        gini_all   gini_positive 
#>       0.6655000       0.6636503       0.7161524       0.1514273

P2, P6, P8 in one breath

Disparity with exposure known only within a factor (Research.P2.disparity_bounds), the aggregate age–crime curve of a mixture and its identical one-type twin (Research.P6.aggregate_not_identifying), and which deterrence partial effects a design can identify (Research.P8.constant_dimension_not_identified):

morie_disparity_exposure_bounds(y = c(A = 300, B = 100), m = c(A = 1000, B = 1000), gamma = 1.5, reference = "B")[, c("group", "ratio_lower", "ratio_upper", "direction_identified")]
#>   group ratio_lower ratio_upper direction_identified
#> 1     A   1.3333333        6.75                 TRUE
#> 2     B   0.4444444        2.25                FALSE
ages <- 10:60
early <- dgamma(ages - 9, shape = 3, rate = 0.5) * 40
late <- dgamma(ages - 9, shape = 8, rate = 0.35) * 40
two <- morie_age_crime_aggregate(c(0.5, 0.5), cbind(early, late), ages)
head(attr(two, "equivalent_single_type"), 3)
#> [1] 0.758164 1.839454 2.510898
morie_deterrence_design_check(p = c(0.1, 0.3, 0.5), s = c(2, 2, 2), c = c(30, 30, 30))$identified
#> certainty  severity  celerity 
#>      TRUE     FALSE     FALSE

References

Ensign D, Friedler SA, Neville S, Scheidegger C, Venkatasubramanian S (2018). Runaway feedback loops in predictive policing. PMLR 81, 160–171.

Chouldechova A (2017). Fair prediction with disparate impact. Big Data 5(2), 153–163.

Bird SM, King R (2018). Multiple systems estimation to inform public policy. Annual Review of Statistics and Its Application 5, 95–118.

Weisburd D (2015). The law of crime concentration and the criminology of place. Criminology 53(2), 133–157.

Nagin DS (2013). Deterrence in the twenty-first century. Crime and Justice 42, 199–263.