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.
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.5998004The 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.
Assumption that enters: that discovery is proportional to presence times the true rate.
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.5With 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.335Assumption that enters: the noise boxes.
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] 2500A 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):
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] -1Under 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.66667One 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.
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):
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 FALSEEnsign 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.