Proved limit of the two-region feedback loop

Returns the long-run share of patrol sent to region A under the mean-field recursion, with the name of the Lean theorem that proves it. With rho > 0 under the naive update the limit is not proved, but the share is proved never to exceed the cap \(\max(x_0, \lambda_A/(\lambda_A + \rho\lambda_B))\) (Research.P4.rho_cap); share_a is then NA and cap carries the bound.

Usage

morie_feedback_loop_limit(
  lam_a,
  lam_b,
  c_a0,
  c_b0,
  update = c("naive", "corrected"),
  rho = 0
)

Arguments

lam_a, lam_b

True crime rates (per patrol visit) of regions A and B; positive.

c_a0, c_b0

Initial discovered-crime counts; positive.

update

"naive" (discovered counts fed back as they are) or "corrected" (each discovery discounted by the presence that produced it, so the increment is the true rate).

rho

Share of crimes that reach the record through public reports independent of patrol presence, in [0, 1]. With rho > 0 the naive share is proved never to exceed \(\max(x_0, \lambda_A/(\lambda_A + \rho\lambda_B))\) (Research.P4.rho_cap): reports cap the loop strictly below 1 but strictly above the true-rate proportion unless rho = 1.

Value

A list with share_a (the limit, or NA), theorem (the Lean name, or NA), note, and for rho > 0 also cap and cap_theorem.

Examples

morie_feedback_loop_limit(0.3, 0.2, 10, 10)                 # 1
#> $share_a
#> [1] 1
#> 
#> $theorem
#> [1] "Research.P4.naiveShare_tendsto_one"
#> 
#> $note
#> [1] "runaway: the higher-rate region absorbs the whole patrol"
#> 
morie_feedback_loop_limit(0.3, 0.2, 10, 10, "corrected")    # 0.6
#> $share_a
#> [1] 0.6
#> 
#> $theorem
#> [1] "Research.P4.corrected_share_tendsto"
#> 
#> $note
#> [1] "limit is the true-rate proportion, for every start"
#> 
morie_feedback_loop_limit(0.3, 0.3, 10, 10)                 # stays at 0.5
#> $share_a
#> [1] 0.5
#> 
#> $theorem
#> [1] "Research.P4.naive_step_drift"
#> 
#> $note
#> [1] "equal rates: the mean-field drift is zero and the share never moves; the stochastic urn instead converges to a random limit (Research.P4.Urn.polya_uniform, see morie_feedback_loop_urn_law)"
#> 
#> $stochastic_theorem
#> [1] "Research.P4.Urn.polya_no_concentration"
#> 
morie_feedback_loop_limit(0.3, 0.2, 10, 10, rho = 0.5)$cap # 0.3 / 0.4 = 0.75
#> [1] 0.75