Monotone likelihood ratio

DefinitionMonotone likelihood ratio#✓fully proved

The likelihood family L : ℕ → ℝ → ℝ (observation, parameter) has a monotone likelihood ratio on the parameter set S: L is nonnegative on S, and for observations n ≤ m and parameters θ ≤ θ' in S, L m θ * L n θ' ≤ L n θ * L m θ' (total positivity of order two). For positive likelihoods this is monotonicity of θ ↦ L m θ / L n θ. The nonnegativity is part of the predicate: without it the downstream posteriorTail would not be a posterior probability (a signed L can give posteriorTail > 1).

def HasMonotoneLikelihoodRatioOn (L : ℕ → ℝ → ℝ) (S : Set ℝ) : Prop :=
  (∀ n θ, θ ∈ S → 0 ≤ L n θ) ∧
    ∀ ⦃n m : ℕ⦄, n ≤ m → ∀ ⦃θ θ' : ℝ⦄, θ ∈ S → θ' ∈ S → θ ≤ θ' →
      L m θ * L n θ' ≤ L n θ * L m θ'

Used by 4

Used byBinomial family has monotone likelihood ratio · Poisson family with monotone mean has monotone likelihood ratio · The posterior is stochastically nondecreasing in the observation · Posterior stochastic ordering, cross-multiplied form

DefinitionAntitone likelihood ratio#✓fully proved

The likelihood family has an antitone likelihood ratio on S: L is nonnegative on S, and for n ≤ m and θ ≤ θ' in S, L n θ * L m θ' ≤ L m θ * L n θ'. For positive likelihoods this says θ ↦ L m θ / L n θ is nonincreasing (larger counts favor smaller parameters).

def HasAntitoneLikelihoodRatioOn (L : ℕ → ℝ → ℝ) (S : Set ℝ) : Prop :=
  (∀ n θ, θ ∈ S → 0 ≤ L n θ) ∧
    ∀ ⦃n m : ℕ⦄, n ≤ m → ∀ ⦃θ θ' : ℝ⦄, θ ∈ S → θ' ∈ S → θ ≤ θ' →
      L n θ * L m θ' ≤ L m θ * L n θ'

Used by 3

Used byPoisson family with antitone mean has antitone likelihood ratio · The posterior is stochastically nonincreasing in the observation · Posterior stochastic ordering for an antitone likelihood ratio, cross-multiplied form

TheoremPosterior stochastic ordering, cross-multiplied form#✓fully proved

Posterior stochastic ordering, cross-multiplied form (Milgrom 1981, Prop. 1). If the family L has a monotone likelihood ratio on a set S carrying the prior μ (μ Sᶜ = 0), and every L n is μ-integrable, then for n ≤ m and every threshold t, (∫_{θ > t} L n dμ) (∫ L m dμ) ≤ (∫_{θ > t} L m dμ) (∫ L n dμ).

theorem setIntegral_Ioi_mul_integral_le_of_hasMLR {μ : Measure ℝ}
    {L : ℕ → ℝ → ℝ} {S : Set ℝ} (hμS : μ Sᶜ = 0)
    (hL : HasMonotoneLikelihoodRatioOn L S) (hint : ∀ n, Integrable (L n) μ)
    {n m : ℕ} (hnm : n ≤ m) (t : ℝ) :
    (∫ θ in Ioi t, L n θ ∂μ) * ∫ θ, L m θ ∂μ ≤ (∫ θ in Ioi t, L m θ ∂μ) * ∫ θ, L n θ ∂μ

Uses 1 · Used by 1

Statement usesMonotone likelihood ratio

Used byThe posterior is stochastically nondecreasing in the observation

TheoremPosterior stochastic ordering for an antitone likelihood ratio, cross-multiplied form#✓fully proved

Under the hypotheses of setIntegral_Ioi_mul_integral_le_of_hasMLR with the reversed ratio condition, for n ≤ m: (∫_{θ > t} L m dμ) (∫ L n dμ) ≤ (∫_{θ > t} L n dμ) (∫ L m dμ).

theorem setIntegral_Ioi_mul_integral_le_of_hasAntitoneLR {μ : Measure ℝ}
    {L : ℕ → ℝ → ℝ} {S : Set ℝ} (hμS : μ Sᶜ = 0)
    (hL : HasAntitoneLikelihoodRatioOn L S) (hint : ∀ n, Integrable (L n) μ)
    {n m : ℕ} (hnm : n ≤ m) (t : ℝ) :
    (∫ θ in Ioi t, L m θ ∂μ) * ∫ θ, L n θ ∂μ ≤ (∫ θ in Ioi t, L n θ ∂μ) * ∫ θ, L m θ ∂μ

Uses 1 · Used by 1

Statement usesAntitone likelihood ratio

Used byThe posterior is stochastically nonincreasing in the observation

DefinitionPosterior tail probability#✓fully proved

Posterior probability of {θ > t} after observing n, by Bayes' formula for the prior μ and likelihood L: (∫_{θ > t} L n θ dμ) / ∫ L n θ dμ. Meaningful when the marginal likelihood ∫ L n dμ is positive (otherwise the division returns the junk value 0), and a genuine posterior probability only when L is nonnegative (as in the MLR predicates: a signed L can give a value outside [0, 1]).

noncomputable def posteriorTail (μ : Measure ℝ) (L : ℕ → ℝ → ℝ) (n : ℕ) (t : ℝ) : ℝ :=
  (∫ θ in Ioi t, L n θ ∂μ) / ∫ θ, L n θ ∂μ

Used by 4

Used byPosterior of s_het is stochastically nonincreasing in the PTV count, any antitone mean · Cassa et al. (2017) model · The posterior is stochastically nonincreasing in the observation · The posterior is stochastically nondecreasing in the observation

TheoremThe posterior is stochastically nondecreasing in the observation#✓fully proved

The posterior is stochastically nondecreasing in the observation for an MLR family and every prior (Milgrom 1981, Prop. 2): if n ≤ m and both marginal likelihoods are positive, then P(θ > t ∣ n) ≤ P(θ > t ∣ m) for every t.

theorem posteriorTail_mono_of_hasMLR {μ : Measure ℝ}
    {L : ℕ → ℝ → ℝ} {S : Set ℝ} (hμS : μ Sᶜ = 0)
    (hL : HasMonotoneLikelihoodRatioOn L S) (hint : ∀ n, Integrable (L n) μ)
    {n m : ℕ} (hnm : n ≤ m) (hn : 0 < ∫ θ, L n θ ∂μ) (hm : 0 < ∫ θ, L m θ ∂μ) (t : ℝ) :
    posteriorTail μ L n t ≤ posteriorTail μ L m t

Uses 3

Statement usesMonotone likelihood ratio · Posterior tail probability

Proof usesPosterior stochastic ordering, cross-multiplied form

TheoremThe posterior is stochastically nonincreasing in the observation#✓fully proved

The posterior is stochastically nonincreasing in the observation for a family with an antitone likelihood ratio and every prior: if n ≤ m and both marginal likelihoods are positive, then P(θ > t ∣ m) ≤ P(θ > t ∣ n) for every t.

theorem posteriorTail_anti_of_hasAntitoneLR {μ : Measure ℝ}
    {L : ℕ → ℝ → ℝ} {S : Set ℝ} (hμS : μ Sᶜ = 0)
    (hL : HasAntitoneLikelihoodRatioOn L S) (hint : ∀ n, Integrable (L n) μ)
    {n m : ℕ} (hnm : n ≤ m) (hn : 0 < ∫ θ, L n θ ∂μ) (hm : 0 < ∫ θ, L m θ ∂μ) (t : ℝ) :
    posteriorTail μ L m t ≤ posteriorTail μ L n t

Uses 3 · Used by 1

Statement usesAntitone likelihood ratio · Posterior tail probability

Proof usesPosterior stochastic ordering for an antitone likelihood ratio, cross-multiplied form

Used byPosterior of s_het is stochastically nonincreasing in the PTV count, any antitone mean

DefinitionPoisson likelihood#✓fully proved

Poisson likelihood with parameter-dependent mean λ θ: L n θ = e^{-λ θ} λ θ ^ n / (n !).

noncomputable def poissonLik (lam : ℝ → ℝ) (n : ℕ) (θ : ℝ) : ℝ :=
  exp (-lam θ) * lam θ ^ n / n !

Used by 4

Used byPosterior of s_het is stochastically nonincreasing in the PTV count, any antitone mean · Cassa et al. (2017) model · Poisson family with antitone mean has antitone likelihood ratio · Poisson family with monotone mean has monotone likelihood ratio

TheoremPoisson family with monotone mean has monotone likelihood ratio#✓fully proved

A Poisson family whose mean is nonnegative and monotone on S has a monotone likelihood ratio on S.

theorem poissonLik_hasMLR {lam : ℝ → ℝ} {S : Set ℝ} (hmono : MonotoneOn lam S)
    (hnn : ∀ θ ∈ S, 0 ≤ lam θ) : HasMonotoneLikelihoodRatioOn (poissonLik lam) S

Uses 2

Statement usesMonotone likelihood ratio · Poisson likelihood

TheoremPoisson family with antitone mean has antitone likelihood ratio#✓fully proved

A Poisson family whose mean is nonnegative and antitone on S has an antitone likelihood ratio on S.

theorem poissonLik_hasAntitoneLR {lam : ℝ → ℝ} {S : Set ℝ} (hanti : AntitoneOn lam S)
    (hnn : ∀ θ ∈ S, 0 ≤ lam θ) : HasAntitoneLikelihoodRatioOn (poissonLik lam) S

Uses 2 · Used by 1

Statement usesAntitone likelihood ratio · Poisson likelihood

Used byPosterior of s_het is stochastically nonincreasing in the PTV count, any antitone mean

DefinitionBinomial likelihood#✓fully proved

Binomial likelihood with N trials and parameter-dependent success probability p θ: L n θ = C(N, n) p θ ^ n (1 - p θ) ^ (N - n) (zero for n > N, since C(N, n) = 0).

noncomputable def binomialLik (N : ℕ) (p : ℝ → ℝ) (n : ℕ) (θ : ℝ) : ℝ :=
  (N.choose n : ℝ) * p θ ^ n * (1 - p θ) ^ (N - n)

Used by 1

Used byBinomial family has monotone likelihood ratio

TheoremBinomial family has monotone likelihood ratio#✓fully proved

A binomial family whose success probability lies in [0, 1] and is monotone on S has a monotone likelihood ratio on S.

theorem binomialLik_hasMLR {N : ℕ} {p : ℝ → ℝ} {S : Set ℝ} (hmono : MonotoneOn p S)
    (hp : ∀ θ ∈ S, p θ ∈ Icc (0 : ℝ) 1) : HasMonotoneLikelihoodRatioOn (binomialLik N p) S

Uses 2

Statement usesMonotone likelihood ratio · Binomial likelihood

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.